From: Eddie Hung <eddie@fpgeh.com>
Date: Sat, 7 Sep 2019 06:19:03 +0000 (-0700)
Subject: Update macc test
X-Git-Tag: working-ls180~1039^2~168
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e68507a71603553426a338bcffb0eccb1653436f;p=yosys.git

Update macc test
---

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