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:*
76 module peepopt_dffmuxext_unsigned(input clk, ce, input [1:0] i, output reg [3:0] o);
77 always @(posedge clk) if (ce) o <= i;
82 equiv_opt -assert peepopt
85 select -assert-count 1 t:$dff r:WIDTH=2 %i
86 select -assert-count 1 t:$mux r:WIDTH=2 %i
87 select -assert-count 0 t:$dff t:$mux %% t:* %D
93 module peepopt_dffmuxext_signed(input clk, ce, input signed [1:0] i, output reg signed [3:0] o);
94 always @(posedge clk) if (ce) o <= i;
99 equiv_opt -assert peepopt
102 select -assert-count 1 t:$dff r:WIDTH=2 %i
103 select -assert-count 1 t:$mux r:WIDTH=2 %i
104 select -assert-count 0 t:$dff t:$mux %% t:* %D
110 module peepopt_dffmuxext_const(input clk, ce, input [1:0] i, output reg [5:0] o);
111 always @(posedge clk) if (ce) o <= {1'b0, i[1], 2'b1x, i[0], 1'bz};
116 equiv_opt -assert peepopt
118 select -assert-count 1 t:$dff r:WIDTH=2 %i
119 select -assert-count 1 t:$mux r:WIDTH=2 %i
120 select -assert-count 0 t:$dff t:$mux %% t:* %D
126 module peepopt_dffmuxext_const_init(input clk, ce, input [1:0] i, (* init=6'b0x00x1 *) output reg [5:0] o);
127 always @(posedge clk) if (ce) o <= {1'b0, i[1], 2'b1x, i[0], 1'bz};
132 equiv_opt -assert peepopt
134 select -assert-count 1 t:$dff r:WIDTH=4 %i
135 select -assert-count 1 t:$mux r:WIDTH=4 %i
136 select -assert-count 0 t:$dff t:$mux %% t:* %D
142 module peepopt_dffmuxext_unsigned_rst(input clk, ce, rst, input [1:0] i, output reg [3:0] o);
143 always @(posedge clk) if (rst) o <= 0; else if (ce) o <= i;
148 equiv_opt -assert peepopt
151 select -assert-count 1 t:$dff r:WIDTH=2 %i
152 select -assert-count 2 t:$mux
153 select -assert-count 2 t:$mux r:WIDTH=2 %i
154 select -assert-count 0 t:$dff t:$mux %% t:* %D
160 module peepopt_dffmuxext_signed_rst(input clk, ce, rstn, input signed [1:0] i, output reg signed [3:0] o);
161 always @(posedge clk) begin
163 if (!rstn) o <= 4'b1111;
169 equiv_opt -assert peepopt
172 select -assert-count 1 t:$dff r:WIDTH=2 %i
173 select -assert-count 2 t:$mux
174 select -assert-count 2 t:$mux r:WIDTH=2 %i
175 select -assert-count 0 t:$logic_not t:$dff t:$mux %% t:* %D
181 module peepopt_dffmuxext_signed_rst_init(input clk, ce, rstn, input signed [1:0] i, output reg signed [3:0] o);
182 initial o <= 4'b0010;
183 always @(posedge clk) begin
185 if (!rstn) o <= 4'b1111;
191 # NB: equiv_opt uses equiv_induct which covers
192 # only the induction half of temporal induction
193 # --- missing the base-case half
194 # This makes it akin to `sat -tempinduct-inductonly`
195 # instead of `sat -tempinduct-baseonly` or
196 # `sat -tempinduct` which is necessary for this
198 #equiv_opt -assert peepopt
204 design -import gold -as gold
205 design -import gate -as gate
206 miter -equiv -flatten -make_assert -make_outputs gold gate miter
207 sat -tempinduct -verify -prove-asserts -show-ports miter
210 select -assert-count 1 t:$dff r:WIDTH=4 %i
211 select -assert-count 2 t:$mux
212 select -assert-count 2 t:$mux r:WIDTH=4 %i
213 select -assert-count 0 t:$logic_not t:$dff t:$mux %% t:* %D