ready for pr

src/V3AssertNfa.cpp

@@ -2734,14 +2734,12 @@ class AssertNfaVisitor final : public VNVisitor {
         UINFO(4, "NFA converted assertion at " << flp << endl);
     }
 
-    // IEEE 1800-2023 9.4.2.4: a sequence instance used as an event control
+    // IEEE 1800-2023 9.4.2.4: a sequence used as an event control (`@seq`)
-    // (`@seq`) triggers when the sequence reaches its end point. Lower it to a
+    // triggers each time the sequence reaches an end point. Lower it to a
     // named-event wait: synthesize an `event`, re-point the sensitivity at it,
     // and add a clocked monitor `always @(clk) if (end-of-match) -> event`. The
-    // match signal is the sequence's NFA terminal-active (the same per-cycle
+    // match is the NFA terminal-active a `cover sequence` fires on, so the event
-    // match a `cover sequence` fires on), so the event fires on every end point,
+    // fires on every end point, including overlapping ones.
-    // including overlapping/consecutive attempts -- unlike a bare-sequence assert
-    // whose pass action is suppressed on cycles where a parallel attempt rejects.
     void buildSeqEventMonitor(AstNodeModule* modp, AstSenItem* senitemp) {
         FileLine* const flp = senitemp->fileline();
         AstVar* const eventp = new AstVar{flp, VVarType::MODULETEMP, m_seqEventNames.get(senitemp),
@@ -2750,15 +2748,12 @@ class AssertNfaVisitor final : public VNVisitor {
         modp->addStmtsp(eventp);
         v3Global.setHasEvents();
 
-        // Detach the sequence reference and re-point the wait at the new event.
         AstFuncRef* const funcrefp = VN_AS(senitemp->sensp()->unlinkFrBack(), FuncRef);
         senitemp->sensp(new AstVarRef{flp, eventp, VAccess::READ});
 
-        // Reuse the assertion machinery to inline the sequence body and hoist
+        // Inline the referenced sequence, then any nested refs. Iterate the member
-        // its clocking event; this also clears the sequence's isReferenced flag.
+        // specp->propp(), not the freshly-new'd specp, to dodge a gcc -Warray-bounds
-        // Inline the referenced sequence first, then any nested sequence refs in
+        // false positive.
-        // its body -- foreaching over specp->propp() (a member access) rather than
-        // the freshly allocated specp keeps gcc -Warray-bounds from a false match.
         AstSequence* const seqp = VN_AS(funcrefp->taskp(), Sequence);
         AstPropSpec* const specp = new AstPropSpec{flp, nullptr, nullptr, funcrefp};
         inlineSequenceRef(funcrefp, seqp);
@@ -2767,9 +2762,7 @@ class AssertNfaVisitor final : public VNVisitor {
             VL_DO_DANGLING(pushDeletep(specp), specp);
             return;
         }
-        // A sequence used as an event must carry its own clocking event; a
+        // A clockless sequence has no sampling edge; require an explicit clock.
-        // clockless sequence is illegal here even under a module default clocking
-        // (confirmed against Questa), unlike one embedded in an assert property.
         if (!specp->sensesp()) {
             specp->v3warn(E_UNSUPPORTED,
                           "Unsupported: '@' event control on a sequence without a clocking event");
@@ -2780,9 +2773,8 @@ class AssertNfaVisitor final : public VNVisitor {
         UASSERT_OBJ(bodyp, specp, "Sequence body must be an expression");
         AstSenTree* const senTreep = new AstSenTree{flp, specp->sensesp()->cloneTree(true)};
 
-        // End-of-match signal: a single-cycle sequence matches on the sampled
+        // End-of-match: sampled boolean for a single-cycle sequence, NFA
-        // boolean at the clock; a multi-cycle sequence matches on the NFA
+        // terminal-active for a multi-cycle one.
-        // terminal-active (the per-cycle end point a `cover sequence` fires on).
         AstNodeExpr* matchp = nullptr;
         if (!hasMultiCycleExpr(bodyp)) {
             matchp = sampled(bodyp->cloneTreePure(false));

test_regress/t/t_assert_seq_event.v

@@ -28,27 +28,23 @@ module t (
   endsequence
   // verilog_format: on
 
-  // Feature under test: a sequence referenced outside an assertion via the `@`
+  // A sequence used as an `@` event control resumes once per sequence end point
-  // event control resumes once per sequence end point (IEEE 1800-2023 9.4.2.4).
+  // (IEEE 1800-2023 9.4.2.4). seq_hits/seq_hits2 are two waiters on the same
+  // multi-cycle sequence; ref_hits is an independent shift-register oracle (end
+  // point at posedge N when a@N-2, b@N-1, c@N); one_hits is the single-cycle case.
   initial forever begin
     @seq;
     seq_hits = seq_hits + 1;
   end
-
-  // A second waiter on the SAME sequence must see exactly the same end points.
   initial forever begin
     @seq;
     seq_hits2 = seq_hits2 + 1;
   end
-
-  // Single-cycle sequence end point: resumes whenever `a` is sampled true.
   initial forever begin
     @seq_one;
     one_hits = one_hits + 1;
   end
 
-  // Independent oracle: an end point lands at posedge N when the sampled values
-  // give a at N-2, b at N-1, c at N.
   always @(posedge clk) begin
     if (a2 && b1 && c) ref_hits = ref_hits + 1;
     a2 <= a1;
@@ -56,9 +52,9 @@ module t (
     b1 <= b;
   end
 
-  // Bits a/b/c are spaced past the ##2 window (crc[0]/crc[4]/crc[8]) so the
+  // a/b/c are spaced to crc[0]/crc[4]/crc[8] -- past the ##2 window -- so the
-  // left-shift LFSR does not correlate a@T, b@T+1, c@T+2 into one bit; the
+  // left-shift LFSR cannot correlate a@T, b@T+1, c@T+2 into one bit; otherwise
-  // multi-cycle end-point machinery is then genuinely exercised.
+  // the multi-cycle end-point machinery would collapse into a triviality.
   always @(posedge clk) begin
     cyc <= cyc + 1;
     crc <= {crc[30:0], crc[31] ^ crc[21] ^ crc[1] ^ crc[0]};
@@ -69,12 +65,11 @@ module t (
   end
 
   // Counts read in final (Postponed) to avoid same-timestep races.
-  // Concrete Verilator counts; Questa: seq_hits=14 ref_hits=14 one_hits=30
   final begin
-    `checkd(seq_hits, ref_hits);
+    `checkd(seq_hits, 14);  // Questa: 14
-    `checkd(seq_hits2, seq_hits);
+    `checkd(seq_hits2, 14);  // Questa: 14
-    `checkd(seq_hits, 14);
+    `checkd(ref_hits, 14);  // Questa: 14
-    `checkd(one_hits, 30);
+    `checkd(one_hits, 30);  // Questa: 30
     $write("*-* All Finished *-*\n");
   end
 endmodule