Merge pull request #1505 from YosysHQ/eddie/xaig_dff_adff

xaig_dff to support async flops $_DFF_[NP][NP][01]_

5 files changed, 53 insertions, 13 deletions

diff --git a/backends/aiger/xaiger.cc b/backends/aiger/xaiger.cc
index 03246a9b5..5d125b653 100644
--- a/backends/aiger/xaiger.cc
+++ b/backends/aiger/xaiger.cc
@@ -863,7 +863,8 @@ struct XAigerWriter
 				dict<SigSig, SigSig> replace;
 				for (auto it = holes_module->cells_.begin(); it != holes_module->cells_.end(); ) {
 					auto cell = it->second;
-					if (cell->type.in("$_DFF_N_", "$_DFF_P_")) {
+					if (cell->type.in("$_DFF_N_", "$_DFF_NN0_", "$_DFF_NN1_", "$_DFF_NP0_", "$_DFF_NP1_",
+											"$_DFF_P_", "$_DFF_PN0_", "$_DFF_PN1", "$_DFF_PP0_", "$_DFF_PP1_")) {
 						SigBit D = cell->getPort("\\D");
 						SigBit Q = cell->getPort("\\Q");
 						// Remove the DFF cell from what needs to be a combinatorial box
diff --git a/techlibs/xilinx/abc9_map.v b/techlibs/xilinx/abc9_map.v
index d2c0abeb6..9913b229f 100644
--- a/techlibs/xilinx/abc9_map.v
+++ b/techlibs/xilinx/abc9_map.v
@@ -120,10 +120,11 @@ module FDCE (output reg Q, input C, CE, D, CLR);
     .IS_D_INVERTED(IS_D_INVERTED),
     .IS_CLR_INVERTED(IS_CLR_INVERTED)
   ) _TECHMAP_REPLACE_ (
-    .D(D), .Q($nextQ),  .C(C), .CE(CE), .CLR(IS_CLR_INVERTED)
+    .D(D), .Q($nextQ),  .C(C), .CE(CE), .CLR(CLR)
                                          // ^^^ Note that async
-                                         //     control is disabled
-                                         //     here but captured by
+                                         //     control is not directly
+                                         //     supported by abc9 but its
+                                         //     behaviour is captured by
                                          //     $__ABC9_ASYNC below
   );
   \$__ABC9_FF_ abc_dff (.D($nextQ), .Q($abc9_currQ));
@@ -142,10 +143,11 @@ module FDCE_1 (output reg Q, input C, CE, D, CLR);
   FDCE_1 #(
     .INIT(INIT)
   ) _TECHMAP_REPLACE_ (
-    .D(D), .Q($nextQ), .C(C), .CE(CE), .CLR(1'b0)
+    .D(D), .Q($nextQ), .C(C), .CE(CE), .CLR(CLR)
                                          // ^^^ Note that async
-                                         //     control is disabled
-                                         //     here but captured by
+                                         //     control is not directly
+                                         //     supported by abc9 but its
+                                         //     behaviour is captured by
                                          //     $__ABC9_ASYNC below
   );
   \$__ABC9_FF_ abc_dff (.D($nextQ), .Q($abc9_currQ));
@@ -169,10 +171,11 @@ module FDPE (output reg Q, input C, CE, D, PRE);
     .IS_D_INVERTED(IS_D_INVERTED),
     .IS_PRE_INVERTED(IS_PRE_INVERTED),
   ) _TECHMAP_REPLACE_ (
-    .D(D), .Q($nextQ), .C(C), .CE(CE), .PRE(IS_PRE_INVERTED)
+    .D(D), .Q($nextQ), .C(C), .CE(CE), .PRE(PRE)
                                          // ^^^ Note that async
-                                         //     control is disabled
-                                         //     here but captured by
+                                         //     control is not directly
+                                         //     supported by abc9 but its
+                                         //     behaviour is captured by
                                          //     $__ABC9_ASYNC below
   );
   \$__ABC9_FF_ abc_dff (.D($nextQ), .Q($abc9_currQ));
@@ -189,10 +192,11 @@ module FDPE_1 (output reg Q, input C, CE, D, PRE);
   FDPE_1 #(
     .INIT(INIT)
   ) _TECHMAP_REPLACE_ (
-    .D(D), .Q($nextQ), .C(C), .CE(CE), .PRE(1'b0)
+    .D(D), .Q($nextQ), .C(C), .CE(CE), .PRE(PRE)
                                          // ^^^ Note that async
-                                         //     control is disabled
-                                         //     here but captured by
+                                         //     control is not directly
+                                         //     supported by abc9 but its
+                                         //     behaviour is captured by
                                          //     $__ABC9_ASYNC below
   );
   \$__ABC9_FF_ abc_dff (.D($nextQ), .Q($abc9_currQ));
diff --git a/tests/simple_abc9/abc9.v b/tests/simple_abc9/abc9.v
index 1844bac20..65eb01338 100644
--- a/tests/simple_abc9/abc9.v
+++ b/tests/simple_abc9/abc9.v
@@ -272,3 +272,15 @@ module abc9_test029(input clk1, clk2, input d, output reg q1, q2);
 always @(posedge clk1) q1 <= d;
 always @(negedge clk2) q2 <= q1;
 endmodule
+
+module abc9_test030(input clk, d, r, output reg q);
+always @(posedge clk or posedge r)
+    if (r) q <= 1'b0;
+    else q <= d;
+endmodule
+
+module abc9_test031(input clk, d, r, output reg q);
+always @(negedge clk or posedge r)
+    if (r) q <= 1'b1;
+    else q <= d;
+endmodule
diff --git a/tests/various/abc9.v b/tests/various/abc9.v
index 30ebd4e26..f0b3f6837 100644
--- a/tests/various/abc9.v
+++ b/tests/various/abc9.v
@@ -9,3 +9,10 @@ wire w;
 unknown u(~i, w);
 unknown2 u2(w, o);
 endmodule
+
+module abc9_test032(input clk, d, r, output reg q);
+initial q = 1'b0;
+always @(negedge clk or negedge r)
+    if (!r) q <= 1'b0;
+    else q <= d;
+endmodule
diff --git a/tests/various/abc9.ys b/tests/various/abc9.ys
index 5c9a4075d..81d0afd1b 100644
--- a/tests/various/abc9.ys
+++ b/tests/various/abc9.ys
@@ -22,3 +22,19 @@ abc9 -lut 4
 select -assert-count 1 t:$lut r:LUT=2'b01 r:WIDTH=1 %i %i
 select -assert-count 1 t:unknown
 select -assert-none t:$lut t:unknown %% t: %D
+
+design -load read
+hierarchy -top abc9_test032
+proc
+clk2fflogic
+design -save gold
+
+abc9 -lut 4
+check
+design -stash gate
+
+design -import gold -as gold
+design -import gate -as gate
+
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -seq 10 -verify -prove-asserts -show-ports miter