filterlib, read_liberty: add loopy retention cell formal equivalence test

tests/liberty/dff.lib.verilogsim.ok

@@ -5,11 +5,9 @@ module dff (D, CLK, Q);
   output Q;
   assign Q = IQ; // IQ
   always @(posedge CLK) begin
-      // D
       IQ <= D;
   end
   always @(posedge CLK) begin
-      // ~(D)
       IQN <= ~(D);
   end
 endmodule

tests/liberty/normal.lib.verilogsim.ok

@@ -58,7 +58,6 @@ module dff (D, CLK, RESET, PRESET, Q, QN);
       IQ <= 1;
     end
     else begin
-      // D
       IQ <= D;
     end
   end
@@ -70,7 +69,6 @@ module dff (D, CLK, RESET, PRESET, Q, QN);
       IQN <= 1;
     end
     else begin
-      // ~(D)
       IQN <= ~(D);
     end
   end

tests/liberty/read_liberty.ys

@@ -0,0 +1,9 @@
+read_liberty retention.lib
+rename retention_cell retention_cell_lib
+read_verilog retention.lib.verilogsim
+proc
+rename retention_cell retention_cell_vlog
+async2sync
+equiv_make retention_cell_lib retention_cell_vlog equiv
+equiv_induct equiv
+equiv_status -assert equiv

tests/liberty/retention.lib

@@ -0,0 +1,57 @@
+library (retention) {
+    delay_model : table_lookup;
+    voltage_unit : 1V;
+    current_unit : 1mA;
+    leakage_power_unit : 1nW;
+    time_unit : 1ns;
+    capacitive_load_unit (1, pf);
+    pulling_resistance_unit : 1kohm;
+    input_threshold_pct_rise : 50;
+    input_threshold_pct_fall : 50;
+    output_threshold_pct_rise : 50;
+    output_threshold_pct_fall : 50;
+    slew_lower_threshold_pct_rise : 30;
+    slew_upper_threshold_pct_rise : 70;
+    slew_upper_threshold_pct_fall : 70;
+    slew_lower_threshold_pct_fall : 30;
+    cell ("retention_cell") {
+        ff (Q1,QN1) {
+            clocked_on : "CK";
+            next_state : "(D * !SE + SI * SE)";
+            clear : "(((!B2B) * !Q2) + !RD)";
+            preset : "((!B2B) * Q2)";
+            clear_preset_var1 : "L";
+            clear_preset_var2 : "H";
+        }
+        latch (Q2,QN2) {
+            enable : "B1";
+            data_in : "Q1";
+        }
+        pin (B1) {
+            direction : input;
+        }
+        pin (B2B) {
+            direction : input;
+        }
+        pin (CK) {
+            clock : true;
+            direction : input;
+        }
+        pin (D) {
+            direction : input;
+        }
+        pin (Q) {
+            direction : output;
+            function : "Q1";
+        }
+        pin (RD) {
+            direction : input;
+        }
+        pin (SE) {
+            direction : input;
+        }
+        pin (SI) {
+            direction : input;
+        }
+    }
+}

tests/liberty/retention.lib.filtered.ok

@@ -0,0 +1,42 @@
+library(retention) {
+  cell("retention_cell") {
+    ff(Q1, QN1) {
+      clocked_on : "CK" ;
+      next_state : "(D * !SE + SI * SE)" ;
+      clear : "(((!B2B) * !Q2) + !RD)" ;
+      preset : "((!B2B) * Q2)" ;
+      clear_preset_var1 : "L" ;
+      clear_preset_var2 : "H" ;
+    }
+    latch(Q2, QN2) {
+      enable : "B1" ;
+      data_in : "Q1" ;
+    }
+    pin(B1) {
+      direction : input ;
+    }
+    pin(B2B) {
+      direction : input ;
+    }
+    pin(CK) {
+      clock : true ;
+      direction : input ;
+    }
+    pin(D) {
+      direction : input ;
+    }
+    pin(Q) {
+      direction : output ;
+      function : "Q1" ;
+    }
+    pin(RD) {
+      direction : input ;
+    }
+    pin(SE) {
+      direction : input ;
+    }
+    pin(SI) {
+      direction : input ;
+    }
+  }
+}

tests/liberty/retention.lib.verilogsim.ok

@@ -0,0 +1,44 @@
+module retention_cell (B1, B2B, CK, D, Q, RD, SE, SI);
+  reg Q1, QN1;
+  wire Q1_clear, Q1_preset;
+  reg Q2, QN2;
+  input B1;
+  input B2B;
+  input CK;
+  input D;
+  output Q;
+  assign Q = Q1; // "Q1"
+  input RD;
+  input SE;
+  input SI;
+  always @(posedge CK, posedge Q1_clear, posedge Q1_preset) begin
+    if (Q1_clear) begin
+      Q1 <= 0;
+    end
+    else if (Q1_preset) begin
+      Q1 <= 1;
+    end
+    else begin
+      Q1 <= ((D&(~SE))|(SI&SE));
+    end
+  end
+  always @(posedge CK, posedge Q1_clear, posedge Q1_preset) begin
+    if (Q1_clear) begin
+      QN1 <= 1;
+    end
+    else if (Q1_preset) begin
+      QN1 <= 0;
+    end
+    else begin
+      QN1 <= ~(((D&(~SE))|(SI&SE)));
+    end
+  end
+  assign Q1_clear = (((~B2B)&(~Q2))|(~RD));
+  assign Q1_preset = ((~B2B)&Q2);
+  always @* begin
+    if (B1) begin
+      Q2 <= Q1;
+      QN2 <= ~(Q1);
+    end
+  end
+endmodule

tests/liberty/semicolextra.lib.verilogsim.ok

@@ -4,11 +4,9 @@ module DFF (D, CK, Q);
   input CK;
   output Q;
   always @(posedge CK) begin
-      // D
       IQ <= D;
   end
   always @(posedge CK) begin
-      // ~(D)
       IQN <= ~(D);
   end
 endmodule

tests/liberty/unquoted.lib.verilogsim.ok

@@ -5,11 +5,9 @@ module dff1 (D, CLK, Q);
   output Q;
   assign Q = IQ; // IQ
   always @(posedge CLK) begin
-      // (~D)
       IQ <= (~D);
   end
   always @(posedge CLK) begin
-      // ~((~D))
       IQN <= ~((~D));
   end
 endmodule
@@ -20,11 +18,9 @@ module dff2 (D, CLK, Q);
   output Q;
   assign Q = IQ; // "IQ"
   always @(posedge CLK) begin
-      // (~D)
       IQ <= (~D);
   end
   always @(posedge CLK) begin
-      // ~((~D))
       IQN <= ~((~D));
   end
 endmodule
@@ -38,11 +34,9 @@ module dffe (D, EN, CLK, Q, QN);
   output QN;
   assign QN = IQN; // "IQN"
   always @(negedge CLK) begin
-      // ((D&EN)|(IQ&(~EN)))
       IQ <= ((D&EN)|(IQ&(~EN)));
   end
   always @(negedge CLK) begin
-      // ~(((D&EN)|(IQ&(~EN))))
       IQN <= ~(((D&EN)|(IQ&(~EN))));
   end
 endmodule