This commit is contained in:
Eddie Hung 2019-10-02 17:48:55 -07:00
parent 62c66406ad
commit e730a595ee
1 changed files with 31 additions and 0 deletions

View File

@ -173,3 +173,34 @@ select -assert-count 1 t:$dff r:WIDTH=2 %i
select -assert-count 2 t:$mux
select -assert-count 2 t:$mux r:WIDTH=2 %i
select -assert-count 0 t:$logic_not t:$dff t:$mux %% t:* %D
####################
design -reset
read_verilog <<EOT
module peepopt_dffmuxext_signed_rst_init(input clk, ce, rstn, input signed [1:0] i, output reg signed [3:0] o);
initial o <= 4'b0010;
always @(posedge clk) begin
if (ce) o <= i;
if (!rstn) o <= 4'b1111;
end
endmodule
EOT
proc
#equiv_opt -assert peepopt
design -save gold
peepopt
design -stash gate
design -import gold -as gold
design -import gate -as gate
miter -equiv -flatten -make_assert -make_outputs gold gate miter
sat -seq 1 -verify -prove-asserts -show-ports miter
design -load postopt
wreduce
select -assert-count 1 t:$dff r:WIDTH=2 %i
select -assert-count 2 t:$mux
select -assert-count 2 t:$mux r:WIDTH=2 %i
select -assert-count 0 t:$logic_not t:$dff t:$mux %% t:* %D