diff --git a/src/V3AssertNfa.cpp b/src/V3AssertNfa.cpp index a495a7d10..07ba3e27f 100644 --- a/src/V3AssertNfa.cpp +++ b/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 - // (`@seq`) triggers when the sequence reaches its end point. Lower it to a + // IEEE 1800-2023 9.4.2.4: a sequence used as an event control (`@seq`) + // 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 a `cover sequence` fires on), so the event fires on every end point, - // including overlapping/consecutive attempts -- unlike a bare-sequence assert - // whose pass action is suppressed on cycles where a parallel attempt rejects. + // match is the NFA terminal-active a `cover sequence` fires on, so the event + // fires on every end point, including overlapping ones. 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 - // its clocking event; this also clears the sequence's isReferenced flag. - // Inline the referenced sequence first, then any nested sequence refs in - // its body -- foreaching over specp->propp() (a member access) rather than - // the freshly allocated specp keeps gcc -Warray-bounds from a false match. + // Inline the referenced sequence, then any nested refs. Iterate the member + // specp->propp(), not the freshly-new'd specp, to dodge a gcc -Warray-bounds + // false positive. 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 - // clockless sequence is illegal here even under a module default clocking - // (confirmed against Questa), unlike one embedded in an assert property. + // A clockless sequence has no sampling edge; require an explicit clock. 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 - // boolean at the clock; a multi-cycle sequence matches on the NFA - // terminal-active (the per-cycle end point a `cover sequence` fires on). + // End-of-match: sampled boolean for a single-cycle sequence, NFA + // terminal-active for a multi-cycle one. AstNodeExpr* matchp = nullptr; if (!hasMultiCycleExpr(bodyp)) { matchp = sampled(bodyp->cloneTreePure(false)); diff --git a/test_regress/t/t_assert_seq_event.v b/test_regress/t/t_assert_seq_event.v index 87e4170ef..2f912c5b4 100644 --- a/test_regress/t/t_assert_seq_event.v +++ b/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 `@` - // event control resumes once per sequence end point (IEEE 1800-2023 9.4.2.4). + // A sequence used as an `@` event control resumes once per sequence end point + // (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 - // left-shift LFSR does not correlate a@T, b@T+1, c@T+2 into one bit; the - // multi-cycle end-point machinery is then genuinely exercised. + // a/b/c are spaced to crc[0]/crc[4]/crc[8] -- past the ##2 window -- so the + // left-shift LFSR cannot correlate a@T, b@T+1, c@T+2 into one bit; otherwise + // 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_hits2, seq_hits); - `checkd(seq_hits, 14); - `checkd(one_hits, 30); + `checkd(seq_hits, 14); // Questa: 14 + `checkd(seq_hits2, 14); // Questa: 14 + `checkd(ref_hits, 14); // Questa: 14 + `checkd(one_hits, 30); // Questa: 30 $write("*-* All Finished *-*\n"); end endmodule