diff --git a/tests/opt/opt_dff_sat_const.ys b/tests/opt/opt_dff_sat_const.ys new file mode 100644 index 000000000..8c8000e8a --- /dev/null +++ b/tests/opt/opt_dff_sat_const.ys @@ -0,0 +1,172 @@ +# D depends on Q +design -reset +read_verilog -sv < 4'd10) & (a < 4'd3); + end + end +endmodule +EOT + +hierarchy -top test_case +prep +design -save gold + +opt_dff +opt_clean -purge +select -assert-count 2 t:$sdff + +# q0 folds (init 0, srst 0, D proven 0), q1 must stay (init 1, srst 0) +design -load gold +opt_dff -sat +opt_clean -purge +select -assert-count 1 t:$sdff +design -save gate + +design -load gold +design -copy-from gate -as gate test_case +equiv_make test_case gate equiv +equiv_induct equiv +equiv_status -assert + + +# async load +design -reset +read_verilog -sv < 4'd10) & (a < 4'd3); + else q0 <= q0 & en; + always @(posedge clk or posedge load) + if (load) q1 <= a[0]; + else q1 <= q1 & en; +endmodule +EOT + +hierarchy -top test_case +prep +select -assert-count 2 t:$aldff +design -save gold + +opt_dff +opt_clean -purge +select -assert-count 2 t:$aldff + +design -load gold +opt_dff -sat +opt_clean -purge +select -assert-count 1 t:$aldff +design -save gate + +design -load gold +design -copy-from gate -as gate test_case +async2sync +equiv_make test_case gate equiv +equiv_induct equiv +equiv_status -assert