support repeat loops with constant repeat counts outside of constant functions

diff --git a/frontends/ast/simplify.cc b/frontends/ast/simplify.cc
index 63b71b80010cd8a13907724c2355c4ed6ccc5607..76da5a97cfcc955c9e14f66784f536455a8e53a0 100644 (file)
--- a/frontends/ast/simplify.cc
+++ b/frontends/ast/simplify.cc
@@ -1030,7 +1030,26 @@ bool AstNode::simplify(bool const_fold, bool at_zero, bool in_lvalue, int stage,
                log_file_error(filename, linenum, "While loops are only allowed in constant functions!\n");
 
        if (type == AST_REPEAT)
-               log_file_error(filename, linenum, "Repeat loops are only allowed in constant functions!\n");
+       {
+               AstNode *count = children[0];
+               AstNode *body = children[1];
+
+               // eval count expression
+               while (count->simplify(true, false, false, stage, 32, true, false)) { }
+
+               if (count->type != AST_CONSTANT)
+                       log_file_error(filename, linenum, "Repeat loops outside must have constant repeat counts!\n");
+
+               // convert to a block with the body repeated n times
+               type = AST_BLOCK;
+               children.clear();
+               for (int i = 0; i < count->bitsAsConst().as_int(); i++)
+                       children.insert(children.begin(), body->clone());
+
+               delete count;
+               delete body;
+               did_something = true;
+       }
 
        // unroll for loops and generate-for blocks
        if ((type == AST_GENFOR || type == AST_FOR) && children.size() != 0)

diff --git a/tests/sat/counters-repeat.v b/tests/sat/counters-repeat.v
new file mode 100644 (file)
index 0000000..2ea4549
--- /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 (file)
index 0000000..b3dcfe0
--- /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
+