From 4100825b810408e25b1773cb1e57d25821f164b5 Mon Sep 17 00:00:00 2001
From: Eddie Hung <eddie@fpgeh.com>
Date: Thu, 19 Sep 2019 22:39:15 -0700
Subject: [PATCH] Add more complicated macc testcase

---
 tests/ice40/macc.v  | 22 ++++++++++++++++++++++
 tests/ice40/macc.ys | 24 ++++++++++++++++++------
 2 files changed, 40 insertions(+), 6 deletions(-)

diff --git a/tests/ice40/macc.v b/tests/ice40/macc.v
index 757c36a66..6f68e7500 100644
--- a/tests/ice40/macc.v
+++ b/tests/ice40/macc.v
@@ -23,3 +23,25 @@ begin
     end
 end
 endmodule
+
+module top2(clk,a,b,c,hold);
+parameter A_WIDTH = 6 /*4*/;
+parameter B_WIDTH = 6 /*3*/;
+input hold;
+input clk;
+input signed [(A_WIDTH - 1):0] a;
+input signed [(B_WIDTH - 1):0] b;
+output signed [(A_WIDTH + B_WIDTH - 1):0] c;
+reg signed [A_WIDTH-1:0] reg_a;
+reg signed [B_WIDTH-1:0] reg_b;
+reg [(A_WIDTH + B_WIDTH - 1):0] reg_tmp_c;
+assign c = reg_tmp_c;
+always @(posedge clk)
+begin
+    if (!hold) begin
+        reg_a <= a;
+        reg_b <= b;
+        reg_tmp_c <= reg_a * reg_b + c;
+    end
+end
+endmodule
diff --git a/tests/ice40/macc.ys b/tests/ice40/macc.ys
index 0f4c19be5..fd30e79c5 100644
--- a/tests/ice40/macc.ys
+++ b/tests/ice40/macc.ys
@@ -1,13 +1,25 @@
 read_verilog macc.v
 proc
+design -save read
+
 hierarchy -top top
-#equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 -dsp # equivalency check
-
-equiv_opt -run :prove -map +/ice40/cells_sim.v synth_ice40 -dsp
-async2sync
-equiv_opt -run prove: -assert null
-
+equiv_opt -assert -multiclock -map +/ice40/cells_sim.v synth_ice40 -dsp # equivalency check
 design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
 cd top # Constrain all select calls below inside the top module
 select -assert-count 1 t:SB_MAC16
 select -assert-none t:SB_MAC16 %% t:* %D
+
+design -load read
+hierarchy -top top2
+
+#equiv_opt -multiclock -assert -map +/ice40/cells_sim.v synth_ice40 -dsp # equivalency check
+
+equiv_opt -run :prove -multiclock -assert -map +/ice40/cells_sim.v synth_ice40 -dsp # equivalency check
+clk2fflogic
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -set-init-zero -seq 4 -verify -prove-asserts -show-ports miter
+
+design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
+cd top2 # Constrain all select calls below inside the top module
+select -assert-count 1 t:SB_MAC16
+select -assert-none t:SB_MAC16 %% t:* %D