From 5855024cccfbcb1919e3225f519bc9f0421c4056 Mon Sep 17 00:00:00 2001
From: Zachary Snow <zach@zachjs.com>
Date: Tue, 9 Apr 2019 12:28:32 -0400
Subject: support repeat loops with constant repeat counts outside of constant
 functions

---
 tests/sat/counters-repeat.v  | 38 ++++++++++++++++++++++++++++++++++++++
 tests/sat/counters-repeat.ys | 10 ++++++++++
 2 files changed, 48 insertions(+)
 create mode 100644 tests/sat/counters-repeat.v
 create mode 100644 tests/sat/counters-repeat.ys

(limited to 'tests')

diff --git a/tests/sat/counters-repeat.v b/tests/sat/counters-repeat.v
new file mode 100644
index 000000000..2ea45499a
--- /dev/null
+++ b/tests/sat/counters-repeat.v
@@ -0,0 +1,38 @@
+// coverage for repeat loops outside of constant functions
+
+module counter1(clk, rst, ping);
+	input clk, rst;
+	output ping;
+	reg [31:0] count;
+
+	always @(posedge clk) begin
+		if (rst)
+			count <= 0;
+		else
+			count <= count + 1;
+	end
+
+	assign ping = &count;
+endmodule
+
+module counter2(clk, rst, ping);
+	input clk, rst;
+	output ping;
+	reg [31:0] count;
+
+	integer i;
+	reg carry;
+
+	always @(posedge clk) begin
+		carry = 1;
+		i = 0;
+		repeat (32) begin
+			count[i] <= !rst & (count[i] ^ carry);
+			carry = count[i] & carry;
+			i = i+1;
+		end
+	end
+
+	assign ping = &count;
+endmodule
+
diff --git a/tests/sat/counters-repeat.ys b/tests/sat/counters-repeat.ys
new file mode 100644
index 000000000..b3dcfe08a
--- /dev/null
+++ b/tests/sat/counters-repeat.ys
@@ -0,0 +1,10 @@
+
+read_verilog counters-repeat.v
+proc; opt
+
+expose -shared counter1 counter2
+miter -equiv -make_assert -make_outputs counter1 counter2 miter
+
+cd miter; flatten; opt
+sat -verify -prove-asserts -tempinduct -set-at 1 in_rst 1 -seq 1 -show-inputs -show-outputs
+
-- 
cgit v1.2.3


From d38f0c1a96c036df4ef67ad2f945dd229e1c3b8e Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Sun, 21 Apr 2019 11:40:20 +0200
Subject: Fix tests

Signed-off-by: Clifford Wolf <clifford@clifford.at>
---
 tests/tools/autotest.sh    | 4 ++--
 tests/various/hierarchy.sh | 1 +
 2 files changed, 3 insertions(+), 2 deletions(-)

(limited to 'tests')

diff --git a/tests/tools/autotest.sh b/tests/tools/autotest.sh
index f3dac504e..bb9c3bfb5 100755
--- a/tests/tools/autotest.sh
+++ b/tests/tools/autotest.sh
@@ -7,7 +7,7 @@ use_modelsim=false
 verbose=false
 keeprunning=false
 makejmode=false
-frontend="verilog"
+frontend="verilog -noblackbox"
 backend_opts="-noattr -noexpr -siminit"
 autotb_opts=""
 include_opts=""
@@ -137,7 +137,7 @@ do
 			egrep -v '^\s*`timescale' ../$fn > ${bn}_ref.${ext}
 		else
 			"$toolsdir"/../../yosys -f "$frontend $include_opts" -b "verilog" -o ${bn}_ref.v ../${fn}
-			frontend="verilog"
+			frontend="verilog -noblackbox"
 		fi
 
 		if [ ! -f ../${bn}_tb.v ]; then
diff --git a/tests/various/hierarchy.sh b/tests/various/hierarchy.sh
index d33a247be..9dbd1c89f 100644
--- a/tests/various/hierarchy.sh
+++ b/tests/various/hierarchy.sh
@@ -53,6 +53,7 @@ echo -n "  no explicit top - "
     module noTop(a, y);
       input a;
       output [31:0] y;
+      assign y = a;
     endmodule
   EOV
   hierarchy -auto-top
-- 
cgit v1.2.3