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

diff --git a/tests/arch/xilinx/macc.v b/tests/arch/xilinx/macc.v
index e36b2bab1e5cf3bcee264fb3f9d8d63abbbebeb5..1645537fd96c96ef68285174e6fca4d744be2854 100644 (file)
--- 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 bf2b363209a6638f0974d2e3be6a728176c4d1de..61a570f4812a670284ea90e0da94aa23443ac406 100644 (file)
--- 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