3 files changed, 55 insertions, 1 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/sat/initval.v b/tests/sat/initval.v
index 5b661f8d6..81f71b5ba 100644
--- a/tests/sat/initval.v
+++ b/tests/sat/initval.v
@@ -1,6 +1,7 @@
-module test(input clk, input [3:0] bar, output [3:0] foo);
+module test(input clk, input [3:0] bar, output [3:0] foo, asdf);
   reg [3:0] foo = 0;
   reg [3:0] last_bar = 0;
+  reg [3:0] asdf = 4'b1xxx;
 
   always @*
     foo[1:0] <= bar[1:0];
@@ -11,5 +12,10 @@ module test(input clk, input [3:0] bar, output [3:0] foo);
   always @(posedge clk)
     last_bar <= bar;
 
+  always @(posedge clk)
+    asdf[3] <= bar[3];
+  always @*
+    asdf[2:0] = 3'b111;
+
   assert property (foo == {last_bar[3:2], bar[1:0]});
 endmodule