From e68507a71603553426a338bcffb0eccb1653436f Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Fri, 6 Sep 2019 23:19:03 -0700 Subject: [PATCH] Update macc test --- tests/xilinx/macc.v | 66 +++++++++++++++++++++++--------------------- tests/xilinx/macc.ys | 18 +++++------- 2 files changed, 42 insertions(+), 42 deletions(-) diff --git a/tests/xilinx/macc.v b/tests/xilinx/macc.v index bae63b5a4..0bb673316 100644 --- a/tests/xilinx/macc.v +++ b/tests/xilinx/macc.v @@ -1,37 +1,41 @@ // Signed 40-bit streaming accumulator with 16-bit inputs // File: HDL_Coding_Techniques/multipliers/multipliers4.v // -module macc # (parameter SIZEIN = /*16*/7, SIZEOUT = 40) - (input clk, ce, sload, - input signed [SIZEIN-1:0] a, b, - 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:0] mult_reg; - reg signed [SIZEOUT-1:0] adder_out, old_result; - always @(adder_out or sload_reg) begin - //if (sload_reg) - //old_result <= 0; - //else - // 'sload' is now active (=low) and opens the accumulation loop. - // The accumulator takes the next multiplier output in - // the same cycle. - old_result <= adder_out; - a_reg <= a; - b_reg <= b; - end +// Source: +// https://www.xilinx.com/support/documentation/sw_manuals/xilinx2014_2/ug901-vivado-synthesis.pdf p.90 +// +module macc # (parameter SIZEIN = 16, SIZEOUT = 40) ( + input clk, ce, sload, + input signed [SIZEIN-1:0] a, b, + 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; +always @* /*(adder_out or sload_reg)*/ begin // Modification necessary to fix sim/synth mismatch + if (sload_reg) + old_result <= 0; + else + // 'sload' is now active (=low) and opens the accumulation loop. + // The accumulator takes the next multiplier output in + // the same cycle. + old_result <= adder_out; +end - always @(posedge clk) - //if (ce) - begin - mult_reg <= a_reg * b_reg; - sload_reg <= sload; - // Store accumulation result into a register - adder_out <= old_result + mult_reg; - end +always @(posedge clk) + if (ce) + begin + a_reg <= a; + b_reg <= b; + mult_reg <= a_reg * b_reg; + sload_reg <= sload; + // Store accumulation result into a register + adder_out <= old_result + mult_reg; + end - // Output accumulation result - assign accum_out = adder_out; + // Output accumulation result + assign accum_out = adder_out; -endmodule // macc +endmodule diff --git a/tests/xilinx/macc.ys b/tests/xilinx/macc.ys index 62b69f4d2..de408162c 100644 --- a/tests/xilinx/macc.ys +++ b/tests/xilinx/macc.ys @@ -1,17 +1,13 @@ read_verilog macc.v proc -hierarchy -top macc -equiv_opt -run :restore -map +/xilinx/cells_sim.v synth_xilinx # equivalency check - -#equiv_miter -trigger miter equiv -#sat -verify -prove-asserts -tempinduct -show-inputs -show-outputs miter - -#equiv_opt -assert -run :prove -map +/xilinx/cells_sim.v synth_xilinx # equivalency check -#miter -equiv -flatten -make_assert -make_outputs gold gate miter -#sat -set-init-zero -verify -prove-asserts -seq 10 -show-inputs -show-outputs miter - +hierarchy -auto-top +#equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx ### TODO +equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx +miter -equiv -flatten -make_assert -make_outputs gold gate miter +sat -verify -prove-asserts -seq 10 -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 +select -assert-count 1 t:FDRE select -assert-count 1 t:DSP48E1 -select -assert-none t:BUFG t:DSP48E1 %% t:* %D +select -assert-none t:BUFG t:FDRE t:DSP48E1 %% t:* %D -- 2.30.2