riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

tests: xilinx macc test to have initval, shorten BMC depth for runtime

This commit is contained in:
Eddie Hung 2020-05-25 09:35:41 -07:00
parent 5b81df57c8
commit 08221edbc1
2 changed files with 8 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
tests/arch/xilinx/macc.v
View File

@ -10,10 +10,10 @@ module macc # (parameter SIZEIN = 16, SIZEOUT = 40) (
output signed [SIZEOUT-1:0] accum_out output signed [SIZEOUT-1:0] accum_out
); );
// Declare registers for intermediate values // Declare registers for intermediate values
reg signed [SIZEIN-1:0] a_reg, b_reg; reg signed [SIZEIN-1:0] a_reg = 0, b_reg = 0;
reg sload_reg; reg sload_reg = 0;
reg signed [2*SIZEIN-1:0] mult_reg; reg signed [2*SIZEIN-1:0] mult_reg = 0;
reg signed [SIZEOUT-1:0] adder_out, old_result; reg signed [SIZEOUT-1:0] adder_out = 0, old_result;
always @* /*(adder_out or sload_reg)*/ begin // Modification necessary to fix sim/synth mismatch always @* /*(adder_out or sload_reg)*/ begin // Modification necessary to fix sim/synth mismatch
if (sload_reg) if (sload_reg)
old_result <= 0; old_result <= 0;
@ -50,10 +50,10 @@ module macc2 # (parameter SIZEIN = 16, SIZEOUT = 40) (
output overflow output overflow
); );
// Declare registers for intermediate values // Declare registers for intermediate values
reg signed [SIZEIN-1:0] a_reg, b_reg, a_reg2, b_reg2; reg signed [SIZEIN-1:0] a_reg = 0, b_reg = 0, a_reg2 = 0, b_reg2 = 0;
reg signed [2*SIZEIN-1:0] mult_reg = 0; reg signed [2*SIZEIN-1:0] mult_reg = 0;
reg signed [SIZEOUT:0] adder_out = 0; reg signed [SIZEOUT:0] adder_out = 0;
reg overflow_reg; reg overflow_reg = 0;
always @(posedge clk) begin always @(posedge clk) begin
//if (ce) //if (ce)
begin begin

4
tests/arch/xilinx/macc.ys
View File

@ -6,7 +6,7 @@ proc
#equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad ### TODO #equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad ### TODO
equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad
miter -equiv -flatten -make_assert -make_outputs gold gate miter miter -equiv -flatten -make_assert -make_outputs gold gate miter
sat -verify -prove-asserts -seq 10 -show-inputs -show-outputs miter sat -verify -prove-asserts -seq 3 -show-inputs -show-outputs miter
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd macc # Constrain all select calls below inside the top module cd macc # Constrain all select calls below inside the top module
select -assert-count 1 t:BUFG select -assert-count 1 t:BUFG
@ -20,7 +20,7 @@ proc
#equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad ### TODO #equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad ### TODO
equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad
miter -equiv -flatten -make_assert -make_outputs gold gate miter miter -equiv -flatten -make_assert -make_outputs gold gate miter
sat -verify -prove-asserts -seq 10 -show-inputs -show-outputs miter sat -verify -prove-asserts -seq 4 -show-inputs -show-outputs miter
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd macc2 # Constrain all select calls below inside the top module cd macc2 # Constrain all select calls below inside the top module