2 module 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);
8 equiv_opt -assert peepopt
11 select -assert-count 1 t:$shiftx
12 select -assert-count 0 t:$shiftx t:* %D
18 module peepopt_shiftmul_1 (output [7:0] y, input [2:0] w);
19 assign y = 1'b1 >> (w * (3'b110));
24 equiv_opt -assert peepopt
27 select -assert-count 1 t:$shr
28 select -assert-count 1 t:$mul
29 select -assert-count 0 t:$shr t:$mul %% t:* %D
35 module peepopt_shiftmul_2 (input [11:0] D, input [1:0] S, output [11:0] Y);
36 assign Y = D >> (S*3);
45 design -import gold -as gold peepopt_shiftmul_2
46 design -import gate -as gate peepopt_shiftmul_2
48 miter -equiv -make_assert -make_outputs -ignore_gold_x -flatten gold gate miter
49 sat -show-public -enable_undef -prove-asserts miter
51 select -assert-count 1 t:$shr
52 select -assert-count 1 t:$mul
53 select -assert-count 0 t:$shr t:$mul %% t:* %D
59 module peepopt_muldiv_0(input [1:0] i, output [1:0] o);
67 equiv_opt -assert peepopt
70 select -assert-count 0 t:*