Skip to content

Instantly share code, notes, and snippets.

# promach/multiply.sby Last active Feb 20, 2019

A signed multiply verilog code using row adder tree multiplier and modified baugh-wooley algorithm
 [tasks] proof cover [options] proof: mode prove proof: depth 5 cover: mode cover cover: depth 20 cover: append 3 [engines] smtbmc yices # smtbmc boolector # abc pdr # aiger avy # aiger suprove [script] read_verilog -formal -sv multiply.v prep -top multiply [files] multiply.v
 module multiply #(parameter A_WIDTH=16, B_WIDTH=16) (clk, reset, in_valid, out_valid, in_A, in_B, out_C); // C=A*B `ifdef FORMAL parameter A_WIDTH = 6; parameter B_WIDTH = 6; `endif input clk, reset; input in_valid; // to signify that in_A, in_B are valid, multiplication process can start input signed [(A_WIDTH-1):0] in_A; input signed [(B_WIDTH-1):0] in_B; output signed [(A_WIDTH+B_WIDTH-1):0] out_C; output reg out_valid; // to signify that out_C is valid, multiplication finished /* This signed multiplier code architecture is a combination of row adder tree and modified baugh-wooley algorithm, thus requires an area of O(N*M*logN) and time O(logN) with M, N being the length(bitwidth) of the multiplicand and multiplier respectively see https://i.imgur.com/NaqjC6G.png (1+1=10 in binary, but it is denoted as 2 here) or Row Adder Tree Multipliers in http://www.andraka.com/multipli.php or https://pdfs.semanticscholar.org/415c/d98dafb5c9cb358c94189927e1f3216b7494.pdf#page=10 regarding the mechanisms within all layers In terms of fmax consideration: In the case of an adder tree, the adders making up the levels closer to the input take up real estate (remember the structure of row adder tree). As the size of the input multiplicand bitwidth grows, it becomes more and more difficult to find a placement that does not use long routes involving multiple switch nodes for FPGA. The result is the maximum clocking speed degrades quickly as the size of the bitwidth grows. For signed multiplication, see also modified baugh-wooley algorithm for trick in skipping sign extension (implemented as verilog example in https://www.dsprelated.com/showarticle/555.php), thus smaller final routed silicon area. https://stackoverflow.com/questions/54268192/understanding-modified-baugh-wooley-multiplication-algorithm/ All layers are pipelined, so throughput = one result for each clock cycle but each multiplication result still have latency = NUM_OF_INTERMEDIATE_LAYERS */ // The multiplication of two numbers is equivalent to adding as many copies of one // of them, the multiplicand, as the value of the other one, the multiplier. // Therefore, multiplicand always have the larger width compared to multipliers localparam SMALLER_WIDTH = (A_WIDTH <= B_WIDTH) ? A_WIDTH : B_WIDTH; localparam LARGER_WIDTH = (A_WIDTH > B_WIDTH) ? A_WIDTH : B_WIDTH; wire [(LARGER_WIDTH-1):0] MULTIPLICAND = (A_WIDTH > B_WIDTH) ? in_A : in_B ; wire [(SMALLER_WIDTH-1):0] MULTIPLIER = (A_WIDTH <= B_WIDTH) ? in_A : in_B ; // to keep the values of multiplicand and multiplier before the multiplication finishes reg signed [(LARGER_WIDTH-1):0] MULTIPLICAND_reg; reg signed [(SMALLER_WIDTH-1):0] MULTIPLIER_reg; always @(posedge clk) begin if(reset) begin MULTIPLICAND_reg <= 0; MULTIPLIER_reg <= 0; end else if(in_valid && !multiply_had_started) begin MULTIPLICAND_reg <= MULTIPLICAND; MULTIPLIER_reg <= MULTIPLIER; end end localparam NUM_OF_INTERMEDIATE_LAYERS = \$clog2(SMALLER_WIDTH); /*Binary multiplications and additions for partial products rows*/ // first layer has "SMALLER_WIDTH" entries of data of width "LARGER_WIDTH" // This resulted in a binary tree with faster vertical addition processes as we have // lesser (NUM_OF_INTERMEDIATE_LAYERS) rows to add // intermediate partial product rows additions // Imagine a rhombus of height of "SMALLER_WIDTH" and width of "LARGER_WIDTH" // being re-arranged into binary row adder tree // such that additions can be done in O(logN) time reg signed [(A_WIDTH+B_WIDTH-1):0] middle_layers[NUM_OF_INTERMEDIATE_LAYERS:0][0:(SMALLER_WIDTH-1)]; generate // duplicates the leafs of the binary tree // layer #0 means the youngest leaf, all the initial partial products are at this layer // layer #NUM_OF_INTERMEDIATE_LAYERS means the tree trunk, the final result is here genvar layer; for(layer=0; layer<=NUM_OF_INTERMEDIATE_LAYERS; layer=layer+1) begin: intermediate_layers integer pp_index; // leaf index within each layer of the tree always @(posedge clk) begin if(reset) begin for(pp_index=0; pp_index 0); assume(positive_value_for_B > 0); cover(in_valid && (in_A == positive_value_for_A) && (in_B == positive_value_for_B)); cover(in_valid && (in_A == negative_value_for_A) && (in_B == positive_value_for_B)); cover(in_valid && (in_A == positive_value_for_A) && (in_B == negative_value_for_B)); cover(in_valid && (in_A == negative_value_for_A) && (in_B == negative_value_for_B)); //cover(in_valid && (in_A == -2) && (in_B == -22)); cover(out_valid); end `endif endmodule
 // Testbench module test_multiply; parameter A_WIDTH=6, B_WIDTH=6; reg i_clk; reg i_reset; reg i_ce; reg signed[(A_WIDTH-1):0] i_a; reg signed[(B_WIDTH-1):0] i_b; wire signed[(A_WIDTH+B_WIDTH-1):0] o_p; wire o_valid; // Instantiate design under test multiply #(A_WIDTH, B_WIDTH) mul(.clk(i_clk), .reset(i_reset), .in_valid(i_ce), .in_A(i_a), .in_B(i_b), .out_valid(o_valid), .out_C(o_p)); initial begin // Dump waves \$dumpfile("test_multiply.vcd"); \$dumpvars(0, test_multiply); i_clk = 0; i_reset = 0; i_ce = 0; i_a = 0; i_b = 0; end localparam SMALLER_WIDTH = (A_WIDTH <= B_WIDTH) ? A_WIDTH : B_WIDTH; localparam NUM_OF_INTERMEDIATE_LAYERS = \$clog2(SMALLER_WIDTH); genvar i, j; // array index generate for(i = 0; i <= NUM_OF_INTERMEDIATE_LAYERS; i = i + 1) begin for(j = 0; j < SMALLER_WIDTH; j = j + 1) begin initial \$dumpvars(0, test_multiply.mul.middle_layers[i][j]); end end endgenerate always #5 i_clk = !i_clk; initial begin @(posedge i_clk); @(posedge i_clk); \$display("Reset flop."); i_reset = 1; @(posedge i_clk); @(posedge i_clk); i_reset = 0; @(posedge i_clk); @(posedge i_clk); i_ce = 1; i_a = 3; i_b = -2; #100 \$finish; end endmodule
to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.