diff options
author | Eddie Hung <eddie@fpgeh.com> | 2020-05-25 09:35:41 -0700 |
---|---|---|
committer | Eddie Hung <eddie@fpgeh.com> | 2020-05-25 10:09:05 -0700 |
commit | 08221edbc15333bcd05ae65cee09c86f875076ab (patch) | |
tree | 45bbb8a4ead0be11cd69d801601630c53bdf9352 /tests/arch | |
parent | 5b81df57c8c6779077c69ed8247fce7647616ade (diff) | |
download | yosys-08221edbc15333bcd05ae65cee09c86f875076ab.tar.gz yosys-08221edbc15333bcd05ae65cee09c86f875076ab.tar.bz2 yosys-08221edbc15333bcd05ae65cee09c86f875076ab.zip |
tests: xilinx macc test to have initval, shorten BMC depth for runtime
Diffstat (limited to 'tests/arch')
-rw-r--r-- | tests/arch/xilinx/macc.v | 12 | ||||
-rw-r--r-- | tests/arch/xilinx/macc.ys | 4 |
2 files changed, 8 insertions, 8 deletions
diff --git a/tests/arch/xilinx/macc.v b/tests/arch/xilinx/macc.v index e36b2bab1..1645537fd 100644 --- a/tests/arch/xilinx/macc.v +++ b/tests/arch/xilinx/macc.v @@ -10,10 +10,10 @@ module macc # (parameter SIZEIN = 16, SIZEOUT = 40) ( output signed [SIZEOUT-1:0] accum_out ); // Declare registers for intermediate values -reg signed [SIZEIN-1:0] a_reg, b_reg; -reg sload_reg; -reg signed [2*SIZEIN-1:0] mult_reg; -reg signed [SIZEOUT-1:0] adder_out, old_result; +reg signed [SIZEIN-1:0] a_reg = 0, b_reg = 0; +reg sload_reg = 0; +reg signed [2*SIZEIN-1:0] mult_reg = 0; +reg signed [SIZEOUT-1:0] adder_out = 0, old_result; always @* /*(adder_out or sload_reg)*/ begin // Modification necessary to fix sim/synth mismatch if (sload_reg) old_result <= 0; @@ -50,10 +50,10 @@ module macc2 # (parameter SIZEIN = 16, SIZEOUT = 40) ( output overflow ); // 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 [SIZEOUT:0] adder_out = 0; -reg overflow_reg; +reg overflow_reg = 0; always @(posedge clk) begin //if (ce) begin diff --git a/tests/arch/xilinx/macc.ys b/tests/arch/xilinx/macc.ys index bf2b36320..61a570f48 100644 --- a/tests/arch/xilinx/macc.ys +++ b/tests/arch/xilinx/macc.ys @@ -6,7 +6,7 @@ proc #equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad ### TODO equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad 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) cd macc # Constrain all select calls below inside the top module 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 -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad 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) cd macc2 # Constrain all select calls below inside the top module |