dfflibmap: fix formal $dffsr tests with sat, prove "no s&r" assumption only needed when appropriate

tests/techmap/dfflibmap_dffsr_x.lib

@@ -0,0 +1,33 @@
+library(test) {
+  cell (dffsr) {
+    area : 6;
+    ff("IQ", "IQN") {
+      next_state : "D";
+      clocked_on : "CLK";
+      clear      : "CLEAR";
+      preset     : "PRESET";
+      clear_preset_var1 : X;
+      clear_preset_var2 : X;
+    }
+    pin(D) {
+      direction : input;
+    }
+    pin(CLK) {
+      direction : input;
+    }
+    pin(CLEAR) {
+      direction : input;
+    }
+    pin(PRESET) {
+      direction : input;
+    }
+    pin(Q) {
+      direction: output;
+      function : "IQ";
+    }
+    pin(QN) {
+      direction: output;
+      function : "IQN";
+    }
+  }
+}

tests/techmap/dfflibmap_formal.ys

@@ -8,6 +8,7 @@ $_DFF_P_ ff0 (.C(C), .D(D), .Q(Q[0]));
 $_DFF_PP0_ ff1 (.C(C), .D(D), .R(R), .Q(Q[1]));
 $_DFF_PP1_ ff2 (.C(C), .D(D), .R(R), .Q(Q[2]));
 
+assume property (~R || ~S);
 $_DFFSR_PPP_ ff3 (.C(C), .D(D), .R(R), .S(S), .Q(Q[3]));
 $_DFFSR_NNN_ ff4 (.C(C), .D(D), .R(~R), .S(~S), .Q(Q[4]));
 
@@ -29,9 +30,12 @@ dfflibmap -liberty dfflibmap_dffsr_s.lib top
 clk2fflogic
 flatten
 opt_clean -purge
-equiv_make top top_unmapped equiv
+miter -equiv -make_assert -flatten top_unmapped top miter
-equiv_induct -set-assumes equiv
+hierarchy -top miter
-equiv_status -assert equiv
+# Prove that this is equivalent with the assumption
+sat -verify -prove-asserts -set-assumes -enable_undef -set-init-undef -show-public -seq 3 miter
+# Prove that this is NOT equivalent WITHOUT the assumption
+sat -falsify -prove-asserts -enable_undef -set-init-undef -seq 3 miter
 
 ##################################################################
 
@@ -44,6 +48,7 @@ $_DFF_P_ ff0 (.C(C), .D(D), .Q(Q[0]));
 $_DFF_PP0_ ff1 (.C(C), .D(D), .R(R), .Q(Q[1]));
 $_DFF_PP1_ ff2 (.C(C), .D(D), .R(R), .Q(Q[2]));
 
+assume property (~R || ~S);
 $_DFFSR_PPP_ ff3 (.C(C), .D(D), .R(R), .S(S), .Q(Q[3]));
 $_DFFSR_NNN_ ff4 (.C(C), .D(D), .R(~R), .S(~S), .Q(Q[4]));
 
@@ -65,9 +70,12 @@ dfflibmap -liberty dfflibmap_dffsr_r.lib top
 clk2fflogic
 flatten
 opt_clean -purge
-equiv_make top top_unmapped equiv
+miter -equiv -make_assert -flatten top_unmapped top miter
-equiv_induct -set-assumes equiv
+hierarchy -top miter
-equiv_status -assert equiv
+# Prove that this is equivalent with the assumption
+sat -verify -prove-asserts -set-assumes -enable_undef -set-init-undef -show-public -seq 3 miter
+# Prove that this is NOT equivalent WITHOUT the assumption
+sat -falsify -prove-asserts -enable_undef -set-init-undef -seq 3 miter
 
 ##################################################################
 
@@ -80,11 +88,47 @@ $_DFF_P_ ff0 (.C(C), .D(D), .Q(Q[0]));
 $_DFF_PP0_ ff1 (.C(C), .D(D), .R(R), .Q(Q[1]));
 $_DFF_PP1_ ff2 (.C(C), .D(D), .R(R), .Q(Q[2]));
 
-// Formal checking of directly instantiated DFFSR doesn't work at the moment
+// no assume when mapping to X
-// likely due to an equiv_induct -set-assumes assume bug #5196
+$_DFFSR_PPP_ ff3 (.C(C), .D(D), .R(R), .S(S), .Q(Q[3]));
+$_DFFSR_NNN_ ff4 (.C(C), .D(D), .R(~R), .S(~S), .Q(Q[4]));
 
-// Workaround for DFFSR bug #5194
+$_DFFE_PP_ ff5 (.C(C), .D(D), .E(E), .Q(Q[5]));
-assume property (~R || ~S);
+
+assign Q[11:6] = ~Q[5:0];
+
+endmodule
+
+EOT
+
+proc
+opt
+read_liberty dfflibmap_dffsr_x.lib
+opt
+
+copy top top_unmapped
+dfflibmap -liberty dfflibmap_dffsr_x.lib top
+
+clk2fflogic
+flatten
+opt_clean -purge
+miter -equiv -make_assert -flatten top_unmapped top miter
+hierarchy -top miter
+
+# Prove that this is equivalent
+sat -verify -prove-asserts -set-init-undef -show-public -seq 3 miter
+
+##################################################################
+
+design -reset
+read_verilog -sv -icells <<EOT
+
+module top(input C, D, E, S, R, output [11:0] Q);
+
+$_DFF_P_ ff0 (.C(C), .D(D), .Q(Q[0]));
+$_DFF_PP0_ ff1 (.C(C), .D(D), .R(R), .Q(Q[1]));
+$_DFF_PP1_ ff2 (.C(C), .D(D), .R(R), .Q(Q[2]));
+
+// no assume when mapping to unset clear_preset_var
 $_DFFSR_PPP_ ff3 (.C(C), .D(D), .R(R), .S(S), .Q(Q[3]));
 $_DFFSR_NNN_ ff4 (.C(C), .D(D), .R(~R), .S(~S), .Q(Q[4]));
 
