From 36d6db7f8aac6568acc2fb2d4ea5a5427d00d667 Mon Sep 17 00:00:00 2001
From: Eddie Hung <eddie@fpgeh.com>
Date: Wed, 11 Sep 2019 09:09:08 -0700
Subject: [PATCH] Extend test for RSTP and RSTM

---
 tests/xilinx/macc.v  | 36 ++++++++++++++++++++++++++++++++++--
 tests/xilinx/macc.ys | 17 ++++++++++++++++-
 2 files changed, 50 insertions(+), 3 deletions(-)

diff --git a/tests/xilinx/macc.v b/tests/xilinx/macc.v
index 0bb673316..c6ad2a578 100644
--- a/tests/xilinx/macc.v
+++ b/tests/xilinx/macc.v
@@ -35,7 +35,39 @@ always @(posedge clk)
 		adder_out <= old_result + mult_reg;
 	end
 
-	// Output accumulation result
-	assign accum_out = adder_out;
+// Output accumulation result
+assign accum_out = adder_out;
+
+endmodule
+
+// Adapted variant of above
+module macc2 # (parameter SIZEIN = 16, SIZEOUT = 40) (
+	input clk, ce, rst,
+	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 rst_reg;
+reg signed [2*SIZEIN-1:0] mult_reg;
+reg signed [SIZEOUT-1:0] adder_out, old_result;
+always @(posedge clk) begin
+	if (ce)
+	begin
+		a_reg <= a;
+		b_reg <= b;
+		mult_reg <= a_reg * b_reg;
+		rst_reg <= rst;
+		// Store accumulation result into a register
+		adder_out <= adder_out + mult_reg;
+	end
+    if (rst) begin
+		mult_reg <= 0;
+		adder_out <= 0;
+    end
+end
+
+// Output accumulation result
+assign accum_out = adder_out;
 
 endmodule
diff --git a/tests/xilinx/macc.ys b/tests/xilinx/macc.ys
index de408162c..294b83c69 100644
--- a/tests/xilinx/macc.ys
+++ b/tests/xilinx/macc.ys
@@ -1,6 +1,8 @@
 read_verilog macc.v
+design -save read
+
 proc
-hierarchy -auto-top
+hierarchy -top macc
 #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
@@ -11,3 +13,16 @@ select -assert-count 1 t:BUFG
 select -assert-count 1 t:FDRE
 select -assert-count 1 t:DSP48E1
 select -assert-none t:BUFG t:FDRE t:DSP48E1 %% t:* %D
+
+design -load read
+proc
+hierarchy -top macc2
+#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 macc2 # Constrain all select calls below inside the top module
+select -assert-count 1 t:BUFG
+select -assert-count 1 t:DSP48E1
+select -assert-none t:BUFG t:DSP48E1 %% t:* %D
-- 
2.30.2