Merge remote-tracking branch 'origin/master' into eddie/abc9_mfs

6 files changed, 645 insertions, 155 deletions

diff --git a/techlibs/xilinx/abc9_map.v b/techlibs/xilinx/abc9_map.v
index cbe2a8cef..0652064cb 100644
--- a/techlibs/xilinx/abc9_map.v
+++ b/techlibs/xilinx/abc9_map.v
@@ -18,8 +18,366 @@
  *
  */
 
-// ============================================================================
+// The following techmapping rules are intended to be run (with -max_iter 1)
+//   before invoking the `abc9` pass in order to transform the design into
+//   a format that it understands.
 
+`ifdef DFF_MODE
+// For example, (complex) flip-flops are expected to be described as an
+//   combinatorial box (containing all control logic such as clock enable
+//   or synchronous resets) followed by a basic D-Q flop.
+// Yosys will automatically analyse the simulation model (described in
+//   cells_sim.v) and detach any $_DFF_P_ or $_DFF_N_ cells present in
+//   order to extract the combinatorial control logic left behind.
+//   Specifically, a simulation model similar to the one below:
+//
+//                ++===================================++
+//                ||                        Sim model  ||
+//                ||      /\/\/\/\                     ||
+//            D -->>-----<        >     +------+       ||
+//            R -->>-----<  Comb. >     |$_DFF_|       ||
+//           CE -->>-----<  logic >-----| [NP]_|---+---->>-- Q
+//                ||  +--<        >     +------+   |   ||
+//                ||  |   \/\/\/\/                 |   ||
+//                ||  |                            |   ||
+//                ||  +----------------------------+   ||
+//                ||                                   ||
+//                ++===================================++
+//
+//   is transformed into:
+//
+//                ++==================++
+//                ||         Comb box ||
+//                ||                  ||
+//                ||      /\/\/\/\    ||
+//           D  -->>-----<        >   ||
+//           R  -->>-----<  Comb. >   ||        +-----------+
+//          CE  -->>-----<  logic >--->>-- $Q --|$__ABC9_FF_|--+-->> Q
+//   abc9_ff.Q +-->>-----<        >   ||        +-----------+  |
+//             |  ||      \/\/\/\/    ||                       |
+//             |  ||                  ||                       |
+//             |  ++==================++                       |
+//             |                                               |
+//             +-----------------------------------------------+
+//
+// The purpose of the following FD* rules are to wrap the flop with:
+// (a) a special $__ABC9_FF_ in front of the FD*'s output, indicating to abc9
+//     the connectivity of its basic D-Q flop
+// (b) an optional $__ABC9_ASYNC_ cell in front of $__ABC_FF_'s output to
+//     capture asynchronous behaviour
+// (c) a special abc9_ff.clock wire to capture its clock domain and polarity
+//     (indicated to `abc9' so that it only performs sequential synthesis
+//     (with reachability analysis) correctly on one domain at a time)
+// (d) a special abc9_ff.init wire to encode the flop's initial state
+//     NOTE: in order to perform sequential synthesis, `abc9' also requires
+//     that the initial value of all flops be zero
+// (e) a special _TECHMAP_REPLACE_.abc9_ff.Q wire that will be used for feedback
+//     into the (combinatorial) FD* cell to facilitate clock-enable behaviour
+
+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 QQ, $Q;
+  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($Q), .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($Q), .C(C), .CE(CE), .R(R)
+    );
+  end
+  endgenerate
+  $__ABC9_FF_ abc9_ff (.D($Q), .Q(QQ));
+
+  // Special signals
+  wire [1:0] abc9_ff.clock = {C, IS_C_INVERTED};
+  wire [0:0] abc9_ff.init = 1'b0;
+  wire [0:0] _TECHMAP_REPLACE_.abc9_ff.Q = QQ;
+endmodule
+module FDRE_1 (output Q, input C, CE, D, R);
+  parameter [0:0] INIT = 1'b0;
+  wire QQ, $Q;
+  generate if (INIT == 1'b1) begin
+    assign Q = ~QQ;
+    FDSE_1 #(
+      .INIT(1'b0)
+    ) _TECHMAP_REPLACE_ (
+      .D(~D), .Q($Q), .C(C), .CE(CE), .S(R)
+    );
+  end
+  else begin
+    assign Q = QQ;
+    FDRE_1 #(
+      .INIT(1'b0)
+    ) _TECHMAP_REPLACE_ (
+      .D(D), .Q($Q), .C(C), .CE(CE), .R(R)
+    );
+  end
+  endgenerate
+  $__ABC9_FF_ abc9_ff (.D($Q), .Q(QQ));
+
+  // Special signals
+  wire [1:0] abc9_ff.clock = {C, 1'b1 /* IS_C_INVERTED */};
+  wire [0:0] abc9_ff.init = 1'b0;
+  wire [0:0] _TECHMAP_REPLACE_.abc9_ff.Q = QQ;
+endmodule
+
+module FDSE (output Q, input C, CE, D, S);
+  parameter [0:0] INIT = 1'b1;
+  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 QQ, $Q;
+  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($Q), .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($Q), .C(C), .CE(CE), .S(S)
+    );
+  end endgenerate
+  $__ABC9_FF_ abc9_ff (.D($Q), .Q(QQ));
+
+  // Special signals
+  wire [1:0] abc9_ff.clock = {C, IS_C_INVERTED};
+  wire [0:0] abc9_ff.init = 1'b0;
+  wire [0:0] _TECHMAP_REPLACE_.abc9_ff.Q = QQ;
+endmodule
+module FDSE_1 (output Q, input C, CE, D, S);
+  parameter [0:0] INIT = 1'b1;
+  wire QQ, $Q;
+  generate if (INIT == 1'b1) begin
+    assign Q = ~QQ;
+    FDRE_1 #(
+      .INIT(1'b0)
+    ) _TECHMAP_REPLACE_ (
+      .D(~D), .Q($Q), .C(C), .CE(CE), .R(S)
+    );
+  end
+  else begin
+    assign Q = QQ;
+    FDSE_1 #(
+      .INIT(1'b0)
+    ) _TECHMAP_REPLACE_ (
+      .D(D), .Q($Q), .C(C), .CE(CE), .S(S)
+    );
+  end endgenerate
+  $__ABC9_FF_ abc9_ff (.D($Q), .Q(QQ));
+
+  // Special signals
+  wire [1:0] abc9_ff.clock = {C, 1'b1 /* IS_C_INVERTED */};
+  wire [0:0] abc9_ff.init = 1'b0;
+  wire [0:0] _TECHMAP_REPLACE_.abc9_ff.Q = QQ;
+endmodule
+
+module FDCE (output Q, input C, CE, D, CLR);
+  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_CLR_INVERTED = 1'b0;
+  wire QQ, $Q, $QQ;
+  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($Q), .C(C), .CE(CE), .PRE(CLR)
+                                            // ^^^ Note that async
+                                            //     control is not directly
+                                            //     supported by abc9 but its
+                                            //     behaviour is captured by
+                                            //     $__ABC9_ASYNC1 below
+    );
+    // Since this is an async flop, async behaviour is dealt with here
+    $__ABC9_ASYNC1 abc_async (.A($QQ), .S(CLR ^ IS_CLR_INVERTED), .Y(QQ));
+  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($Q), .C(C), .CE(CE), .CLR(CLR)
+                                           // ^^^ Note that async
+                                           //     control is not directly
+                                           //     supported by abc9 but its
+                                           //     behaviour is captured by
+                                           //     $__ABC9_ASYNC0 below
+    );
+    // Since this is an async flop, async behaviour is dealt with here
+    $__ABC9_ASYNC0 abc_async (.A($QQ), .S(CLR ^ IS_CLR_INVERTED), .Y(QQ));
+  end endgenerate
+  $__ABC9_FF_ abc9_ff (.D($Q), .Q($QQ));
+
+  // Special signals
+  wire [1:0] abc9_ff.clock = {C, IS_C_INVERTED};
+  wire [0:0] abc9_ff.init = 1'b0;
+  wire [0:0] _TECHMAP_REPLACE_.abc9_ff.Q = $QQ;
+endmodule
+module FDCE_1 (output Q, input C, CE, D, CLR);
+  parameter [0:0] INIT = 1'b0;
+  wire QQ, $Q, $QQ;
+  generate if (INIT == 1'b1) begin
+    assign Q = ~QQ;
+    FDPE_1 #(
+      .INIT(1'b0)
+    ) _TECHMAP_REPLACE_ (
+      .D(~D), .Q($Q), .C(C), .CE(CE), .PRE(CLR)
+                                            // ^^^ Note that async
+                                            //     control is not directly
+                                            //     supported by abc9 but its
+                                            //     behaviour is captured by
+                                            //     $__ABC9_ASYNC1 below
+    );
+    $__ABC9_ASYNC1 abc_async (.A($QQ), .S(CLR), .Y(QQ));
+  end
+  else begin
+    assign Q = QQ;
+    FDCE_1 #(
+      .INIT(1'b0)
+    ) _TECHMAP_REPLACE_ (
+      .D(D), .Q($Q), .C(C), .CE(CE), .CLR(CLR)
+                                           // ^^^ Note that async
+                                           //     control is not directly
+                                           //     supported by abc9 but its
+                                           //     behaviour is captured by
+                                           //     $__ABC9_ASYNC0 below
+    );
+    $__ABC9_ASYNC0 abc_async (.A($QQ), .S(CLR), .Y(QQ));
+  end endgenerate
+  $__ABC9_FF_ abc9_ff (.D($Q), .Q($QQ));
+
+  // Special signals
+  wire [1:0] abc9_ff.clock = {C, 1'b1 /* IS_C_INVERTED */};
+  wire [0:0] abc9_ff.init = 1'b0;
+  wire [0:0] _TECHMAP_REPLACE_.abc9_ff.Q = $QQ;
+endmodule
+
+module FDPE (output Q, input C, CE, D, PRE);
+  parameter [0:0] INIT = 1'b1;
+  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 QQ, $Q, $QQ;
+  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($Q), .C(C), .CE(CE), .CLR(PRE)
+                                            // ^^^ Note that async
+                                            //     control is not directly
+                                            //     supported by abc9 but its
+                                            //     behaviour is captured by
+                                            //     $__ABC9_ASYNC0 below
+    );
+    $__ABC9_ASYNC0 abc_async (.A($QQ), .S(PRE ^ IS_PRE_INVERTED), .Y(QQ));
+  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($Q), .C(C), .CE(CE), .PRE(PRE)
+                                           // ^^^ Note that async
+                                           //     control is not directly
+                                           //     supported by abc9 but its
+                                           //     behaviour is captured by
+                                           //     $__ABC9_ASYNC1 below
+    );
+    $__ABC9_ASYNC1 abc_async (.A($QQ), .S(PRE ^ IS_PRE_INVERTED), .Y(QQ));
+  end endgenerate
+  $__ABC9_FF_ abc9_ff (.D($Q), .Q($QQ));
+
+  // Special signals
+  wire [1:0] abc9_ff.clock = {C, IS_C_INVERTED};
+  wire [0:0] abc9_ff.init = 1'b0;
+  wire [0:0] _TECHMAP_REPLACE_.abc9_ff.Q = $QQ;
+endmodule
+module FDPE_1 (output Q, input C, CE, D, PRE);
+  parameter [0:0] INIT = 1'b1;
+  wire QQ, $Q, $QQ;
+  generate if (INIT == 1'b1) begin
+    assign Q = ~QQ;
+    FDCE_1 #(
+      .INIT(1'b0)
+    ) _TECHMAP_REPLACE_ (
+      .D(~D), .Q($Q), .C(C), .CE(CE), .CLR(PRE)
+                                            // ^^^ Note that async
+                                            //     control is not directly
+                                            //     supported by abc9 but its
+                                            //     behaviour is captured by
+                                            //     $__ABC9_ASYNC0 below
+    );
+    $__ABC9_ASYNC0 abc_async (.A($QQ), .S(PRE), .Y(QQ));
+  end
+  else begin
+    assign Q = QQ;
+    FDPE_1 #(
+      .INIT(1'b0)
+    ) _TECHMAP_REPLACE_ (
+      .D(D), .Q($Q), .C(C), .CE(CE), .PRE(PRE)
+                                           // ^^^ Note that async
+                                           //     control is not directly
+                                           //     supported by abc9 but its
+                                           //     behaviour is captured by
+                                           //     $__ABC9_ASYNC1 below
+    );
+    $__ABC9_ASYNC1 abc_async (.A($QQ), .S(PRE), .Y(QQ));
+  end endgenerate
+  $__ABC9_FF_ abc9_ff (.D($Q), .Q($QQ));
+
+  // Special signals
+  wire [1:0] abc9_ff.clock = {C, 1'b1 /* IS_C_INVERTED */};
+  wire [0:0] abc9_ff.init = 1'b0;
+  wire [0:0] _TECHMAP_REPLACE_.abc9_ff.Q = $QQ;
+endmodule
+`endif
+
+// Attach a (combinatorial) black-box onto the output
+//   of thes LUTRAM primitives to capture their
+//   asynchronous read behaviour
 module RAM32X1D (
   output DPO, SPO,
   (* techmap_autopurge *) input  D,
@@ -30,17 +388,17 @@ module RAM32X1D (
 );
   parameter INIT = 32'h0;
   parameter IS_WCLK_INVERTED = 1'b0;
-  wire \$DPO , \$SPO ;
+  wire $DPO, $SPO;
   RAM32X1D #(
     .INIT(INIT), .IS_WCLK_INVERTED(IS_WCLK_INVERTED)
   ) _TECHMAP_REPLACE_ (
-    .DPO(\$DPO ), .SPO(\$SPO ),
+    .DPO($DPO), .SPO($SPO),
     .D(D), .WCLK(WCLK), .WE(WE),
     .A0(A0), .A1(A1), .A2(A2), .A3(A3), .A4(A4),
     .DPRA0(DPRA0), .DPRA1(DPRA1), .DPRA2(DPRA2), .DPRA3(DPRA3), .DPRA4(DPRA4)
   );
-  \$__ABC9_LUT6 spo (.A(\$SPO ), .S({1'b1, A4, A3, A2, A1, A0}), .Y(SPO));
-  \$__ABC9_LUT6 dpo (.A(\$DPO ), .S({1'b1, DPRA4, DPRA3, DPRA2, DPRA1, DPRA0}), .Y(DPO));
+  $__ABC9_LUT6 spo (.A($SPO), .S({1'b1, A4, A3, A2, A1, A0}), .Y(SPO));
+  $__ABC9_LUT6 dpo (.A($DPO), .S({1'b1, DPRA4, DPRA3, DPRA2, DPRA1, DPRA0}), .Y(DPO));
 endmodule
 
 module RAM64X1D (
@@ -53,17 +411,17 @@ module RAM64X1D (
 );
   parameter INIT = 64'h0;
   parameter IS_WCLK_INVERTED = 1'b0;
-  wire \$DPO , \$SPO ;
+  wire $DPO, $SPO;
   RAM64X1D #(
     .INIT(INIT), .IS_WCLK_INVERTED(IS_WCLK_INVERTED)
   ) _TECHMAP_REPLACE_ (
-    .DPO(\$DPO ), .SPO(\$SPO ),
+    .DPO($DPO), .SPO($SPO),
     .D(D), .WCLK(WCLK), .WE(WE),
     .A0(A0), .A1(A1), .A2(A2), .A3(A3), .A4(A4), .A5(A5),
     .DPRA0(DPRA0), .DPRA1(DPRA1), .DPRA2(DPRA2), .DPRA3(DPRA3), .DPRA4(DPRA4), .DPRA5(DPRA5)
   );
-  \$__ABC9_LUT6 spo (.A(\$SPO ), .S({A5, A4, A3, A2, A1, A0}), .Y(SPO));
-  \$__ABC9_LUT6 dpo (.A(\$DPO ), .S({DPRA5, DPRA4, DPRA3, DPRA2, DPRA1, DPRA0}), .Y(DPO));
+  $__ABC9_LUT6 spo (.A($SPO), .S({A5, A4, A3, A2, A1, A0}), .Y(SPO));
+  $__ABC9_LUT6 dpo (.A($DPO), .S({DPRA5, DPRA4, DPRA3, DPRA2, DPRA1, DPRA0}), .Y(DPO));
 endmodule
 
 module RAM128X1D (
@@ -75,17 +433,17 @@ module RAM128X1D (
 );
   parameter INIT = 128'h0;
   parameter IS_WCLK_INVERTED = 1'b0;
-  wire \$DPO , \$SPO ;
+  wire $DPO, $SPO;
   RAM128X1D #(
     .INIT(INIT), .IS_WCLK_INVERTED(IS_WCLK_INVERTED)
   ) _TECHMAP_REPLACE_ (
-    .DPO(\$DPO ), .SPO(\$SPO ),
+    .DPO($DPO), .SPO($SPO),
     .D(D), .WCLK(WCLK), .WE(WE),
     .A(A),
     .DPRA(DPRA)
   );
-  \$__ABC9_LUT7 spo (.A(\$SPO ), .S(A), .Y(SPO));
-  \$__ABC9_LUT7 dpo (.A(\$DPO ), .S(DPRA), .Y(DPO));
+  $__ABC9_LUT7 spo (.A($SPO), .S(A), .Y(SPO));
+  $__ABC9_LUT7 dpo (.A($DPO), .S(DPRA), .Y(DPO));
 endmodule
 
 module RAM32M (
@@ -109,24 +467,24 @@ module RAM32M (
   parameter [63:0] INIT_C = 64'h0000000000000000;
   parameter [63:0] INIT_D = 64'h0000000000000000;
   parameter [0:0] IS_WCLK_INVERTED = 1'b0;
-  wire [1:0] \$DOA , \$DOB , \$DOC , \$DOD ;
+  wire [1:0] $DOA, $DOB, $DOC, $DOD;
   RAM32M #(
     .INIT_A(INIT_A), .INIT_B(INIT_B), .INIT_C(INIT_C), .INIT_D(INIT_D),
     .IS_WCLK_INVERTED(IS_WCLK_INVERTED)
   ) _TECHMAP_REPLACE_ (
-    .DOA(\$DOA ), .DOB(\$DOB ), .DOC(\$DOC ), .DOD(\$DOD ),
+    .DOA($DOA), .DOB($DOB), .DOC($DOC), .DOD($DOD),
     .WCLK(WCLK), .WE(WE),
     .ADDRA(ADDRA), .ADDRB(ADDRB), .ADDRC(ADDRC), .ADDRD(ADDRD),
     .DIA(DIA), .DIB(DIB), .DIC(DIC), .DID(DID)
   );
-  \$__ABC9_LUT6 doa0 (.A(\$DOA [0]), .S({1'b1, ADDRA}), .Y(DOA[0]));
-  \$__ABC9_LUT6 doa1 (.A(\$DOA [1]), .S({1'b1, ADDRA}), .Y(DOA[1]));
-  \$__ABC9_LUT6 dob0 (.A(\$DOB [0]), .S({1'b1, ADDRB}), .Y(DOB[0]));
-  \$__ABC9_LUT6 dob1 (.A(\$DOB [1]), .S({1'b1, ADDRB}), .Y(DOB[1]));
-  \$__ABC9_LUT6 doc0 (.A(\$DOC [0]), .S({1'b1, ADDRC}), .Y(DOC[0]));
-  \$__ABC9_LUT6 doc1 (.A(\$DOC [1]), .S({1'b1, ADDRC}), .Y(DOC[1]));
-  \$__ABC9_LUT6 dod0 (.A(\$DOD [0]), .S({1'b1, ADDRD}), .Y(DOD[0]));
-  \$__ABC9_LUT6 dod1 (.A(\$DOD [1]), .S({1'b1, ADDRD}), .Y(DOD[1]));
+  $__ABC9_LUT6 doa0 (.A($DOA[0]), .S({1'b1, ADDRA}), .Y(DOA[0]));
+  $__ABC9_LUT6 doa1 (.A($DOA[1]), .S({1'b1, ADDRA}), .Y(DOA[1]));
+  $__ABC9_LUT6 dob0 (.A($DOB[0]), .S({1'b1, ADDRB}), .Y(DOB[0]));
+  $__ABC9_LUT6 dob1 (.A($DOB[1]), .S({1'b1, ADDRB}), .Y(DOB[1]));
+  $__ABC9_LUT6 doc0 (.A($DOC[0]), .S({1'b1, ADDRC}), .Y(DOC[0]));
+  $__ABC9_LUT6 doc1 (.A($DOC[1]), .S({1'b1, ADDRC}), .Y(DOC[1]));
+  $__ABC9_LUT6 dod0 (.A($DOD[0]), .S({1'b1, ADDRD}), .Y(DOD[0]));
+  $__ABC9_LUT6 dod1 (.A($DOD[1]), .S({1'b1, ADDRD}), .Y(DOD[1]));
 endmodule
 
 module RAM64M (
@@ -150,20 +508,20 @@ module RAM64M (
   parameter [63:0] INIT_C = 64'h0000000000000000;
   parameter [63:0] INIT_D = 64'h0000000000000000;
   parameter [0:0] IS_WCLK_INVERTED = 1'b0;
-  wire \$DOA , \$DOB , \$DOC , \$DOD ;
+  wire $DOA, $DOB, $DOC, $DOD;
   RAM64M #(
     .INIT_A(INIT_A), .INIT_B(INIT_B), .INIT_C(INIT_C), .INIT_D(INIT_D),
     .IS_WCLK_INVERTED(IS_WCLK_INVERTED)
   ) _TECHMAP_REPLACE_ (
-    .DOA(\$DOA ), .DOB(\$DOB ), .DOC(\$DOC ), .DOD(\$DOD ),
+    .DOA($DOA), .DOB($DOB), .DOC($DOC), .DOD($DOD),
     .WCLK(WCLK), .WE(WE),
     .ADDRA(ADDRA), .ADDRB(ADDRB), .ADDRC(ADDRC), .ADDRD(ADDRD),
     .DIA(DIA), .DIB(DIB), .DIC(DIC), .DID(DID)
   );
-  \$__ABC9_LUT6 doa (.A(\$DOA ), .S(ADDRA), .Y(DOA));
-  \$__ABC9_LUT6 dob (.A(\$DOB ), .S(ADDRB), .Y(DOB));
-  \$__ABC9_LUT6 doc (.A(\$DOC ), .S(ADDRC), .Y(DOC));
-  \$__ABC9_LUT6 dod (.A(\$DOD ), .S(ADDRD), .Y(DOD));
+  $__ABC9_LUT6 doa (.A($DOA), .S(ADDRA), .Y(DOA));
+  $__ABC9_LUT6 dob (.A($DOB), .S(ADDRB), .Y(DOB));
+  $__ABC9_LUT6 doc (.A($DOC), .S(ADDRC), .Y(DOC));
+  $__ABC9_LUT6 dod (.A($DOD), .S(ADDRD), .Y(DOD));
 endmodule
 
 module SRL16E (
@@ -172,14 +530,14 @@ module SRL16E (
 );
   parameter [15:0] INIT = 16'h0000;
   parameter [0:0] IS_CLK_INVERTED = 1'b0;
-  wire \$Q ;
+  wire $Q;
   SRL16E #(
     .INIT(INIT), .IS_CLK_INVERTED(IS_CLK_INVERTED)
   ) _TECHMAP_REPLACE_ (
-    .Q(\$Q ),
+    .Q($Q),
     .A0(A0), .A1(A1), .A2(A2), .A3(A3), .CE(CE), .CLK(CLK), .D(D)
   );
-  \$__ABC9_LUT6 q (.A(\$Q ), .S({1'b1, A3, A2, A1, A0, 1'b1}), .Y(Q));
+  $__ABC9_LUT6 q (.A($Q), .S({1'b1, A3, A2, A1, A0, 1'b1}), .Y(Q));
 endmodule
 
 module SRLC32E (
@@ -190,14 +548,14 @@ module SRLC32E (
 );
   parameter [31:0] INIT = 32'h00000000;
   parameter [0:0] IS_CLK_INVERTED = 1'b0;
-  wire \$Q ;
+  wire $Q;
   SRLC32E #(
     .INIT(INIT), .IS_CLK_INVERTED(IS_CLK_INVERTED)
   ) _TECHMAP_REPLACE_ (
-    .Q(\$Q ), .Q31(Q31),
+    .Q($Q), .Q31(Q31),
     .A(A), .CE(CE), .CLK(CLK), .D(D)
   );
-  \$__ABC9_LUT6 q (.A(\$Q ), .S({1'b1, A}), .Y(Q));
+  $__ABC9_LUT6 q (.A($Q), .S({1'b1, A}), .Y(Q));
 endmodule
 
 module DSP48E1 (
diff --git a/techlibs/xilinx/abc9_model.v b/techlibs/xilinx/abc9_model.v
index 18d59dcd6..204fa883f 100644
--- a/techlibs/xilinx/abc9_model.v
+++ b/techlibs/xilinx/abc9_model.v
@@ -30,7 +30,22 @@ module \$__XILINX_MUXF78 (output O, input I0, I1, I2, I3, S0, S1);
                 : (S0 ? I1 : I0);
 endmodule
 
-// Box to emulate comb/seq behaviour of RAMD{32,64} and SRL{16,32}
+module \$__ABC9_FF_ (input D, output Q);
+endmodule
+
+// Box to emulate async behaviour of FDC*
+(* abc9_box_id = 1000, lib_whitebox *)
+module \$__ABC9_ASYNC0 (input A, S, output Y);
+  assign Y = S ? 1'b0 : A;
+endmodule
+
+// Box to emulate async behaviour of FDP*
+(* abc9_box_id = 1001, lib_whitebox *)
+module \$__ABC9_ASYNC1 (input A, S, output Y);
+  assign Y = S ? 1'b0 : A;
+endmodule
+
+// Box to emulate comb/seq behaviour of RAM{32,64} and SRL{16,32}
 //   Necessary since RAMD* and SRL* have both combinatorial (i.e.
 //   same-cycle read operation) and sequential (write operation
 //   is only committed on the next clock edge).
@@ -39,7 +54,7 @@ endmodule
 (* abc9_box_id=2000 *)
 module \$__ABC9_LUT6 (input A, input [5:0] S, output Y);
 endmodule
-// Box to emulate comb/seq behaviour of RAMD128
+// Box to emulate comb/seq behaviour of RAM128
 (* abc9_box_id=2001 *)
 module \$__ABC9_LUT7 (input A, input [6:0] S, output Y);
 endmodule
diff --git a/techlibs/xilinx/abc9_unmap.v b/techlibs/xilinx/abc9_unmap.v
index 64135e9a7..f2342ce62 100644
--- a/techlibs/xilinx/abc9_unmap.v
+++ b/techlibs/xilinx/abc9_unmap.v
@@ -20,6 +20,15 @@
 
 // ============================================================================
 
+(* techmap_celltype = "$__ABC9_ASYNC0 $__ABC9_ASYNC1" *)
+module $__ABC9_ASYNC01(input A, S, output Y);
+  assign Y = A;
+endmodule
+
+module $__ABC9_FF_(input D, output Q);
+  assign Q = D;
+endmodule
+
 module $__ABC9_LUT6(input A, input [5:0] S, output Y);
   assign Y = A;
 endmodule
diff --git a/techlibs/xilinx/abc9_xc7.box b/techlibs/xilinx/abc9_xc7.box
index 9fb1cc0ef..64170546c 100644
--- a/techlibs/xilinx/abc9_xc7.box
+++ b/techlibs/xilinx/abc9_xc7.box
@@ -1,64 +1,142 @@
 # Max delays from https://github.com/SymbiFlow/prjxray-db/blob/34ea6eb08a63d21ec16264ad37a0a7b142ff6031/artix7/timings/CLBLL_L.sdf
 #                 https://github.com/SymbiFlow/prjxray-db/blob/23c8b0851f979f0799318eaca90174413a46b257/artix7/timings/slicel.sdf
 
-# NB: Inputs/Outputs must be ordered alphabetically
-#     (with exceptions for carry in/out)
+# NB: Box inputs/outputs must each be in the same order
+#     as their corresponding module definition
+#     (with exceptions detailed below)
 
-# Average across F7[AB]MUX
-# Inputs: I0 I1 S0
-# Outputs: O
-MUXF7 1 1 3 1
-204 208 286
+# Box 1 : MUXF7
+#   Max delays from: https://github.com/SymbiFlow/prjxray-db/blob/34ea6eb08a63d21ec16264ad37a0a7b142ff6031/artix7/timings/CLBLL_L.sdf#L451-L453
+# name ID w/b ins outs
+MUXF7  1  1   3   1
+#I0 I1  S0
+204 208 286 # O
 
-# Inputs: I0 I1 S0
-# Outputs: O
-MUXF8 2 1 3 1
-104 94 273
+# Box 2 : MUXF8
+#   Max delays from: https://github.com/SymbiFlow/prjxray-db/blob/34ea6eb08a63d21ec16264ad37a0a7b142ff6031/artix7/timings/CLBLL_L.sdf#L462-L464
+# name ID w/b ins outs
+MUXF8  2  1   3   1
+#I0 I1 S0
+104 94 273 # O
 
-# Box containing MUXF7.[AB] + MUXF8,
-#   Necessary to make these an atomic unit so that
-#   ABC cannot optimise just one of the MUXF7 away
-#   and expect to save on its delay
-# Inputs: I0 I1 I2 I3 S0 S1
-# Outputs: O
-$__MUXF78 3 1 6 1
-294 297 311 317 390 273
+# Box 3 : $__MUXF78
+#         (private cell used to preserve 2xMUXF7 + 1xMUXF8
+#          an atomic unit so that ABC cannot optimise just
+#          one of the MUXF7 away and expect to save on its
+#          delay, since MUXF8 is only reachable through an
+#          MUXF7)
+# name    ID w/b ins outs
+$__MUXF78 3  1   6   1
+#I0 I1  I2  I3  S0  S1
+294 297 311 317 390 273 # O
 
-# CARRY4 + CARRY4_[ABCD]X
-# Inputs: CYINIT DI0 DI1 DI2 DI3 S0 S1 S2 S3 CI
-# Outputs:  O0 O1 O2 O3 CO0 CO1 CO2 CO3
-#   (NB: carry chain input/output must be last
-#        input/output and the entire bus has been
+# Box 4 : CARRY4 + CARRY4_[ABCD]X
+#   (Exception: carry chain input/output must be the
+#        last input and output and the entire bus has been
 #        moved there overriding the otherwise
 #        alphabetical ordering)
-CARRY4 4 1 10 8
-482 -   -   -   -   223 -   -   -   222
-598 407 -   -   -   400 205 -   -   334
-584 556 537 -   -   523 558 226 -   239
-642 615 596 438 -   582 618 330 227 313
-536 379 -   -   -   340 -   -   -   271
-494 465 445 -   -   433 469 -   -   157
-592 540 520 356 -   512 548 292 -   228
-580 526 507 398 385 508 528 378 380 114
+#   Max delays from: https://github.com/SymbiFlow/prjxray-db/blob/34ea6eb08a63d21ec16264ad37a0a7b142ff6031/artix7/timings/CLBLL_L.sdf#L11-L46
+# name ID w/b ins outs
+CARRY4 4  1   10  8
+#CYINIT DI0 DI1 DI2 DI3 S0  S1  S2  S3  CI
+482     -   -   -   -   223 -   -   -   222 # O0
+598     407 -   -   -   400 205 -   -   334 # O1
+584     556 537 -   -   523 558 226 -   239 # O2
+642     615 596 438 -   582 618 330 227 313 # O3
+536     379 -   -   -   340 -   -   -   271 # CO0
+494     465 445 -   -   433 469 -   -   157 # CO1
+592     540 520 356 -   512 548 292 -   228 # CO2
+580     526 507 398 385 508 528 378 380 114 # CO3
 
+# Box 1000 : $__ABC9_ASYNC0
+#            (private cell to emulate async behaviour of FDC*)
+# name         ID   w/b ins outs
+$__ABC9_ASYNC0 1000 1   2   1
+#A S
+0  764 # Y
+
+# Box 1001 : $__ABC9_ASYNC1
+#            (private cell to emulate async behaviour of FDP*)
+# name         ID   w/b ins outs
+$__ABC9_ASYNC1 1001 1   2   1
+#A S
+0  764 # Y
+
+# Flop boxes:
+# * Max delays from https://github.com/SymbiFlow/prjxray-db/blob/23c8b0851f979f0799318eaca90174413a46b257/artix7/timings/slicel.sdf#L237-L251
+#                   https://github.com/SymbiFlow/prjxray-db/blob/23c8b0851f979f0799318eaca90174413a46b257/artix7/timings/slicel.sdf#L265-L277
+# * Exception: $abc9_currQ is a special input (located last) necessary for clock-enable functionality
+
+# Box 1100 : FDRE
+# name ID   w/b ins outs
+FDRE   1100 1   5   1
+#C CE  D   R   $abc9_currQ
+#0 109 -46 404 0
+0 109 0   404 0 # Q (-46ps Tsu clamped to 0)
+
+# Box 1101 : FDRE_1
+# name ID   w/b ins outs
+FDRE_1 1101 1   5   1
+#C CE  D   R   $abc9_currQ
+#0 109 -46 404 0
+0 109 0   404 0 # Q (-46ps Tsu clamped to 0)
+
+# Box 1102 : FDSE
+# name ID   w/b ins outs
+FDSE   1102 1   5   1
+#C CE  D   R   $abc9_currQ
+#0 109 -46 404 0
+0 109 0   404 0 # Q (-46ps Tsu clamped to 0)
+
+# Box 1103 : FDSE_1
+# name ID   w/b ins outs
+FDSE_1 1103 1   5   1
+#C CE  D   R   $abc9_currQ
+#0 109 -46 404 0
+0 109 0   404 0 # Q (-46ps Tsu clamped to 0)
+
+# Box 1104 : FDCE
+# name ID   w/b ins outs
+FDCE   1104 1   5   1
+#C CE  CLR D   $abc9_currQ
+#0 109 764 -46 0
+0 109 764 0   0 # Q (-46ps Tsu clamped to 0)
+
+# Box 1105 : FDCE_1
+# name ID   w/b ins outs
+FDCE_1 1105 1   5   1
+#C CE  CLR D   $abc9_currQ
+#0 109 764 -46 0
+0 109 764 0   0 # Q (-46ps Tsu clamped to 0)
+
+# Box 1106 : FDPE
+# name ID   w/b ins outs
+FDPE   1106 1   5   1
+#C CE  D   PRE $abc9_currQ
+#0 109 -46 764 0
+0 109 0   764 0 # Q (-46ps Tsu clamped to 0)
+
+# Box 1107 : FDPE_1
+# name ID   w/b ins outs
+FDPE_1 1107 1   5   1
+#C CE  D   PRE $abc9_currQ
+#0 109 -46 764 0
+0 109 0   764 0 # Q (-46ps Tsu clamped to 0)
+
+# Box 2000 : $__ABC9_LUT6
+#            (private cell to emulate async behaviour of LUTRAMs)
 # SLICEM/A6LUT
-# Box to emulate comb/seq behaviour of RAMD{32,64} and SRL{16,32}
-#   Necessary since RAMD* and SRL* have both combinatorial (i.e.
-#   same-cycle read operation) and sequential (write operation
-#   is only committed on the next clock edge).
-#   To model the combinatorial path, such cells have to be split
-#   into comb and seq parts, with this box modelling only the former.
-# Inputs: A S0 S1 S2 S3 S4 S5
-# Outputs: Y
-$__ABC9_LUT6 2000 0 7 1
-0 642 631 472 407 238 127
+# name       ID   w/b ins outs
+$__ABC9_LUT6 2000 0   7   1
+#A S0  S1  S2  S3  S4  S5
+0  642 631 472 407 238 127 # Y
 
-# SLICEM/A6LUT + F7BMUX
-# Box to emulate comb/seq behaviour of RAMD128
-# Inputs: A S0 S1 S2 S3 S4 S5 S6
-# Outputs: DPO SPO
+# Box 2001 : $__ABC9_LUT6
+#            (private cell to emulate async behaviour of LUITRAMs)
+# name       ID   w/b ins outs
 $__ABC9_LUT7 2001 0 8 1
-0 1047 1036 877 812 643 532 478
+#A S0   S1   S2  S3  S4  S5  S6
+0  1047 1036 877 812 643 532 478 # Y
 
 # Boxes used to represent the comb behaviour of various modes
 #   of DSP48E1
diff --git a/techlibs/xilinx/cells_sim.v b/techlibs/xilinx/cells_sim.v
index 1cd4d2f30..22dca3c47 100644
--- a/techlibs/xilinx/cells_sim.v
+++ b/techlibs/xilinx/cells_sim.v
@@ -325,6 +325,7 @@ endmodule
 
 // Max delay from: https://github.com/SymbiFlow/prjxray-db/blob/34ea6eb08a63d21ec16264ad37a0a7b142ff6031/artix7/timings/CLBLL_L.sdf#L238-L250
 
+(* abc9_box_id=1100, lib_whitebox, abc9_flop *)
 module FDRE (
   (* abc9_arrival=303 *)
   output reg Q,
@@ -348,6 +349,20 @@ module FDRE (
   endcase endgenerate
 endmodule
 
+(* abc9_box_id=1101, lib_whitebox, abc9_flop *)
+module FDRE_1 (
+  (* abc9_arrival=303 *)
+  output reg Q,
+  (* clkbuf_sink *)
+  input C,
+  input CE, D, R
+);
+  parameter [0:0] INIT = 1'b0;
+  initial Q <= INIT;
+  always @(negedge C) if (R) Q <= 1'b0; else if (CE) Q <= D;
+endmodule
+
+(* abc9_box_id=1102, lib_whitebox, abc9_flop *)
 module FDSE (
   (* abc9_arrival=303 *)
   output reg Q,
@@ -371,6 +386,19 @@ module FDSE (
   endcase endgenerate
 endmodule
 
+(* abc9_box_id=1103, lib_whitebox, abc9_flop *)
+module FDSE_1 (
+  (* abc9_arrival=303 *)
+  output reg Q,
+  (* clkbuf_sink *)
+  input C,
+  input CE, D, S
+);
+  parameter [0:0] INIT = 1'b1;
+  initial Q <= INIT;
+  always @(negedge C) if (S) Q <= 1'b1; else if (CE) Q <= D;
+endmodule
+
 module FDRSE (
   output reg Q,
   (* clkbuf_sink *)
@@ -406,6 +434,7 @@ module FDRSE (
       Q <= d;
 endmodule
 
+(* abc9_box_id=1104, lib_whitebox, abc9_flop *)
 module FDCE (
   (* abc9_arrival=303 *)
   output reg Q,
@@ -413,10 +442,10 @@ module FDCE (
   (* invertible_pin = "IS_C_INVERTED" *)
   input C,
   input CE,
-  (* invertible_pin = "IS_D_INVERTED" *)
-  input D,
   (* invertible_pin = "IS_CLR_INVERTED" *)
-  input CLR
+  input CLR,
+  (* invertible_pin = "IS_D_INVERTED" *)
+  input D
 );
   parameter [0:0] INIT = 1'b0;
   parameter [0:0] IS_C_INVERTED = 1'b0;
@@ -431,6 +460,20 @@ module FDCE (
   endcase endgenerate
 endmodule
 
+(* abc9_box_id=1105, lib_whitebox, abc9_flop *)
+module FDCE_1 (
+  (* abc9_arrival=303 *)
+  output reg Q,
+  (* clkbuf_sink *)
+  input C,
+  input CE, D, CLR
+);
+  parameter [0:0] INIT = 1'b0;
+  initial Q <= INIT;
+  always @(negedge C, posedge CLR) if (CLR) Q <= 1'b0; else if (CE) Q <= D;
+endmodule
+
+(* abc9_box_id=1106, lib_whitebox, abc9_flop *)
 module FDPE (
   (* abc9_arrival=303 *)
   output reg Q,
@@ -456,6 +499,19 @@ module FDPE (
   endcase endgenerate
 endmodule
 
+(* abc9_box_id=1107, lib_whitebox, abc9_flop *)
+module FDPE_1 (
+  (* abc9_arrival=303 *)
+  output reg Q,
+  (* clkbuf_sink *)
+  input C,
+  input CE, D, PRE
+);
+  parameter [0:0] INIT = 1'b1;
+  initial Q <= INIT;
+  always @(negedge C, posedge PRE) if (PRE) Q <= 1'b1; else if (CE) Q <= D;
+endmodule
+
 module FDCPE (
   output wire Q,
   (* clkbuf_sink *)
@@ -501,54 +557,6 @@ module FDCPE (
   assign Q = qs ? qp : qc;
 endmodule
 
-module FDRE_1 (
-  (* abc9_arrival=303 *)
-  output reg Q,
-  (* clkbuf_sink *)
-  input C,
-  input CE, D, R
-);
-  parameter [0:0] INIT = 1'b0;
-  initial Q <= INIT;
-  always @(negedge C) if (R) Q <= 1'b0; else if(CE) Q <= D;
-endmodule
-
-module FDSE_1 (
-  (* abc9_arrival=303 *)
-  output reg Q,
-  (* clkbuf_sink *)
-  input C,
-  input CE, D, S
-);
-  parameter [0:0] INIT = 1'b1;
-  initial Q <= INIT;
-  always @(negedge C) if (S) Q <= 1'b1; else if(CE) Q <= D;
-endmodule
-
-module FDCE_1 (
-  (* abc9_arrival=303 *)
-  output reg Q,
-  (* clkbuf_sink *)
-  input C,
-  input CE, D, CLR
-);
-  parameter [0:0] INIT = 1'b0;
-  initial Q <= INIT;
-  always @(negedge C, posedge CLR) if (CLR) Q <= 1'b0; else if (CE) Q <= D;
-endmodule
-
-module FDPE_1 (
-  (* abc9_arrival=303 *)
-  output reg Q,
-  (* clkbuf_sink *)
-  input C,
-  input CE, D, PRE
-);
-  parameter [0:0] INIT = 1'b1;
-  initial Q <= INIT;
-  always @(negedge C, posedge PRE) if (PRE) Q <= 1'b1; else if (CE) Q <= D;
-endmodule
-
 module LDCE (
   output reg Q,
   (* invertible_pin = "IS_CLR_INVERTED" *)
@@ -2388,8 +2396,8 @@ module DSP48E1 (
                     if (CEB2) Br2 <= Br1;
                 end
         end else if (BREG == 1) begin
-            //initial Br1 = 25'b0;
-            initial Br2 = 25'b0;
+            //initial Br1 = 18'b0;
+            initial Br2 = 18'b0;
             always @(posedge CLK)
                 if (RSTB) begin
                     Br1 <= 18'b0;
@@ -2436,7 +2444,7 @@ module DSP48E1 (
     endgenerate
 
     // A/D input selection and pre-adder
-    wire signed [29:0] Ar12_muxed = INMODEr[0] ? Ar1 : Ar2;
+    wire signed [24:0] Ar12_muxed = INMODEr[0] ? Ar1 : Ar2;
     wire signed [24:0] Ar12_gated = INMODEr[1] ? 25'b0 : Ar12_muxed;
     wire signed [24:0] Dr_gated   = INMODEr[2] ? Dr : 25'b0;
     wire signed [24:0] AD_result  = INMODEr[3] ? (Dr_gated - Ar12_gated) : (Dr_gated + Ar12_gated);
diff --git a/techlibs/xilinx/synth_xilinx.cc b/techlibs/xilinx/synth_xilinx.cc
index e1748562e..63d00027a 100644
--- a/techlibs/xilinx/synth_xilinx.cc
+++ b/techlibs/xilinx/synth_xilinx.cc
@@ -107,8 +107,12 @@ struct SynthXilinxPass : public ScriptPass
 		log("    -flatten\n");
 		log("        flatten design before synthesis\n");
 		log("\n");
+		log("    -dff\n");
+		log("        run 'abc'/'abc9' with -dff option\n");
+		log("\n");
 		log("    -retime\n");
-		log("        run 'abc' with '-dff -D 1' options\n");
+		log("        run 'abc' with '-D 1' option to enable flip-flop retiming.\n");
+		log("        implies -dff.\n");
 		log("\n");
 		log("    -abc9\n");
 		log("        use new ABC9 flow (EXPERIMENTAL)\n");
@@ -120,7 +124,8 @@ struct SynthXilinxPass : public ScriptPass
 	}
 
 	std::string top_opt, edif_file, blif_file, family;
-	bool flatten, retime, vpr, ise, noiopad, noclkbuf, nobram, nolutram, nosrl, nocarry, nowidelut, nodsp, uram, abc9;
+	bool flatten, retime, vpr, ise, noiopad, noclkbuf, nobram, nolutram, nosrl, nocarry, nowidelut, nodsp, uram;
+	bool abc9, dff_mode;
 	bool flatten_before_abc;
 	int widemux;
 
@@ -145,6 +150,7 @@ struct SynthXilinxPass : public ScriptPass
 		nodsp = false;
 		uram = false;
 		abc9 = false;
+		dff_mode = false;
 		flatten_before_abc = false;
 		widemux = 0;
 	}
@@ -190,6 +196,7 @@ struct SynthXilinxPass : public ScriptPass
 				continue;
 			}
 			if (args[argidx] == "-retime") {
+				dff_mode = true;
 				retime = true;
 				continue;
 			}
@@ -252,6 +259,10 @@ struct SynthXilinxPass : public ScriptPass
 				uram = true;
 				continue;
 			}
+			if (args[argidx] == "-dff") {
+				dff_mode = true;
+				continue;
+			}
 			break;
 		}
 		extra_args(args, argidx, design);
@@ -287,10 +298,11 @@ struct SynthXilinxPass : public ScriptPass
 			ff_map_file = "+/xilinx/xc7_ff_map.v";
 
 		if (check_label("begin")) {
+			std::string read_args;
 			if (vpr)
-				run("read_verilog -lib -D_EXPLICIT_CARRY +/xilinx/cells_sim.v");
-			else
-				run("read_verilog -lib +/xilinx/cells_sim.v");
+				read_args += " -D_EXPLICIT_CARRY";
+			read_args += " -lib +/xilinx/cells_sim.v";
+			run("read_verilog" + read_args);
 
 			run("read_verilog -lib +/xilinx/cells_xtra.v");
 
@@ -532,12 +544,15 @@ struct SynthXilinxPass : public ScriptPass
 			if (flatten_before_abc)
 				run("flatten");
 			if (help_mode)
-				run("abc -luts 2:2,3,6:5[,10,20] [-dff]", "(option for 'nowidelut'; option for '-retime')");
+				run("abc -luts 2:2,3,6:5[,10,20] [-dff] [-D 1]", "(option for 'nowidelut', '-dff', '-retime')");
 			else if (abc9) {
 				if (family != "xc7")
 					log_warning("'synth_xilinx -abc9' not currently supported for the '%s' family, "
 							"will use timing for 'xc7' instead.\n", family.c_str());
-				run("techmap -map +/xilinx/abc9_map.v -max_iter 1");
+				std::string techmap_args = "-map +/xilinx/abc9_map.v -max_iter 1";
+				if (dff_mode)
+					techmap_args += " -D DFF_MODE";
+				run("techmap " + techmap_args);
 				run("read_verilog -icells -lib +/xilinx/abc9_model.v");
 				std::string abc9_opts = " -box +/xilinx/abc9_xc7.box";
 				abc9_opts += stringf(" -W %d", XC7_WIRE_DELAY);
@@ -545,13 +560,22 @@ struct SynthXilinxPass : public ScriptPass
 					abc9_opts += " -lut +/xilinx/abc9_xc7_nowide.lut";
 				else
 					abc9_opts += " -lut +/xilinx/abc9_xc7.lut";
+				if (dff_mode)
+					abc9_opts += " -dff";
 				run("abc9" + abc9_opts);
+				run("techmap -map +/xilinx/abc9_unmap.v");
 			}
 			else {
+				std::string abc_opts;
 				if (nowidelut)
-					run("abc -luts 2:2,3,6:5" + string(retime ? " -dff -D 1" : ""));
+					abc_opts += " -luts 2:2,3,6:5";
 				else
-					run("abc -luts 2:2,3,6:5,10,20" + string(retime ? " -dff -D 1" : ""));
+					abc_opts += " -luts 2:2,3,6:5,10,20";
+				if (dff_mode)
+					abc_opts += " -dff";
+				if (retime)
+					abc_opts += " -D 1";
+				run("abc" + abc_opts);
 			}
 			run("clean");
 
@@ -561,14 +585,11 @@ struct SynthXilinxPass : public ScriptPass
 				run("xilinx_srl -fixed -minlen 3", "(skip if '-nosrl')");
 			std::string techmap_args = "-map +/xilinx/lut_map.v -map +/xilinx/cells_map.v";
 			if (help_mode)
-				techmap_args += " [-map " + ff_map_file + "]";
-			else if (abc9)
-				techmap_args += " -map +/xilinx/abc9_unmap.v";
-			else
-				techmap_args += " -map " + ff_map_file;
-			run("techmap " + techmap_args);
+				techmap_args += stringf("[-map %s]", ff_map_file.c_str());
+			else if (!abc9)
+				techmap_args += stringf(" -map %s", ff_map_file.c_str());
+			run("techmap " + techmap_args, "(only if '-abc9')");
 			run("xilinx_dffopt");
-			run("clean");
 		}
 
 		if (check_label("finalize")) {
@@ -576,6 +597,7 @@ struct SynthXilinxPass : public ScriptPass
 				run("clkbufmap -buf BUFG O:I ", "(skip if '-noclkbuf')");
 			if (help_mode || ise)
 				run("extractinv -inv INV O:I", "(only if '-ise')");
+			run("clean");
 		}
 
 		if (check_label("check")) {