@@ -107,9 +151,11 @@ dfflibmap -liberty dfflibmap_dffn_dffe.lib -liberty dfflibmap_dffsr_not_next.lib
 clk2fflogic
 flatten
 opt_clean -purge
-equiv_make top top_unmapped equiv
+miter -equiv -make_assert -flatten top_unmapped top miter
-equiv_induct -set-assumes equiv
+hierarchy -top miter
-equiv_status -assert equiv
+
+# Prove that this is equivalent
+sat -verify -prove-asserts -set-init-undef -show-public -seq 3 miter
 
 ##################################################################
 
@@ -122,10 +168,6 @@ $_DFF_P_ ff0 (.C(C), .D(D), .Q(Q[0]));
 $_DFF_PP0_ ff1 (.C(C), .D(D), .R(R), .Q(Q[1]));
 $_DFF_PP1_ ff2 (.C(C), .D(D), .R(R), .Q(Q[2]));
 
-// Formal checking of directly instantiated DFFSR doesn't work at the moment
-// likely due to an equiv_induct -set-assumes assume bug #5196
-
-// Workaround for DFFSR inconsistency #5194
 assume property (~R || ~S);
 $_DFFSR_PPP_ ff3 (.C(C), .D(D), .R(R), .S(S), .Q(Q[3]));
 $_DFFSR_NNN_ ff4 (.C(C), .D(D), .R(~R), .S(~S), .Q(Q[4]));
@@ -140,17 +182,21 @@ EOT
 
 proc
 opt
-read_liberty dfflibmap_dffr_not_next.lib
+read_liberty dfflibmap_dffsr_not_next_l.lib
 
 copy top top_unmapped
-dfflibmap -liberty dfflibmap_dffr_not_next.lib top
+dfflibmap -liberty dfflibmap_dffsr_not_next_l.lib top
 
 clk2fflogic
 flatten
 opt_clean -purge
-equiv_make top top_unmapped equiv
+miter -equiv -make_assert -flatten top_unmapped top miter
-equiv_induct -set-assumes equiv
+hierarchy -top miter
-equiv_status -assert equiv
+
+# Prove that this is equivalent with the assumption
+sat -verify -prove-asserts -set-assumes -enable_undef -set-init-undef -show-public -seq 3 miter
+# Prove that this is NOT equivalent WITHOUT the assumption
+sat -falsify -prove-asserts -enable_undef -set-init-undef -seq 3 miter
 
 ##################################################################
 

tests/techmap/dfflibmap_proc_formal.ys

@@ -52,48 +52,49 @@ dfflibmap -liberty dfflibmap_dffsr_s.lib top
 clk2fflogic
 flatten
 opt_clean -purge
-equiv_make top top_unmapped equiv
+miter -equiv -make_assert -flatten top_unmapped top miter
-equiv_induct equiv
+
-equiv_status -assert equiv
+# Prove that this is equivalent
+sat -verify -prove-asserts -set-init-undef -show-public -seq 3 miter
 
 ##################################################################
 
-delete top equiv
+delete top miter
 
 copy top_unmapped top
 dfflibmap -liberty dfflibmap_dffsr_r.lib top
 
 clk2fflogic
 flatten
-opt_clean -purge
+miter -equiv -make_assert -flatten top_unmapped top miter
-equiv_make top top_unmapped equiv
+
-equiv_induct equiv
+# Prove that this is equivalent
-equiv_status -assert equiv
+sat -verify -prove-asserts -set-init-undef -show-public -seq 3 miter
 
 ##################################################################
 
-delete top equiv
+delete top miter
 
 copy top_unmapped top
 dfflibmap -liberty dfflibmap_dffsr_mixedpol.lib top
 
 async2sync
 flatten
-opt_clean -purge
+miter -equiv -make_assert -flatten top_unmapped top miter
-equiv_make top top_unmapped equiv
+
-equiv_induct equiv
+# Prove that this is equivalent
-equiv_status -assert equiv
+sat -verify -prove-asserts -set-init-undef -show-public -seq 3 miter
 
 ##################################################################
 
-delete top equiv
+delete top miter
 
 copy top_unmapped top
 dfflibmap -liberty dfflibmap_dffsr_not_next.lib top
 
 async2sync
 flatten
-opt_clean -purge
+miter -equiv -make_assert -flatten top_unmapped top miter
-equiv_make top top_unmapped equiv
+
-equiv_induct equiv
+# Prove that this is equivalent
-equiv_status -assert equiv
+sat -verify -prove-asserts -set-init-undef -show-public -seq 3 miter