Merge remote-tracking branch 'origin/master' into xc7srl

4 files changed, 51 insertions, 2 deletions

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
+
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