abc9_map.v to transform INIT=1 to INIT=0

diff --git a/techlibs/xilinx/abc9_map.v b/techlibs/xilinx/abc9_map.v
index d84b9a8fa9031892f2cbee674dd315ec797cc84f..3fa5f5a1cd4468c2b4beef0381e1fec3c86efc65 100644 (file)
--- a/techlibs/xilinx/abc9_map.v
+++ b/techlibs/xilinx/abc9_map.v
@@ -71,27 +71,39 @@
 //     state
 // (e) a special _TECHMAP_REPLACE_.$abc9_currQ wire that will be used for feedback
 //     into the (combinatorial) FD* cell to facilitate clock-enable behaviour
+//
 // In order to perform sequential synthesis, `abc9' also requires that
 // the initial value of all flops be zero.
+
 module FDRE (output Q, input C, CE, D, R);
   parameter [0:0] INIT = 1'b0;
   parameter [0:0] IS_C_INVERTED = 1'b0;
   parameter [0:0] IS_D_INVERTED = 1'b0;
   parameter [0:0] IS_R_INVERTED = 1'b0;
-  wire DD, QQ, $nextQ;
-  generate if (INIT == 1'b1)
-    assign DD = ~D, Q = ~QQ;
-  else
-    assign DD = D, Q = QQ;
+  wire QQ, $nextQ;
+  generate if (INIT == 1'b1) begin
+    assign Q = ~QQ;
+    FDSE #(
+      .INIT(1'b0),
+      .IS_C_INVERTED(IS_C_INVERTED),
+      .IS_D_INVERTED(IS_D_INVERTED),
+      .IS_S_INVERTED(IS_R_INVERTED)
+    ) _TECHMAP_REPLACE_ (
+      .D(~D), .Q($nextQ), .C(C), .CE(CE), .S(R)
+    );
+  end
+  else begin
+    assign Q = QQ;
+    FDRE #(
+      .INIT(1'b0),
+      .IS_C_INVERTED(IS_C_INVERTED),
+      .IS_D_INVERTED(IS_D_INVERTED),
+      .IS_R_INVERTED(IS_R_INVERTED)
+    ) _TECHMAP_REPLACE_ (
+      .D(D), .Q($nextQ), .C(C), .CE(CE), .R(R)
+    );
+  end
   endgenerate
-  FDRE #(
-    .INIT(1'b0),
-    .IS_C_INVERTED(IS_C_INVERTED),
-    .IS_D_INVERTED(IS_D_INVERTED),
-    .IS_R_INVERTED(IS_R_INVERTED)
-  ) _TECHMAP_REPLACE_ (
-    .D(DD), .Q($nextQ), .C(C), .CE(CE), .R(R)
-  );
   \$__ABC9_FF_ abc_dff (.D($nextQ), .Q(QQ));
 
   // Special signals
@@ -102,17 +114,24 @@ module FDRE (output Q, input C, CE, D, R);
 endmodule
 module FDRE_1 (output Q, input C, CE, D, R);
   parameter [0:0] INIT = 1'b0;
-  wire DD, QQ, $nextQ;
-  generate if (INIT == 1'b1)
-    assign DD = ~D, Q = ~QQ;
-  else
-    assign DD = D, Q = QQ;
+  wire QQ, $nextQ;
+  generate if (INIT == 1'b1) begin
+    assign Q = ~QQ;
+    FDSE_1 #(
+      .INIT(1'b0)
+    ) _TECHMAP_REPLACE_ (
+      .D(~D), .Q($nextQ), .C(C), .CE(CE), .S(R)
+    );
+  end
+  else begin
+    assign Q = QQ;
+    FDRE_1 #(
+      .INIT(1'b0)
+    ) _TECHMAP_REPLACE_ (
+      .D(D), .Q($nextQ), .C(C), .CE(CE), .R(R)
+    );
+  end
   endgenerate
-  FDRE_1 #(
-    .INIT(1'b0),
-  ) _TECHMAP_REPLACE_ (
-    .D(DD), .Q($nextQ), .C(C), .CE(CE), .R(R)
-  );
   \$__ABC9_FF_ abc_dff (.D($nextQ), .Q(QQ));
 
   // Special signals
@@ -127,25 +146,39 @@ module FDCE (output Q, input C, CE, D, CLR);
   parameter [0:0] IS_C_INVERTED = 1'b0;
   parameter [0:0] IS_D_INVERTED = 1'b0;
   parameter [0:0] IS_CLR_INVERTED = 1'b0;
-  wire DD, QQ, $nextQ, $abc9_currQ;
-  generate if (INIT == 1'b1)
-    assign DD = ~D, Q = ~QQ;
-  else
-    assign DD = D, Q = QQ;
-  endgenerate
-  FDCE #(
-    .INIT(1'b0),
-    .IS_C_INVERTED(IS_C_INVERTED),
-    .IS_D_INVERTED(IS_D_INVERTED),
-    .IS_CLR_INVERTED(IS_CLR_INVERTED)
-  ) _TECHMAP_REPLACE_ (
-    .D(DD), .Q($nextQ), .C(C), .CE(CE), .CLR(CLR)
-                                          // ^^^ Note that async
-                                          //     control is not directly
-                                          //     supported by abc9 but its
-                                          //     behaviour is captured by
-                                          //     $__ABC9_ASYNC below
-  );
+  wire QQ, $nextQ, $abc9_currQ;
+  generate if (INIT == 1'b1) begin
+    assign Q = ~QQ;
+    FDPE #(
+      .INIT(1'b0),
+      .IS_C_INVERTED(IS_C_INVERTED),
+      .IS_D_INVERTED(IS_D_INVERTED),
+      .IS_PRE_INVERTED(IS_CLR_INVERTED)
+    ) _TECHMAP_REPLACE_ (
+      .D(~D), .Q($nextQ), .C(C), .CE(CE), .PRE(CLR)
+                                            // ^^^ Note that async
+                                            //     control is not directly
+                                            //     supported by abc9 but its
+                                            //     behaviour is captured by
+                                            //     $__ABC9_ASYNC below
+    );
+  end
+  else begin
+    assign Q = QQ;
+    FDCE #(
+      .INIT(1'b0),
+      .IS_C_INVERTED(IS_C_INVERTED),
+      .IS_D_INVERTED(IS_D_INVERTED),
+      .IS_CLR_INVERTED(IS_CLR_INVERTED)
+    ) _TECHMAP_REPLACE_ (
+      .D(D), .Q($nextQ), .C(C), .CE(CE), .CLR(CLR)
+                                           // ^^^ Note that async
+                                           //     control is not directly
+                                           //     supported by abc9 but its
+                                           //     behaviour is captured by
+                                           //     $__ABC9_ASYNC below
+    );
+  end endgenerate
   \$__ABC9_FF_ abc_dff (.D($nextQ), .Q($abc9_currQ));
   // Since this is an async flop, async behaviour is also dealt with
   //   using the $_ABC9_ASYNC box by abc9_map.v
@@ -159,22 +192,32 @@ module FDCE (output Q, input C, CE, D, CLR);
 endmodule
 module FDCE_1 (output Q, input C, CE, D, CLR);
   parameter [0:0] INIT = 1'b0;
-  wire DD, QQ, $nextQ, $abc9_currQ;
-  generate if (INIT == 1'b1)
-    assign DD = ~D, Q = ~QQ;
-  else
-    assign DD = D, Q = QQ;
-  endgenerate
-  FDCE_1 #(
-    .INIT(1'b0)
-  ) _TECHMAP_REPLACE_ (
-    .D(DD), .Q($nextQ), .C(C), .CE(CE), .CLR(CLR)
-                                          // ^^^ Note that async
-                                          //     control is not directly
-                                          //     supported by abc9 but its
-                                          //     behaviour is captured by
-                                          //     $__ABC9_ASYNC below
-  );
+  generate if (INIT == 1'b1) begin
+    assign Q = ~QQ;
+    FDPE_1 #(
+      .INIT(1'b0)
+    ) _TECHMAP_REPLACE_ (
+      .D(~D), .Q($nextQ), .C(C), .CE(CE), .PRE(CLR)
+                                            // ^^^ Note that async
+                                            //     control is not directly
+                                            //     supported by abc9 but its
+                                            //     behaviour is captured by
+                                            //     $__ABC9_ASYNC below
+    );
+  end
+  else begin
+    assign Q = QQ;
+    FDCE_1 #(
+      .INIT(1'b0)
+    ) _TECHMAP_REPLACE_ (
+      .D(D), .Q($nextQ), .C(C), .CE(CE), .CLR(CLR)
+                                           // ^^^ Note that async
+                                           //     control is not directly
+                                           //     supported by abc9 but its
+                                           //     behaviour is captured by
+                                           //     $__ABC9_ASYNC below
+    );
+  end endgenerate
   \$__ABC9_FF_ abc_dff (.D($nextQ), .Q($abc9_currQ));
   \$__ABC9_ASYNC abc_async (.A($abc9_currQ), .S(CLR), .Y(QQ));
 
@@ -190,25 +233,39 @@ module FDPE (output Q, input C, CE, D, PRE);
   parameter [0:0] IS_C_INVERTED = 1'b0;
   parameter [0:0] IS_D_INVERTED = 1'b0;
   parameter [0:0] IS_PRE_INVERTED = 1'b0;
-  wire DD, QQ, $nextQ, $abc9_currQ;
-  generate if (INIT == 1'b1)
-    assign DD = ~D, Q = ~QQ;
-  else
-    assign DD = D, Q = QQ;
-  endgenerate
-  FDPE #(
-    .INIT(1'b0),
-    .IS_C_INVERTED(IS_C_INVERTED),
-    .IS_D_INVERTED(IS_D_INVERTED),
-    .IS_PRE_INVERTED(IS_PRE_INVERTED),
-  ) _TECHMAP_REPLACE_ (
-    .D(DD), .Q($nextQ), .C(C), .CE(CE), .PRE(PRE)
-                                          // ^^^ Note that async
-                                          //     control is not directly
-                                          //     supported by abc9 but its
-                                          //     behaviour is captured by
-                                          //     $__ABC9_ASYNC below
-  );
+  wire QQ, $nextQ, $abc9_currQ;
+  generate if (INIT == 1'b1) begin
+    assign Q = ~QQ;
+    FDCE #(
+      .INIT(1'b0),
+      .IS_C_INVERTED(IS_C_INVERTED),
+      .IS_D_INVERTED(IS_D_INVERTED),
+      .IS_CLR_INVERTED(IS_PRE_INVERTED),
+    ) _TECHMAP_REPLACE_ (
+      .D(~D), .Q($nextQ), .C(C), .CE(CE), .CLR(PRE)
+                                            // ^^^ Note that async
+                                            //     control is not directly
+                                            //     supported by abc9 but its
+                                            //     behaviour is captured by
+                                            //     $__ABC9_ASYNC below
+    );
+  end
+  else begin
+    assign Q = QQ;
+    FDPE #(
+      .INIT(1'b0),
+      .IS_C_INVERTED(IS_C_INVERTED),
+      .IS_D_INVERTED(IS_D_INVERTED),
+      .IS_PRE_INVERTED(IS_PRE_INVERTED),
+    ) _TECHMAP_REPLACE_ (
+      .D(D), .Q($nextQ), .C(C), .CE(CE), .PRE(PRE)
+                                           // ^^^ Note that async
+                                           //     control is not directly
+                                           //     supported by abc9 but its
+                                           //     behaviour is captured by
+                                           //     $__ABC9_ASYNC below
+    );
+  end endgenerate
   \$__ABC9_FF_ abc_dff (.D($nextQ), .Q($abc9_currQ));
   \$__ABC9_ASYNC abc_async (.A($abc9_currQ), .S(PRE ^ IS_PRE_INVERTED), .Y(QQ));
 
@@ -220,22 +277,33 @@ module FDPE (output Q, input C, CE, D, PRE);
 endmodule
 module FDPE_1 (output Q, input C, CE, D, PRE);
   parameter [0:0] INIT = 1'b1;
-  wire DD, QQ, $nextQ, $abc9_currQ;
-  generate if (INIT == 1'b1)
-    assign DD = ~D, Q = ~QQ;
-  else
-    assign DD = D, Q = QQ;
-  endgenerate
-  FDPE_1 #(
-    .INIT(1'b0),
-  ) _TECHMAP_REPLACE_ (
-    .D(DD), .Q($nextQ), .C(C), .CE(CE), .PRE(PRE)
-                                          // ^^^ Note that async
-                                          //     control is not directly
-                                          //     supported by abc9 but its
-                                          //     behaviour is captured by
-                                          //     $__ABC9_ASYNC below
-  );
+  wire QQ, $nextQ, $abc9_currQ;
+  generate if (INIT == 1'b1) begin
+    assign Q = ~QQ;
+    FDCE_1 #(
+      .INIT(1'b0)
+    ) _TECHMAP_REPLACE_ (
+      .D(~D), .Q($nextQ), .C(C), .CE(CE), .CLR(PRE)
+                                            // ^^^ Note that async
+                                            //     control is not directly
+                                            //     supported by abc9 but its
+                                            //     behaviour is captured by
+                                            //     $__ABC9_ASYNC below
+    );
+  end
+  else begin
+    assign Q = QQ;
+    FDPE_1 #(
+      .INIT(1'b0)
+    ) _TECHMAP_REPLACE_ (
+      .D(D), .Q($nextQ), .C(C), .CE(CE), .PRE(PRE)
+                                           // ^^^ Note that async
+                                           //     control is not directly
+                                           //     supported by abc9 but its
+                                           //     behaviour is captured by
+                                           //     $__ABC9_ASYNC below
+    );
+  end endgenerate
   \$__ABC9_FF_ abc_dff (.D($nextQ), .Q($abc9_currQ));
   \$__ABC9_ASYNC abc_async (.A($abc9_currQ), .S(PRE), .Y(QQ));
 
@@ -251,20 +319,29 @@ module FDSE (output Q, input C, CE, D, S);
   parameter [0:0] IS_C_INVERTED = 1'b0;
   parameter [0:0] IS_D_INVERTED = 1'b0;
   parameter [0:0] IS_S_INVERTED = 1'b0;
-  wire DD, QQ, $nextQ;
-  generate if (INIT == 1'b1)
-    assign DD = ~D, Q = ~QQ;
-  else
-    assign DD = D, Q = QQ;
-  endgenerate
-  FDSE #(
-    .INIT(1'b0),
-    .IS_C_INVERTED(IS_C_INVERTED),
-    .IS_D_INVERTED(IS_D_INVERTED),
-    .IS_S_INVERTED(IS_S_INVERTED)
-  ) _TECHMAP_REPLACE_ (
-    .D(DD), .Q($nextQ), .C(C), .CE(CE), .S(S)
-  );
+  wire QQ, $nextQ;
+  generate if (INIT == 1'b1) begin
+    assign Q = ~QQ;
+    FDRE #(
+      .INIT(1'b0),
+      .IS_C_INVERTED(IS_C_INVERTED),
+      .IS_D_INVERTED(IS_D_INVERTED),
+      .IS_R_INVERTED(IS_S_INVERTED)
+    ) _TECHMAP_REPLACE_ (
+      .D(~D), .Q($nextQ), .C(C), .CE(CE), .R(S)
+    );
+  end
+  else begin
+    assign Q = QQ;
+    FDSE #(
+      .INIT(1'b0),
+      .IS_C_INVERTED(IS_C_INVERTED),
+      .IS_D_INVERTED(IS_D_INVERTED),
+      .IS_S_INVERTED(IS_S_INVERTED)
+    ) _TECHMAP_REPLACE_ (
+      .D(D), .Q($nextQ), .C(C), .CE(CE), .S(S)
+    );
+  end endgenerate
   \$__ABC9_FF_ abc_dff (.D($nextQ), .Q(QQ));
 
   // Special signals
@@ -275,17 +352,23 @@ module FDSE (output Q, input C, CE, D, S);
 endmodule
 module FDSE_1 (output Q, input C, CE, D, S);
   parameter [0:0] INIT = 1'b1;
-  wire DD, QQ, $nextQ;
-  generate if (INIT == 1'b1)
-    assign DD = ~D, Q = ~QQ;
-  else
-    assign DD = D, Q = QQ;
-  endgenerate
-  FDSE_1 #(
-    .INIT(1'b0),
-  ) _TECHMAP_REPLACE_ (
-    .D(DD), .Q($nextQ), .C(C), .CE(CE), .S(S)
-  );
+  wire QQ, $nextQ;
+  generate if (INIT == 1'b1) begin
+    assign Q = ~QQ;
+    FDRE_1 #(
+      .INIT(1'b0)
+    ) _TECHMAP_REPLACE_ (
+      .D(~D), .Q($nextQ), .C(C), .CE(CE), .R(S)
+    );
+  end
+  else begin
+    assign Q = QQ;
+    FDSE_1 #(
+      .INIT(1'b0)
+    ) _TECHMAP_REPLACE_ (
+      .D(D), .Q($nextQ), .C(C), .CE(CE), .S(S)
+    );
+  end endgenerate
   \$__ABC9_FF_ abc_dff (.D($nextQ), .Q(QQ));
 
   // Special signals

diff --git a/tests/arch/xilinx/abc9_map.ys b/tests/arch/xilinx/abc9_map.ys
new file mode 100644 (file)
index 0000000..6823589
--- /dev/null
+++ b/tests/arch/xilinx/abc9_map.ys
@@ -0,0 +1,91 @@
+read_verilog <<EOT
+module top(input C, CE, D, R, output [1:0] Q);
+FDRE   #(.INIT(1'b1)) ff1 (.C(C), .CE(CE), .D(D), .R(R), .Q(Q[0]));
+FDRE_1 #(.INIT(1'b1)) ff2 (.C(C), .CE(CE), .D(D), .R(R), .Q(Q[1]));
+endmodule
+EOT
+design -save gold
+
+techmap -map +/xilinx/abc9_map.v -max_iter 1
+techmap -map +/xilinx/abc9_unmap.v
+select -assert-count 1 t:FDSE
+select -assert-count 1 t:FDSE_1
+techmap -autoproc -map +/xilinx/cells_sim.v
+design -stash gate
+
+design -import gold -as gold
+design -import gate -as gate
+techmap -autoproc -map +/xilinx/cells_sim.v
+
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -seq 2 -verify -prove-asserts -show-ports miter
+
+design -reset
+read_verilog <<EOT
+module top(input C, CE, D, S, output [1:0] Q);
+FDSE   #(.INIT(1'b1)) ff1 (.C(C), .CE(CE), .D(D), .S(S), .Q(Q[0]));
+FDSE_1 #(.INIT(1'b1)) ff2 (.C(C), .CE(CE), .D(D), .S(S), .Q(Q[1]));
+endmodule
+EOT
+design -save gold
+
+techmap -map +/xilinx/abc9_map.v -max_iter 1
+techmap -map +/xilinx/abc9_unmap.v
+select -assert-count 1 t:FDRE
+select -assert-count 1 t:FDRE_1
+techmap -autoproc -map +/xilinx/cells_sim.v
+design -stash gate
+
+design -import gold -as gold
+design -import gate -as gate
+techmap -autoproc -map +/xilinx/cells_sim.v
+
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -seq 2 -set-init-zero -verify -prove-asserts -show-ports miter
+
+design -reset
+read_verilog <<EOT
+module top(input C, CE, D, PRE, output [1:0] Q);
+FDPE   #(.INIT(1'b1)) ff1 (.C(C), .CE(CE), .D(D), .PRE(PRE), .Q(Q[0]));
+FDPE_1 #(.INIT(1'b1)) ff2 (.C(C), .CE(CE), .D(D), .PRE(PRE), .Q(Q[1]));
+endmodule
+EOT
+design -save gold
+
+techmap -map +/xilinx/abc9_map.v -max_iter 1
+techmap -map +/xilinx/abc9_unmap.v
+select -assert-count 1 t:FDCE
+select -assert-count 1 t:FDCE_1
+techmap -autoproc -map +/xilinx/cells_sim.v
+design -stash gate
+
+design -import gold -as gold
+design -import gate -as gate
+techmap -autoproc -map +/xilinx/cells_sim.v
+clk2fflogic
+
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -seq 2 -set-init-zero -verify -prove-asserts -show-ports miter
+
+design -reset
+read_verilog <<EOT
+module top(input C, CE, D, CLR, output [1:0] Q);
+FDCE   #(.INIT(1'b1)) ff1 (.C(C), .CE(CE), .D(D), .CLR(CLR), .Q(Q[0]));
+FDCE_1 #(.INIT(1'b1)) ff2 (.C(C), .CE(CE), .D(D), .CLR(CLR), .Q(Q[1]));
+endmodule
+EOT
+design -save gold
+
+techmap -map +/xilinx/abc9_map.v -max_iter 1
+techmap -map +/xilinx/abc9_unmap.v
+select -assert-count 1 t:FDPE
+techmap -autoproc -map +/xilinx/cells_sim.v
+design -stash gate
+
+design -import gold -as gold
+design -import gate -as gate
+techmap -autoproc -map +/xilinx/cells_sim.v
+clk2fflogic
+
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -seq 2 -set-init-zero -verify -prove-asserts -show-ports miter