From 2b836858efa53e41d738fcf566a130f0acaff3a3 Mon Sep 17 00:00:00 2001 From: Yilou Wang Date: Thu, 25 Jun 2026 20:49:32 +0200 Subject: [PATCH] Support a sequence used as an event control --- src/V3AssertNfa.cpp | 89 +++++++++++++++++++++ test_regress/t/t_assert_seq_event.py | 18 +++++ test_regress/t/t_assert_seq_event.v | 80 ++++++++++++++++++ test_regress/t/t_assert_seq_event_unsup.out | 11 +++ test_regress/t/t_assert_seq_event_unsup.py | 16 ++++ test_regress/t/t_assert_seq_event_unsup.v | 37 +++++++++ 6 files changed, 251 insertions(+) create mode 100755 test_regress/t/t_assert_seq_event.py create mode 100644 test_regress/t/t_assert_seq_event.v create mode 100644 test_regress/t/t_assert_seq_event_unsup.out create mode 100755 test_regress/t/t_assert_seq_event_unsup.py create mode 100644 test_regress/t/t_assert_seq_event_unsup.v diff --git a/src/V3AssertNfa.cpp b/src/V3AssertNfa.cpp index b6ec6964f..4eaef46dd 100644 --- a/src/V3AssertNfa.cpp +++ b/src/V3AssertNfa.cpp @@ -2071,6 +2071,7 @@ class AssertNfaVisitor final : public VNVisitor { V3UniqueNames m_propVarNames{"__Vpropvar"}; // Property-local variable names V3UniqueNames m_disableCntNames{"__VnfaDis"}; // Disable-iff counter names V3UniqueNames m_propTempNames{"__VnfaSampled"}; // Hoisted $sampled(propp) temps + V3UniqueNames m_seqEventNames{"__VseqEvent"}; // Synthesized `@seq` end-point events std::set m_inliningProps; // Recursion guard for inlineNamedProperty // Wire match vertex and mid-window sources for a successful NFA build. @@ -2733,6 +2734,85 @@ 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 + // 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. + void buildSeqEventMonitor(AstNodeModule* modp, AstSenItem* senitemp) { + FileLine* const flp = senitemp->fileline(); + AstVar* const eventp = new AstVar{flp, VVarType::MODULETEMP, m_seqEventNames.get(senitemp), + modp->findBasicDType(VBasicDTypeKwd::EVENT)}; + eventp->lifetime(VLifetime::STATIC_EXPLICIT); + 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. + AstPropSpec* const specp = new AstPropSpec{flp, nullptr, nullptr, funcrefp}; + inlineAllSequenceRefs(specp); + if (hoistClockedSeq(specp)) { // Unsupported clocking form, already reported + 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. + if (!specp->sensesp()) { + specp->v3warn(E_UNSUPPORTED, + "Unsupported: '@' event control on a sequence without a clocking event"); + VL_DO_DANGLING(pushDeletep(specp), specp); + return; + } + AstNodeExpr* const bodyp = VN_CAST(specp->propp(), NodeExpr); + 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). + AstNodeExpr* matchp = nullptr; + if (!hasMultiCycleExpr(bodyp)) { + matchp = sampled(bodyp->cloneTreePure(false)); + } else { + const PropertyParts parts = decomposeProperty(bodyp); + UASSERT_OBJ(parts.seqExprp, bodyp, "Sequence body must be an expression"); + SvaGraph graph; + SvaNfaBuilder builder{graph, modp, m_propTempNames, /*isCoverSeq=*/false}; + const BuildResult result + = buildAssertionGraph(builder, graph, parts.seqExprp, parts, flp); + if (!result.valid()) { + if (!result.errorEmitted) { + specp->v3warn( + E_UNSUPPORTED, + "Unsupported: this sequence form referenced by an '@' event control"); + } + VL_DO_DANGLING(pushDeletep(senTreep), senTreep); + VL_DO_DANGLING(pushDeletep(specp), specp); + return; + } + wireMatchAndMidSources(graph, result, flp); + AstNodeExpr* const triggerp = new AstConst{flp, AstConst::BitTrue{}}; + matchp = m_loweringp->lower(flp, graph, triggerp, senTreep, result.finalCondp, + /*isCover=*/true); + VL_DO_DANGLING(pushDeletep(triggerp), triggerp); + if (result.finalCondp && !result.finalCondp->backp()) pushDeletep(result.finalCondp); + } + + AstFireEvent* const firep + = new AstFireEvent{flp, new AstVarRef{flp, eventp, VAccess::WRITE}, false}; + modp->addStmtsp(new AstAlways{flp, VAlwaysKwd::ALWAYS, senTreep, + new AstIf{flp, matchp, firep, nullptr}}); + VL_DO_DANGLING(pushDeletep(specp), specp); + } + // VISITORS void visit(AstNodeModule* nodep) override { VL_RESTORER(m_modp); @@ -2750,6 +2830,15 @@ class AssertNfaVisitor final : public VNVisitor { if (nodep->isDefault() && !m_defaultClockingp) m_defaultClockingp = nodep; iterateChildren(nodep); } + void visit(AstSenItem* nodep) override { + if (const AstFuncRef* const funcrefp = VN_CAST(nodep->sensp(), FuncRef)) { + if (VN_IS(funcrefp->taskp(), Sequence)) { + buildSeqEventMonitor(m_modp, nodep); + return; + } + } + iterateChildren(nodep); + } void visit(AstGenBlock* nodep) override { VL_RESTORER(m_defaultDisablep); m_defaultDisablep = nodep->defaultDisablep(); diff --git a/test_regress/t/t_assert_seq_event.py b/test_regress/t/t_assert_seq_event.py new file mode 100755 index 000000000..e8cdbc78d --- /dev/null +++ b/test_regress/t/t_assert_seq_event.py @@ -0,0 +1,18 @@ +#!/usr/bin/env python3 +# DESCRIPTION: Verilator: Verilog Test driver/expect definition +# +# This program is free software; you can redistribute it and/or modify it +# under the terms of either the GNU Lesser General Public License Version 3 +# or the Perl Artistic License Version 2.0. +# SPDX-FileCopyrightText: 2026 Wilson Snyder +# SPDX-License-Identifier: LGPL-3.0-only OR Artistic-2.0 + +import vltest_bootstrap + +test.scenarios('vlt') + +test.compile(verilator_flags2=['--timing']) + +test.execute() + +test.passes() diff --git a/test_regress/t/t_assert_seq_event.v b/test_regress/t/t_assert_seq_event.v new file mode 100644 index 000000000..87e4170ef --- /dev/null +++ b/test_regress/t/t_assert_seq_event.v @@ -0,0 +1,80 @@ +// DESCRIPTION: Verilator: Verilog Test module +// +// This file ONLY is placed under the Creative Commons Public Domain. +// SPDX-FileCopyrightText: 2026 PlanV GmbH +// SPDX-License-Identifier: CC0-1.0 + +// verilog_format: off +`define stop $stop +`define checkd(gotv,expv) do if ((gotv) !== (expv)) begin $write("%%Error: %s:%0d: got=%0d exp=%0d (%s !== %s)\n", `__FILE__,`__LINE__, (gotv), (expv), `"gotv`", `"expv`"); `stop; end while(0); +// verilog_format: on + +module t ( + input clk +); + int unsigned crc = 32'h1; + bit a, b, c; + bit a1, a2, b1; + int cyc = 0; + int seq_hits = 0, seq_hits2 = 0, ref_hits = 0, one_hits = 0; + + // verilog_format: off // verible does not support clocking events inside sequence declarations + sequence seq; + @(posedge clk) a ##1 b ##1 c; + endsequence + + sequence seq_one; + @(posedge clk) a; + 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). + 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; + a1 <= a; + 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. + always @(posedge clk) begin + cyc <= cyc + 1; + crc <= {crc[30:0], crc[31] ^ crc[21] ^ crc[1] ^ crc[0]}; + a <= crc[0]; + b <= crc[4]; + c <= crc[8]; + if (cyc == 60) $finish; + 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); + $write("*-* All Finished *-*\n"); + end +endmodule diff --git a/test_regress/t/t_assert_seq_event_unsup.out b/test_regress/t/t_assert_seq_event_unsup.out new file mode 100644 index 000000000..27270c9fc --- /dev/null +++ b/test_regress/t/t_assert_seq_event_unsup.out @@ -0,0 +1,11 @@ +%Error-UNSUPPORTED: t/t_assert_seq_event_unsup.v:33:6: Unsupported: '@' event control on a sequence without a clocking event + 33 | @s_unclocked; + | ^~~~~~~~~~~ + ... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest +%Error-UNSUPPORTED: t/t_assert_seq_event_unsup.v:24:5: Unsupported: non-edge clocking event on a sequence; use an edge such as @(posedge clk) + 24 | @(g) a ##1 b; + | ^ +%Error-UNSUPPORTED: t/t_assert_seq_event_unsup.v:35:6: Unsupported: this sequence form referenced by an '@' event control + 35 | @s_noncons; + | ^~~~~~~~~ +%Error: Exiting due to diff --git a/test_regress/t/t_assert_seq_event_unsup.py b/test_regress/t/t_assert_seq_event_unsup.py new file mode 100755 index 000000000..f051d14b9 --- /dev/null +++ b/test_regress/t/t_assert_seq_event_unsup.py @@ -0,0 +1,16 @@ +#!/usr/bin/env python3 +# DESCRIPTION: Verilator: Verilog Test driver/expect definition +# +# This program is free software; you can redistribute it and/or modify it +# under the terms of either the GNU Lesser General Public License Version 3 +# or the Perl Artistic License Version 2.0. +# SPDX-FileCopyrightText: 2026 Wilson Snyder +# SPDX-License-Identifier: LGPL-3.0-only OR Artistic-2.0 + +import vltest_bootstrap + +test.scenarios('vlt') + +test.lint(expect_filename=test.golden_filename, verilator_flags2=['--timing'], fails=True) + +test.passes() diff --git a/test_regress/t/t_assert_seq_event_unsup.v b/test_regress/t/t_assert_seq_event_unsup.v new file mode 100644 index 000000000..a43b33477 --- /dev/null +++ b/test_regress/t/t_assert_seq_event_unsup.v @@ -0,0 +1,37 @@ +// DESCRIPTION: Verilator: Verilog Test module +// +// This file ONLY is placed under the Creative Commons Public Domain. +// SPDX-FileCopyrightText: 2026 PlanV GmbH +// SPDX-License-Identifier: CC0-1.0 + +module t ( + input clk +); + bit a, b; + logic g = 0; + + // A module default clocking does NOT make a clockless sequence legal as an + // event (confirmed against Questa); s_unclocked below stays E_UNSUPPORTED. + default clocking @(posedge clk); + endclocking + + // verilog_format: off + sequence s_unclocked; + a ##1 b; + endsequence + + sequence s_nonedge; + @(g) a ##1 b; + endsequence + + sequence s_noncons; + @(posedge clk) a[=2]; + endsequence + // verilog_format: on + + initial begin + @s_unclocked; + @s_nonedge; + @s_noncons; + end +endmodule