tharunchitipolu / dadda-multiplier-using-csa Goto Github PK

Hey, it seems like these multipliers are not correct. I don't have the time for debugging them currently but thought you should be aware.

For example when I run dadda_16 in simulation with A = 18432 (0x4800) and B = 1152 (0x0480), I get 17039360 (0x01040000) instead of the expected 21233664 (0x01440000).

For reference I found these examples with a simple SymbiYosys config file of the form below:

[options]
mode bmc
depth 1

[engines]
smtbmc

[script]
read_verilog HA.v
read_verilog csa_dadda.v
read_verilog dadda_8.v
read_verilog dadda_16.v

read_verilog -sv <<EOT
module top(
    input [15:0] A,
    input [15:0] B,
    output wire [31:0] Y
);

dadda_16 dut(.*);
always @* assert(Y == A * B);
endmodule
EOT

prep -top top

[files]
HA.v
csa_dadda.v
dadda_8.v
dadda_16.v