dfflibmap: test dffsr with either priority liberty file

tests/techmap/dfflibmap.ys

@@ -64,8 +64,8 @@ select -assert-count 1 t:dffe
 select -assert-none t:dffn t:dffsr t:dffe t:$_NOT_ %% %n t:* %i
 
 design -load orig
-dfflibmap -prepare -liberty dfflibmap_dffn_dffe.lib -liberty dfflibmap_dffsr.lib
+dfflibmap -prepare -liberty dfflibmap_dffn_dffe.lib -liberty dfflibmap_dffsr_r.lib
-dfflibmap -map-only -liberty dfflibmap_dffn_dffe.lib -liberty dfflibmap_dffsr.lib
+dfflibmap -map-only -liberty dfflibmap_dffn_dffe.lib -liberty dfflibmap_dffsr_r.lib
 clean
 
 select -assert-count 5 t:$_NOT_

tests/techmap/dfflibmap_dffsr_r.lib

@@ -7,8 +7,8 @@ library(test) {
       clear      : "CLEAR";
       preset     : "PRESET";
       clear_preset_var1 : L;
-      clear_preset_var2 : L;
+      clear_preset_var2 : H;
-    } 
+    }
     pin(D) {
       direction : input;
     }
@@ -28,6 +28,6 @@ library(test) {
     pin(QN) {
       direction: output;
       function : "IQN";
-    } 
+    }
   }
 }

tests/techmap/dfflibmap_dffsr_s.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 : H;
+      clear_preset_var2 : L;
+    }
+    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

@@ -21,10 +21,46 @@ EOT
 
 proc
 opt
-read_liberty dfflibmap_dffsr.lib
+read_liberty dfflibmap_dffsr_s.lib
 
 copy top top_unmapped
-dfflibmap -liberty dfflibmap_dffsr.lib top
+dfflibmap -liberty dfflibmap_dffsr_s.lib top
+
+async2sync
+flatten
+opt_clean -purge
+equiv_make top top_unmapped equiv
+equiv_induct equiv
+equiv_status -assert equiv
+
+##################################################################
+
+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]));
+
+$_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]));
+
+$_DFFE_PP_ ff5 (.C(C), .D(D), .E(E), .Q(Q[5]));
+
+assign Q[11:6] = ~Q[5:0];
+
+endmodule
+
+EOT
+
+proc
+opt
+read_liberty dfflibmap_dffsr_r.lib
+
+copy top top_unmapped
+dfflibmap -liberty dfflibmap_dffsr_r.lib top
 
 async2sync
 flatten