Fix crash on nonconsecutive repetition in implication consequent (#8612) (#8620)

docs/CONTRIBUTORS

@@ -75,6 +75,7 @@ dependabot[bot]
 Dercury
 Demin Han
 Diego Roux
+Doha Nam
 Dominick Grochowina
 Don Williamson
 Dragon-Git

src/V3AssertPre.cpp

@@ -1494,9 +1494,16 @@ private:
             }
             // Wrap existing PExpr body: if (antecedent) { <original body> } else { /* vacuous pass
             // */ }
+            // Only the statements are guarded; declarations stay directly in the block. After
+            // V3Fork moves the block's statements into a task, V3Task only handles variables
+            // that are direct statements of the task.
             AstBegin* const bodyp = pexprp->bodyp();
-            AstNode* const origStmtsp = bodyp->stmtsp()->unlinkFrBackWithNext();
-            AstIf* const guardp = new AstIf{flp, condp, origStmtsp};
+            AstIf* const guardp = new AstIf{flp, condp};
+            for (AstNode* stmtp = bodyp->stmtsp(); stmtp;) {
+                AstNode* const nextp = stmtp->nextp();
+                if (!VN_IS(stmtp, Var)) guardp->addThensp(stmtp->unlinkFrBack());
+                stmtp = nextp;
+            }
             bodyp->addStmtsp(guardp);
             nodep->replaceWith(pexprp);
             // Don't iterate pexprp here -- it was already iterated when created

test_regress/t/t_assert_nonconsec_rep.v

@@ -27,6 +27,10 @@ module t (
   int count_fail2 = 0;
   int count_fail3 = 0;
   int count_fail4 = 0;
+  int count_pass5 = 0;
+  int count_fail5 = 0;
+  int count_pass6 = 0;
+  int count_fail6 = 0;
 
   // Test 1: a[=2] |-> b (overlapping implication, 2 non-consecutive occurrences)
   assert property (@(posedge clk) a [= 2] |-> b)
@@ -44,6 +48,16 @@ module t (
   assert property (@(posedge clk) b [= 2])
   else count_fail4 <= count_fail4 + 1;
 
+  // Test 5: nonconsec rep as consequent of an overlapping implication (#8612).
+  // The antecedent holds every cycle, so no attempt is vacuous. Passes use a
+  // blocking increment, as several attempts can pass on the same edge.
+  assert property (@(posedge clk) cyc >= 0 |-> b [= 2]) count_pass5++;
+  else count_fail5 <= count_fail5 + 1;
+
+  // Test 6: nonconsec rep as consequent of a non-overlapping implication
+  assert property (@(posedge clk) cyc >= 0 |=> d [= 2]) count_pass6++;
+  else count_fail6 <= count_fail6 + 1;
+
   always @(posedge clk) begin
 `ifdef TEST_VERBOSE
     $write("[%0t] cyc==%0d crc=%x a=%b b=%b c=%b d=%b\n", $time, cyc, crc, a, b, c, d);
@@ -59,6 +73,10 @@ module t (
       `checkd(count_fail2, 27);  // Other sims: 32, one other: 25
       `checkd(count_fail3, 25);  // Other sims: 29, one other: 25
       `checkd(count_fail4, 0);
+      `checkd(count_pass5, 91);
+      `checkd(count_fail5, 0);
+      `checkd(count_pass6, 96);
+      `checkd(count_fail6, 0);
       $write("*-* All Finished *-*\n");
       $finish;
     end