1read_verilog <<EOT 2module peepopt_shiftmul_0 #(parameter N=3, parameter W=3) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output [W-1:0] o); 3assign o = i[s*W+:W]; 4endmodule 5EOT 6 7prep -nokeepdc 8equiv_opt -assert peepopt 9design -load postopt 10clean 11select -assert-count 1 t:$shiftx 12select -assert-count 0 t:$shiftx t:* %D 13 14#################### 15 16design -reset 17read_verilog <<EOT 18module peepopt_shiftmul_1 (output [7:0] y, input [2:0] w); 19assign y = 1'b1 >> (w * (3'b110)); 20endmodule 21EOT 22 23prep -nokeepdc 24equiv_opt -assert peepopt 25design -load postopt 26clean 27select -assert-count 1 t:$shr 28select -assert-count 1 t:$mul 29select -assert-count 0 t:$shr t:$mul %% t:* %D 30 31#################### 32 33design -reset 34read_verilog <<EOT 35module peepopt_shiftmul_2 (input [11:0] D, input [1:0] S, output [11:0] Y); 36 assign Y = D >> (S*3); 37endmodule 38EOT 39 40prep 41design -save gold 42peepopt 43design -stash gate 44 45design -import gold -as gold peepopt_shiftmul_2 46design -import gate -as gate peepopt_shiftmul_2 47 48miter -equiv -make_assert -make_outputs -ignore_gold_x -flatten gold gate miter 49sat -show-public -enable_undef -prove-asserts miter 50cd gate 51select -assert-count 1 t:$shr 52select -assert-count 1 t:$mul 53select -assert-count 0 t:$shr t:$mul %% t:* %D 54 55#################### 56 57design -reset 58read_verilog <<EOT 59module peepopt_muldiv_0(input [1:0] i, output [1:0] o); 60wire [3:0] t; 61assign t = i * 3; 62assign o = t / 3; 63endmodule 64EOT 65 66prep -nokeepdc 67equiv_opt -assert peepopt 68design -load postopt 69clean 70select -assert-count 0 t:* 71