From f2cf07584d8f3eafc8bc1ecde2ae0a3e6e8bdf23 Mon Sep 17 00:00:00 2001 From: nella Date: Wed, 5 Aug 2026 12:55:13 +0200 Subject: [PATCH] Improve test coverage. --- tests/opt/opt_dff_sat_const.ys | 172 +++++++++++++++++++++++++++++++++ 1 file changed, 172 insertions(+) create mode 100644 tests/opt/opt_dff_sat_const.ys 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