diff --git a/tests/arch/nexus/dsp_equiv.sv b/tests/arch/nexus/dsp_equiv.sv new file mode 100644 index 000000000..88eb8bb21 --- /dev/null +++ b/tests/arch/nexus/dsp_equiv.sv @@ -0,0 +1,45 @@ +// https://github.com/YosysHQ/yosys/issues/5906 +module mac_add_u (input [8:0] a, b, input [17:0] c, output [17:0] y); + assign y = a*b + c; +endmodule + +module mac_add_s (input signed [8:0] a, b, input signed [17:0] c, output signed [17:0] y); + assign y = a*b + c; +endmodule + +module mac_sub_u (input [8:0] a, b, input [17:0] c, output [17:0] y); + assign y = c - a*b; +endmodule + +module mac_sub_s (input signed [8:0] a, b, input signed [17:0] c, output signed [17:0] y); + assign y = c - a*b; +endmodule + +module mac_subrev_u (input [8:0] a, b, input [17:0] c, output [17:0] y); + assign y = a*b - c; +endmodule + +module mac_wide_s (input signed [8:0] a, b, input signed [17:0] c, output signed [29:0] y); + assign y = c - a*b; +endmodule + +// https://github.com/YosysHQ/yosys/issues/5929 +module mul_pipe_u (input clk, input [8:0] a, b, output reg [17:0] y); + reg [8:0] a_r; + reg [8:0] b_r; + always @(posedge clk) begin + a_r <= a; + b_r <= b; + y <= a_r * b_r; + end +endmodule + +module mul_pipe_s (input clk, input signed [8:0] a, b, output reg signed [17:0] y); + reg signed [8:0] a_r; + reg signed [8:0] b_r; + always @(posedge clk) begin + a_r <= a; + b_r <= b; + y <= a_r * b_r; + end +endmodule diff --git a/tests/arch/nexus/dsp_equiv.ys b/tests/arch/nexus/dsp_equiv.ys new file mode 100644 index 000000000..61b0df443 --- /dev/null +++ b/tests/arch/nexus/dsp_equiv.ys @@ -0,0 +1,154 @@ +read_verilog -sv dsp_equiv.sv +design -save src + +# y = a*b + c (unsigned) +design -load src +hierarchy -top mac_add_u +proc +design -stash gold +design -load src +hierarchy -top mac_add_u +synth_nexus -family lifcl -noiopad +select -assert-count 1 t:MULTADDSUB18X18 +read_verilog +/lattice/cells_sim_nexus.v +hierarchy -top mac_add_u +flatten +proc +design -stash gate +design -copy-from gold -as gold mac_add_u +design -copy-from gate -as gate mac_add_u +miter -equiv -make_assert -flatten gold gate equiv +sat -seq 1 -set-init-zero -prove-asserts -verify equiv + +# y = a*b + c (signed) +design -load src +hierarchy -top mac_add_s +proc +design -stash gold +design -load src +hierarchy -top mac_add_s +synth_nexus -family lifcl -noiopad +select -assert-count 1 t:MULTADDSUB18X18 +read_verilog +/lattice/cells_sim_nexus.v +hierarchy -top mac_add_s +flatten +proc +design -stash gate +design -copy-from gold -as gold mac_add_s +design -copy-from gate -as gate mac_add_s +miter -equiv -make_assert -flatten gold gate equiv +sat -seq 1 -set-init-zero -prove-asserts -verify equiv + +# y = c - a*b (unsigned) +design -load src +hierarchy -top mac_sub_u +proc +design -stash gold +design -load src +hierarchy -top mac_sub_u +synth_nexus -family lifcl -noiopad +select -assert-count 1 t:MULTADDSUB18X18 +read_verilog +/lattice/cells_sim_nexus.v +hierarchy -top mac_sub_u +flatten +proc +design -stash gate +design -copy-from gold -as gold mac_sub_u +design -copy-from gate -as gate mac_sub_u +miter -equiv -make_assert -flatten gold gate equiv +sat -seq 1 -set-init-zero -prove-asserts -verify equiv + +# y = c - a*b (signed) +design -load src +hierarchy -top mac_sub_s +proc +design -stash gold +design -load src +hierarchy -top mac_sub_s +synth_nexus -family lifcl -noiopad +select -assert-count 1 t:MULTADDSUB18X18 +read_verilog +/lattice/cells_sim_nexus.v +hierarchy -top mac_sub_s +flatten +proc +design -stash gate +design -copy-from gold -as gold mac_sub_s +design -copy-from gate -as gate mac_sub_s +miter -equiv -make_assert -flatten gold gate equiv +sat -seq 1 -set-init-zero -prove-asserts -verify equiv + +# y = c - a*b (signed, wide out) +design -load src +hierarchy -top mac_wide_s +proc +design -stash gold +design -load src +hierarchy -top mac_wide_s +synth_nexus -family lifcl -noiopad +select -assert-count 1 t:MULTADDSUB18X18 +read_verilog +/lattice/cells_sim_nexus.v +hierarchy -top mac_wide_s +flatten +proc +design -stash gate +design -copy-from gold -as gold mac_wide_s +design -copy-from gate -as gate mac_wide_s +miter -equiv -make_assert -flatten gold gate equiv +sat -seq 1 -set-init-zero -prove-asserts -verify equiv + +# y = a*b - c (minuend mul) +design -load src +hierarchy -top mac_subrev_u +proc +design -stash gold +design -load src +hierarchy -top mac_subrev_u +synth_nexus -family lifcl -noiopad +select -assert-count 0 t:MULTADDSUB18X18 +read_verilog +/lattice/cells_sim_nexus.v +hierarchy -top mac_subrev_u +flatten +proc +design -stash gate +design -copy-from gold -as gold mac_subrev_u +design -copy-from gate -as gate mac_subrev_u +miter -equiv -make_assert -flatten gold gate equiv +sat -seq 1 -set-init-zero -prove-asserts -verify equiv + +# pipelined mul (unsigned) +design -load src +hierarchy -top mul_pipe_u +proc +design -stash gold +design -load src +hierarchy -top mul_pipe_u +synth_nexus -family lifcl -noiopad +select -assert-count 1 t:MULT18X18 r:REGINPUTA=REGISTER r:REGINPUTB=REGISTER r:REGOUTPUT=REGISTER +read_verilog +/lattice/cells_sim_nexus.v +hierarchy -top mul_pipe_u +flatten +proc +design -stash gate +design -copy-from gold -as gold mul_pipe_u +design -copy-from gate -as gate mul_pipe_u +miter -equiv -make_assert -flatten gold gate equiv +sat -seq 6 -set-init-zero -prove-asserts -verify equiv + +# pipelined mul (signed) +design -load src +hierarchy -top mul_pipe_s +proc +design -stash gold +design -load src +hierarchy -top mul_pipe_s +synth_nexus -family lifcl -noiopad +select -assert-count 1 t:MULT18X18 r:REGINPUTA=REGISTER r:REGINPUTB=REGISTER r:REGOUTPUT=REGISTER +read_verilog +/lattice/cells_sim_nexus.v +hierarchy -top mul_pipe_s +flatten +proc +design -stash gate +design -copy-from gold -as gold mul_pipe_s +design -copy-from gate -as gate mul_pipe_s +miter -equiv -make_assert -flatten gold gate equiv +sat -seq 6 -set-init-zero -prove-asserts -verify equiv