Bsg mul add unsigned dev

bin/main.rkt

@@ -533,4 +533,4 @@
                                   (error "Yosys failed."))))
        (output-port))]
 
-     [_ (error "Invalid output format.")])])
+     [_ (error "Invalid output format.")])])

integration_tests/lakeroad/.gitignore

@@ -0,0 +1 @@
+*.log

integration_tests/lakeroad/bsg_defines.sv

@@ -0,0 +1,194 @@
+`ifndef BSG_DEFINES_V
+`define BSG_DEFINES_V
+
+`define BSG_MAX(x,y) (((x)>(y)) ? (x) : (y))
+`define BSG_MIN(x,y) (((x)<(y)) ? (x) : (y))
+
+`define BSG_SIGN_EXTEND(sig, width) \
+  ({{`BSG_MAX(width-$bits(sig),0){sig[$bits(sig)-1]}}, sig[0+:`BSG_MIN(width, $bits(sig))]})
+`define BSG_ZERO_EXTEND(sig, width) \
+  ({{`BSG_MAX(width-$bits(sig),0){1'b0}}, sig[0+:`BSG_MIN(width, $bits(sig))]})
+
+// place this macro at the end of a verilog module file if that module has invalid parameters
+// that must be specified by the user. this will prevent that module from becoming a top-level
+// module per the discussion here: https://github.com/SymbiFlow/sv-tests/issues/1160 and the
+// SystemVerilog Standard
+
+//    "Top-level modules are modules that are included in the SystemVerilog
+//    source text, but do not appear in any module instantiation statement, as
+//    described in 23.3.2. This applies even if the module instantiation appears
+//    in a generate block that is not itself instantiated (see 27.3). A design
+//    shall contain at least one top-level module. A top-level module is
+//    implicitly instantiated once, and its instance name is the same as the
+//    module name. Such an instance is called a top-level instance."
+//  
+
+`define BSG_ABSTRACT_MODULE(fn) \
+    /*verilator lint_off DECLFILENAME*/ \
+    /*verilator lint_off PINMISSING*/ \
+    module fn``__abstract(); if (0) fn not_used(); endmodule \
+    /*verilator lint_on PINMISSING*/ \
+    /*verilator lint_on DECLFILENAME*/
+
+// macro for defining invalid parameter; with the abstract module declaration
+// it should be sufficient to omit the "inv" but we include this for tool portability
+// if later we find that all tools are compatible, we can remove the use of this from BaseJump STL
+
+`ifdef XCELIUM // Bare default parameters are incompatible as of 20.09.012
+               // = "inv" causes type inference mismatch as of 20.09.012
+`define BSG_INV_PARAM(param) param = -1
+`elsif YOSYS // Bare default parameters are incompatible as of 0.9
+`define BSG_INV_PARAM(param) param = "inv"
+`else // VIVADO, DC, VERILATOR, GENUS, SURELOG
+`define BSG_INV_PARAM(param) param
+`endif
+
+
+// maps 1 --> 1 instead of to 0
+`define BSG_SAFE_CLOG2(x) ( (((x)==1) || ((x)==0))? 1 : $clog2((x)))
+`define BSG_IS_POW2(x) ( (1 << $clog2(x)) == (x))
+`define BSG_WIDTH(x) ($clog2(x+1))
+`define BSG_SAFE_MINUS(x, y) (((x)<(y))) ? 0 : ((x)-(y))
+
+// calculate ceil(x/y) 
+`define BSG_CDIV(x,y) (((x)+(y)-1)/(y))
+
+`ifdef SYNTHESIS
+`define BSG_UNDEFINED_IN_SIM(val) (val)
+`else
+`define BSG_UNDEFINED_IN_SIM(val) ('X)
+`endif
+
+`ifdef VERILATOR
+`define BSG_HIDE_FROM_VERILATOR(val)
+`else
+`define BSG_HIDE_FROM_VERILATOR(val) val
+`endif
+
+`ifdef SYNTHESIS
+`define BSG_DISCONNECTED_IN_SIM(val) (val)
+`elsif VERILATOR
+`define BSG_DISCONNECTED_IN_SIM(val) (val)
+`else
+`define BSG_DISCONNECTED_IN_SIM(val) ('z)
+`endif
+
+// Ufortunately per the Xilinx forums, Xilinx does not define
+// any variable that indicates that Vivado Synthesis is running
+// so as a result we identify Vivado merely as the exclusion of
+// Synopsys Design Compiler (DC). Support beyond DC and Vivado
+// will require modification of this macro.
+
+`ifdef SYNTHESIS
+  `ifdef DC
+  `define BSG_VIVADO_SYNTH_FAILS
+  `elsif CDS_TOOL_DEFINE
+  `define BSG_VIVADO_SYNTH_FAILS
+  `elsif SURELOG
+  `define BSG_VIVADO_SYNTH_FAILS
+  `elsif YOSYS
+  `define BSG_VIVADO_SYNTH_FAILS
+  `else
+  `define BSG_VIVADO_SYNTH_FAILS this_module_is_not_synthesizeable_in_vivado
+  `endif
+`else
+`define BSG_VIVADO_SYNTH_FAILS
+`endif
+
+`define BSG_STRINGIFY(x) `"x`"
+
+
+// For the modules that must be hardened, add this macro at the top.
+`ifdef SYNTHESIS
+`define BSG_SYNTH_MUST_HARDEN this_module_must_be_hardened
+`else
+`define BSG_SYNTH_MUST_HARDEN
+`endif
+
+
+// using C-style shifts instead of a[i] allows the parameter of BSG_GET_BIT to be a parameter subrange                                                                                                                                                                               
+// e.g., parameter[4:1][1], which DC 2016.12 does not allow                                                                                                                                                                                                                          
+
+`define BSG_GET_BIT(X,NUM) (((X)>>(NUM))&1'b1)
+
+// This version of countones works in synthesis, but only up to 64 bits                                                                                                                                                                                                              
+// we do a funny thing where we propagate X's in simulation if it is more than 64 bits                                                                                                                                                                                               
+// and in synthesis, go ahead and ignore the high bits                                                                                                                                                                      
+
+`define BSG_COUNTONES_SYNTH(y) (($bits(y) < 65) ? 1'b0 : `BSG_UNDEFINED_IN_SIM(1'b0)) + (`BSG_GET_BIT(y,0) +`BSG_GET_BIT(y,1) +`BSG_GET_BIT(y,2) +`BSG_GET_BIT(y,3) +`BSG_GET_BIT(y,4) +`BSG_GET_BIT(y,5) +`BSG_GET_BIT(y,6)+`BSG_GET_BIT(y,7) +`BSG_GET_BIT(y,8)+`BSG_GET_BIT(y,9) \
+                                                                                       +`BSG_GET_BIT(y,10)+`BSG_GET_BIT(y,11)+`BSG_GET_BIT(y,12)+`BSG_GET_BIT(y,13)+`BSG_GET_BIT(y,14)+`BSG_GET_BIT(y,15)+`BSG_GET_BIT(y,16)+`BSG_GET_BIT(y,17)+`BSG_GET_BIT(y,18)+`BSG_GET_BIT(y,19) \
+                                                                                       +`BSG_GET_BIT(y,20)+`BSG_GET_BIT(y,21)+`BSG_GET_BIT(y,22)+`BSG_GET_BIT(y,23)+`BSG_GET_BIT(y,24)+`BSG_GET_BIT(y,25)+`BSG_GET_BIT(y,26)+`BSG_GET_BIT(y,27)+`BSG_GET_BIT(y,28)+`BSG_GET_BIT(y,29) \
+                                                                                       +`BSG_GET_BIT(y,30)+`BSG_GET_BIT(y,31)+`BSG_GET_BIT(y,32)+`BSG_GET_BIT(y,33)+`BSG_GET_BIT(y,34)+`BSG_GET_BIT(y,35)+`BSG_GET_BIT(y,36)+`BSG_GET_BIT(y,37)+`BSG_GET_BIT(y,38)+`BSG_GET_BIT(y,39) \
+                                                                                       +`BSG_GET_BIT(y,40)+`BSG_GET_BIT(y,41)+`BSG_GET_BIT(y,42)+`BSG_GET_BIT(y,43)+`BSG_GET_BIT(y,44)+`BSG_GET_BIT(y,45)+`BSG_GET_BIT(y,46)+`BSG_GET_BIT(y,47)+`BSG_GET_BIT(y,48)+`BSG_GET_BIT(y,49) \
+                                                                                       +`BSG_GET_BIT(y,50)+`BSG_GET_BIT(y,51)+`BSG_GET_BIT(y,52)+`BSG_GET_BIT(y,53)+`BSG_GET_BIT(y,54)+`BSG_GET_BIT(y,55)+`BSG_GET_BIT(y,56)+`BSG_GET_BIT(y,57)+`BSG_GET_BIT(y,58)+`BSG_GET_BIT(y,59) \
+                                                                                       +`BSG_GET_BIT(y,60)+`BSG_GET_BIT(y,61)+`BSG_GET_BIT(y,62)+`BSG_GET_BIT(y,63))
+
+// nullify rpgroups
+`ifndef rpgroup
+`define rpgroup(x)
+`endif
+
+// verilog preprocessing -> if defined(A) && defined(B) then define C
+`define BSG_DEFIF_A_AND_B(A,B,C) \
+    `undef C \
+    `ifdef A \
+        `ifdef B \
+            `define C \
+        `endif \
+    `endif
+
+// verilog preprocessing -> if defined(A) && !defined(B) then define C
+`define BSG_DEFIF_A_AND_NOT_B(A,B,C) \
+    `undef C \
+    `ifdef A \
+        `ifndef B \
+            `define C \
+        `endif \
+    `endif
+
+// verilog preprocessing -> if !defined(A) && defined(B) then define C
+`define BSG_DEFIF_NOT_A_AND_B(A,B,C) `BSG_DEFIF_A_AND_NOT_B(B,A,C)
+
+// verilog preprocessing -> if !defined(A) && !defined(B) then define C
+`define BSG_DEFIF_NOT_A_AND_NOT_B(A,B,C) \
+    `undef C \
+    `ifndef A \
+        `ifndef B \
+            `define C \
+        `endif \
+    `endif
+
+// verilog preprocessing -> if defined(A) || defined(B) then define C
+`define BSG_DEFIF_A_OR_B(A,B,C) \
+    `undef C \
+    `ifdef A \
+        `define C \
+    `endif \
+    `ifdef B \
+        `define C \
+    `endif
+
+// verilog preprocessing -> if defined(A) || !defined(B) then define C
+`define BSG_DEFIF_A_OR_NOT_B(A,B,C) \
+    `undef C \
+    `ifdef A \
+        `define C \
+    `endif \
+    `ifndef B \
+        `define C \
+    `endif
+
+// verilog preprocessing -> if !defined(A) || defined(B) then define C
+`define BSG_DEFIF_NOT_A_OR_B(A,B,C) `BSG_DEFIF_A_OR_NOT_B(B,A,C)
+
+// verilog preprocessing -> if !defined(A) || !defined(B) then define C
+`define BSG_DEFIF_NOT_A_OR_NOT_B(A,B,C) \
+    `undef C \
+    `ifndef A \
+        `define C \
+    `endif \
+    `ifndef B \
+        `define C \
+    `endif
+
+`endif

integration_tests/lakeroad/bsg_dff.sv

@@ -0,0 +1,20 @@
+
+`include "bsg_defines.sv"
+
+module bsg_dff #(parameter `BSG_INV_PARAM(width_p)
+		 ,harden_p=0
+		 ,strength_p=1   // set drive strength
+		 )
+   (input   clk_i
+    ,input  [width_p-1:0] data_i
+    ,output [width_p-1:0] data_o
+    );
+
+   reg [width_p-1:0] data_r;
+
+   assign data_o = data_r;
+
+   always @(posedge clk_i)
+     data_r <= data_i;
+
+endmodule

integration_tests/lakeroad/bsg_dff_chain.sv

@@ -0,0 +1,52 @@
+ //====================================================================
+// bsg_dff_chain.sv
+// 04/01/2018, shawnless.xie@gmail.com
+//====================================================================
+//
+// Pass the input singal to a chainded  DFF registers
+
+`include "bsg_defines.sv"
+`include "bsg_dff.sv"
+
+module bsg_dff_chain #(
+                 //the width of the input signal
+                 parameter width_p = 27
+
+                 //the stages of the chained DFF register
+                 //can be 0
+                ,parameter       num_stages_p    =       1
+        )
+        (
+                 input                           clk_i
+                ,input [width_p-1:0]             data_i
+                ,output[width_p-1:0]             data_o
+        );
+
+        logic [1:0][27-1:0] data_delayed;
+
+        if( num_stages_p == 0) begin:pass_through
+                wire unused = clk_i;
+                assign data_o   = data_i;
+        end:pass_through
+
+        else begin:chained
+                // data_i -- delayed[0]
+                //
+                // data_o -- delayed[num_stages_p]
+
+                assign data_delayed[0]  = data_i                        ;
+                assign data_o           = data_delayed[num_stages_p]    ;
+
+                genvar i;
+                for(i=1; i<= 1; i++) begin
+                        bsg_dff #( .width_p ( width_p ) )
+                                ch_reg (
+                                        .clk_i        ( clk_i                 )
+                                       ,.data_i         ( data_delayed[ i-1 ]   )
+                                       ,.data_o         ( data_delayed[ i   ]   )
+                                );
+                end
+
+        end:chained
+
+endmodule

integration_tests/lakeroad/bsg_mul_add_unsigned.sv

@@ -0,0 +1,91 @@
+// RUN: outfile=$(mktemp)
+// RUN: racket $LAKEROAD_DIR/bin/main.rkt \
+// RUN:  --solver bitwuzla \
+// RUN:  --verilog-module-filepath %s \
+// RUN:  --architecture xilinx-ultrascale-plus \
+// RUN:  --template dsp \
+// RUN:  --out-format verilog \
+// RUN:  --top-module-name top \
+// RUN:  --verilog-module-out-signal o:27 \
+// RUN:  --pipeline-depth 1 \
+// RUN:  --clock-name clk_i \
+// RUN:  --module-name test_module \
+// RUN:  --input-signal a_i:13 \
+// RUN:  --input-signal b_i:13 \
+// RUN:  --input-signal c_i:26 \
+// RUN:  --timeout 270 \
+// RUN: > $outfile
+// RUN: cat $outfile
+// RUN: FileCheck %s < $outfile
+// RUN: if [ -z ${LAKEROAD_PRIVATE_DIR+x} ]; then \
+// RUN:   echo "Warning: LAKEROAD_PRIVATE_DIR is not set. Skipping simulation."; \
+// RUN:   exit 0; \
+// RUN: else \
+// RUN:   python3 $LAKEROAD_DIR/bin/simulate_with_verilator.py \
+// RUN:    --test_module_name test_module \
+// RUN:    --ground_truth_module_name top \
+// RUN:    --max_num_tests=10000 \
+// RUN:    --verilog_filepath $outfile \
+// RUN:    --verilog_filepath %s \
+// RUN:    --clock_name clk_i \
+// RUN:    --pipeline_depth 1 \
+// RUN:    --output_signal o:27 \
+// RUN:    --input_signal a_i:13 \
+// RUN:    --input_signal b_i:13 \
+// RUN:    --input_signal c_i:26 \
+// RUN:    --verilator_include_dir "$LAKEROAD_PRIVATE_DIR/DSP48E2/" \
+// RUN:    --testbench_stdout_log_filepath "tmp.log" \
+// RUN:    --verilator_extra_arg='-DXIL_XECLIB' \
+// RUN:    --verilator_extra_arg='-Wno-UNOPTFLAT' \
+// RUN:    --verilator_extra_arg='-Wno-LATCH' \
+// RUN:    --verilator_extra_arg='-Wno-WIDTH' \
+// RUN:    --verilator_extra_arg='-Wno-STMTDLY' \
+// RUN:    --verilator_extra_arg='-Wno-CASEX' \
+// RUN:    --verilator_extra_arg='-Wno-TIMESCALEMOD' \
+// RUN:    --verilator_extra_arg='-Wno-PINMISSING'; \
+// RUN: fi
+
+`include "bsg_defines.sv"
+`include "bsg_dff_chain.sv"
+
+(* use_dsp = "yes" *) module top #(
+    parameter  width_a_p = 13
+    ,parameter width_b_p = 13
+    ,parameter width_c_p = 26
+    ,parameter width_o_p = 27
+    ,parameter pipeline_p = 1
+  ) (
+     input [width_a_p-1 : 0] a_i
+    ,input [width_b_p-1 : 0] b_i
+    ,input [width_c_p-1 : 0] c_i
+    ,input clk_i
+    ,output [width_o_p-1 : 0] o
+    );
+
+    localparam pre_pipeline_lp = pipeline_p > 2 ? 1 : 0;
+    localparam post_pipeline_lp = pipeline_p > 2 ? pipeline_p -1 : pipeline_p; //for excess
+
+    wire [width_a_p-1:0] a_r;
+    wire [width_b_p-1:0] b_r;
+    wire [width_c_p-1:0] c_r;
+
+    bsg_dff_chain #(width_a_p + width_b_p + width_c_p, pre_pipeline_lp)
+        pre_mul_add (
+            .clk_i(clk_i)
+            ,.data_i({a_i, b_i, c_i})
+            ,.data_o({a_r, b_r, c_r})
+        );
+
+    wire [width_o_p-1:0] o_r = a_r * b_r + c_r;
+
+    bsg_dff_chain #(width_o_p, post_pipeline_lp)
+        post_mul_add (
+            .clk_i(clk_i)
+            ,.data_i(o_r)
+            ,.data_o(o)
+        );
+endmodule
+
+// CHECK: module test_module(a_i, b_i, c_i, clk_i, o);
+// CHECK:   DSP48E2 #(
+// CHECK: endmodule

integration_tests/lakeroad/tmp/rosette17222789411722278941006.smt2

@@ -0,0 +1,9 @@
+(set-option :auto-config true)
+(set-option :produce-unsat-cores false)
+(set-option :smt.mbqi.max_iterations 10000000)
+(set-option :smt.relevancy 2)
+(reset)
+(set-option :auto-config true)
+(set-option :produce-unsat-cores false)
+(set-option :smt.mbqi.max_iterations 10000000)
+(set-option :smt.relevancy 2)