xilinx: do not make DSP48E1 a whitebox for ABC9 by default (#2325)

* xilinx: eliminate SCCs from DSP48E1 model

* xilinx: add SCC test for DSP48E1

* Update techlibs/xilinx/cells_sim.v

* xilinx: Gate DSP48E1 being a whitebox behind ALLOW_WHITEBOX_DSP48E1

Have a test that checks it works through ABC9 when enabled

techlibs/xilinx/cells_sim.v

@@ -3014,8 +3014,12 @@ endmodule
 // Virtex 6, Series 7.
 
 `ifdef YOSYS
-(* abc9_box=!(PREG || AREG || ADREG || BREG || CREG || DREG || MREG),
+(* abc9_box=!(PREG || AREG || ADREG || BREG || CREG || DREG || MREG)
-   lib_whitebox=!(PREG || AREG || ADREG || BREG || CREG || DREG || MREG) *)
+`ifdef ALLOW_WHITEBOX_DSP48E1
+   // Do not make DSP48E1 a whitebox for ABC9 even if fully combinatorial, since it is a big complex block
+   , lib_whitebox=!(PREG || AREG || ADREG || BREG || CREG || DREG || MREG || INMODEREG || OPMODEREG || ALUMODEREG || CARRYINREG || CARRYINSELREG)
+`endif
+*)
 `endif
 module DSP48E1 (
     output [29:0] ACOUT,
@@ -3503,11 +3507,15 @@ module DSP48E1 (
                 if (OPMODEr[3:2] != 2'b01) $fatal(1, "OPMODEr[3:2] must be 2'b01 when OPMODEr[1:0] is 2'b01");
 `endif
             end
-            2'b10: begin X = P;
+            2'b10:
+                if (PREG == 1)
+                    X = P;
+                else begin
+                    X = 48'bx;
 `ifndef YOSYS
-                if (PREG != 1) $fatal(1, "PREG must be 1 when OPMODEr[1:0] is 2'b10");
+                    $fatal(1, "PREG must be 1 when OPMODEr[1:0] is 2'b10");
 `endif
-            end
+                end
             2'b11: X = $signed({Ar2, Br2});
             default: X = 48'bx;
         endcase
@@ -3529,20 +3537,36 @@ module DSP48E1 (
         case (OPMODEr[6:4])
             3'b000: Z = 48'b0;
             3'b001: Z = PCIN;
-            3'b010: begin Z = P;
+            3'b010:
+                if (PREG == 1)
+                    Z = P;
+                else begin
+                    Z = 48'bx;
 `ifndef YOSYS
-                if (PREG != 1) $fatal(1, "PREG must be 1 when OPMODEr[6:4] i0s 3'b010");
+                    $fatal(1, "PREG must be 1 when OPMODEr[6:4] is 3'b010");
 `endif
-            end
+                end
             3'b011: Z = Cr;
-            3'b100: begin Z = P;
+            3'b100:
+                if (PREG == 1 && OPMODEr[3:0] === 4'b1000)
+                    Z = P;
+                else begin
+                    Z = 48'bx;
 `ifndef YOSYS
-                if (PREG != 1) $fatal(1, "PREG must be 1 when OPMODEr[6:4] is 3'b100");
+                    if (PREG != 1) $fatal(1, "PREG must be 1 when OPMODEr[6:4] is 3'b100");
-                if (OPMODEr[3:0] != 4'b1000) $fatal(1, "OPMODEr[3:0] must be 4'b1000 when OPMODEr[6:4] i0s 3'b100");
+                    if (OPMODEr[3:0] != 4'b1000) $fatal(1, "OPMODEr[3:0] must be 4'b1000 when OPMODEr[6:4] i0s 3'b100");
 `endif
-            end
+                end
             3'b101: Z = $signed(PCIN[47:17]);
-            3'b110: Z = $signed(P[47:17]);
+            3'b110:
+                if (PREG == 1)
+                    Z = $signed(P[47:17]);
+                else begin
+                    Z = 48'bx;
+`ifndef YOSYS
+                    $fatal(1, "PREG must be 1 when OPMODEr[6:4] is 3'b110");
+`endif
+                end
             default: Z = 48'bx;
         endcase
     end
@@ -3568,10 +3592,34 @@ module DSP48E1 (
             3'b001: cin_muxed = ~PCIN[47];
             3'b010: cin_muxed = CARRYCASCIN;
             3'b011: cin_muxed = PCIN[47];
-            3'b100: cin_muxed = CARRYCASCOUT;
+            3'b100:
-            3'b101: cin_muxed = ~P[47];
+                if (PREG == 1)
+                    cin_muxed = CARRYCASCOUT;
+                else begin
+                    cin_muxed = 1'bx;
+`ifndef YOSYS
+                    $fatal(1, "PREG must be 1 when CARRYINSEL is 3'b100");
+`endif
+                end
+            3'b101:
+                if (PREG == 1)
+                    cin_muxed = ~P[47];
+                else begin
+                    cin_muxed = 1'bx;
+`ifndef YOSYS
+                    $fatal(1, "PREG must be 1 when CARRYINSEL is 3'b101");
+`endif
+                end
             3'b110: cin_muxed = A24_xnor_B17;
-            3'b111: cin_muxed = P[47];
+            3'b111:
+                if (PREG == 1)
+                    cin_muxed = P[47];
+                else begin
+                    cin_muxed = 1'bx;
+`ifndef YOSYS
+                    $fatal(1, "PREG must be 1 when CARRYINSEL is 3'b111");
+`endif
+                end
             default: cin_muxed = 1'bx;
         endcase
     end
@@ -4163,4 +4211,3 @@ module RAMB36E1 (
         if (|DOB_REG) (posedge CLKBWRCLK => (DOPBDOP : 4'bx)) = 882;
     endspecify
 endmodule
-

techlibs/xilinx/xc7_dsp_map.v

@@ -33,6 +33,7 @@ module \$__MUL25X18 (input [24:0] A, input [17:0] B, output [42:0] Y);
 		.B(B),
 		.C(48'b0),
 		.D(25'b0),
+		.CARRYIN(1'b0),
 		.P(P_48),
 
 		.INMODE(5'b00000),

tests/arch/xilinx/dsp_abc9.ys

@@ -0,0 +1,37 @@
+read_verilog <<EOT
+module top(input [24:0] A, input [17:0] B, output [47:0] P);
+DSP48E1 #(.PREG(0)) dsp(.A(A), .B(B), .P(P));
+endmodule
+EOT
+techmap -autoproc -wb -map +/xilinx/cells_sim.v
+opt
+scc -expect 0
+
+
+design -reset
+read_verilog <<EOT
+module top(input signed [24:0] A, input signed [17:0] B, output [47:0] P);
+assign P = A * B;
+endmodule
+EOT
+synth_xilinx -abc9
+techmap -autoproc -wb -map +/xilinx/cells_sim.v
+opt -full -fine
+select -assert-count 1 t:$mul
+select -assert-count 0 t:* t:$mul %D
+
+
+design -reset
+read_verilog -icells -formal <<EOT
+module top(output [42:0] P);
+\$__MUL25X18 mul (.A(42), .B(42), .Y(P));
+assert property (P == 42*42);
+endmodule
+EOT
+techmap -map +/xilinx/xc7_dsp_map.v
+verilog_defaults -add -D ALLOW_WHITEBOX_DSP48E1
+synth_xilinx -abc9
+techmap -autoproc -wb -map +/xilinx/cells_sim.v
+opt -full -fine
+select -assert-count 0 t:* t:$assert %d
+sat -verify -prove-asserts