luke
/
verilator
mirror of https://github.com/verilator/verilator.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Lower sequence event controls via the cover sequence path

This commit is contained in:
Yilou Wang 2026-07-03 22:01:16 +02:00
parent 51c3681859
commit 951404eac7
11 changed files with 136 additions and 108 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

67
src/V3Assert.cpp
View File

@ -20,6 +20,7 @@
#include "V3AstUserAllocator.h"
#include "V3Stats.h"
#include "V3UniqueNames.h"
VL_DEFINE_DEBUG_FUNCTIONS;
@ -89,6 +90,61 @@ public:
explicit DefaultDisablePropagateVisitor(AstNetlist* nodep) { iterate(nodep); }
};
// Lower a sequence used as an event control ('@seq', IEEE 1800-2023 9.4.2.4) into a
// synthesized event plus an internal 'cover sequence' that fires the event on every
// end-of-match. Runs before V3AssertNfa so the sequence's automaton is built by the
// ordinary cover-sequence path; nothing sequence-event-specific reaches V3AssertNfa.
class SeqEventLowerVisitor final : public VNVisitor {
// STATE
AstNodeModule* m_modp = nullptr; // Current module
V3UniqueNames m_names{"__VseqEvent"}; // Synthesized event names
// VISITORS
void visit(AstNodeModule* nodep) override {
VL_RESTORER(m_modp);
m_modp = nodep;
iterateChildren(nodep);
}
void visit(AstSenItem* nodep) override {
AstFuncRef* const funcrefp = VN_CAST(nodep->sensp(), FuncRef);
if (funcrefp && VN_IS(funcrefp->taskp(), Sequence)) {
FileLine* const flp = nodep->fileline();
AstVar* const eventp = new AstVar{flp, VVarType::MODULETEMP, m_names.get(nodep),
m_modp->findBasicDType(VBasicDTypeKwd::EVENT)};
eventp->lifetime(VLifetime::STATIC_EXPLICIT);
m_modp->addStmtsp(eventp);
v3Global.setHasEvents();
funcrefp->unlinkFrBack();
nodep->sensp(new AstVarRef{flp, eventp, VAccess::READ});
// An automatic actual cannot be referenced from the module-level cover
const bool automaticActual = funcrefp->exists([](const AstNodeVarRef* refp) {
return refp->varp() && refp->varp()->lifetime().isAutomatic();
});
if (automaticActual) {
nodep->v3warn(E_UNSUPPORTED, "Unsupported: automatic variable as an argument"
" of a sequence used as an event control");
VN_AS(funcrefp->taskp(), Sequence)->isReferenced(false);
VL_DO_DANGLING(pushDeletep(funcrefp), funcrefp);
return;
}
AstFireEvent* const firep
= new AstFireEvent{flp, new AstVarRef{flp, eventp, VAccess::WRITE}, false};
AstCover* const coverp
= new AstCover{flp, new AstPropSpec{flp, nullptr, nullptr, funcrefp}, firep,
VAssertType::CONCURRENT};
coverp->isCoverSeq(true);
coverp->isSeqEvent(true);
m_modp->addStmtsp(coverp);
return;
}
iterateChildren(nodep);
}
void visit(AstNode* nodep) override { iterateChildren(nodep); }
public:
explicit SeqEventLowerVisitor(AstNetlist* nodep) { iterate(nodep); }
};
} // namespace
void V3AssertCommon::collectDefaultDisable(AstNetlist* nodep) {
@ -96,6 +152,11 @@ void V3AssertCommon::collectDefaultDisable(AstNetlist* nodep) {
{ DefaultDisablePropagateVisitor{nodep}; }
}
void V3AssertCommon::lowerSequenceEvents(AstNetlist* nodep) {
{ SeqEventLowerVisitor{nodep}; }
V3Global::dumpCheckGlobalTree("assertseqevent", 0, dumpTreeEitherLevel() >= 3);
}
//######################################################################
// AssertDeFutureVisitor
// If any AstFuture, then move all non-future varrefs to be one cycle behind,
@ -546,7 +607,11 @@ class AssertVisitor final : public VNVisitor {
bool passspGated = false;
if (const AstCover* const snodep = VN_CAST(nodep, Cover)) {
++m_statCover;
if (!v3Global.opt.coverageUser()) {
if (snodep->isSeqEvent()) {
// Synthesized driver for a sequence used as an event control; keep the
// action (the event fire) with no coverage bucket, independent of
// --coverage.
} else if (!v3Global.opt.coverageUser()) {
selfDestruct = true;
} else {
// V3Coverage assigned us a bucket to increment.

1
src/V3Assert.h
View File

@ -27,6 +27,7 @@
class V3AssertCommon final {
public:
static void collectDefaultDisable(AstNetlist* nodep) VL_MT_DISABLED;
static void lowerSequenceEvents(AstNetlist* nodep) VL_MT_DISABLED;
};
class V3Assert final {

91
src/V3AssertNfa.cpp
View File

@ -2071,7 +2071,6 @@ 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<const AstProperty*> m_inliningProps; // Recursion guard for inlineNamedProperty
// Wire match vertex and mid-window sources for a successful NFA build.
@ -2734,87 +2733,6 @@ class AssertNfaVisitor final : public VNVisitor {
UINFO(4, "NFA converted assertion at " << flp << endl);
}
// 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 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),
modp->findBasicDType(VBasicDTypeKwd::EVENT)};
eventp->lifetime(VLifetime::STATIC_EXPLICIT);
modp->addStmtsp(eventp);
v3Global.setHasEvents();
AstFuncRef* const funcrefp = VN_AS(senitemp->sensp()->unlinkFrBack(), FuncRef);
senitemp->sensp(new AstVarRef{flp, eventp, VAccess::READ});
// 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);
inlineAllSequenceRefs(specp->propp());
if (hoistClockedSeq(specp)) { // Unsupported clocking form, already reported
VL_DO_DANGLING(pushDeletep(specp), specp);
return;
}
// Inherit the module default clocking (IEEE 14.12, 16.15) when the
// sequence has none of its own.
if (!specp->sensesp() && m_defaultClockingp) {
specp->sensesp(m_defaultClockingp->sensesp()->cloneTree(true));
}
// A clockless sequence with no default clocking has no sampling edge.
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: 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));
} 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);
@ -2832,15 +2750,6 @@ 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();

5
src/V3AstNodeStmt.h
View File

@ -1612,6 +1612,9 @@ class AstCover final : public AstNodeCoverOrAssert {
// @astgen op3 := coverincsp: List[AstNode] // Coverage node
bool m_isCoverSeq = false; // 'cover sequence' (IEEE 1800-2023 16.14.3): fires per
// end-of-match, not per property success
bool m_isSeqEvent = false; // Synthesized to implement a sequence used as an event
// control (IEEE 1800-2023 9.4.2.4); its action fires the
// event on every end-of-match, independent of --coverage
public:
ASTGEN_MEMBERS_AstCover;
AstCover(FileLine* fl, AstNode* propp, AstNode* stmtsp, VAssertType type,
@ -1622,6 +1625,8 @@ public:
void dumpJson(std::ostream& str) const override;
bool isCoverSeq() const { return m_isCoverSeq; }
void isCoverSeq(bool flag) { m_isCoverSeq = flag; }
bool isSeqEvent() const { return m_isSeqEvent; }
void isSeqEvent(bool flag) { m_isSeqEvent = flag; }
};
class AstRestrict final : public AstNodeCoverOrAssert {
public:

2
src/V3AstNodes.cpp
View File

@ -2226,9 +2226,11 @@ void AstNodeCoverOrAssert::dumpJson(std::ostream& str) const {
void AstCover::dump(std::ostream& str) const {
this->AstNodeCoverOrAssert::dump(str);
if (isCoverSeq()) str << " [COVERSEQ]";
if (isSeqEvent()) str << " [SEQEVENT]";
}
void AstCover::dumpJson(std::ostream& str) const {
dumpJsonBoolFuncIf(str, isCoverSeq);
dumpJsonBoolFuncIf(str, isSeqEvent);
this->AstNodeCoverOrAssert::dumpJson(str);
}
void AstClocking::dump(std::ostream& str) const {

1
src/Verilator.cpp
View File

@ -261,6 +261,7 @@ static void process() {
// Assertion insertion
// After we've added block coverage, but before other nasty transforms
V3AssertCommon::collectDefaultDisable(v3Global.rootp());
V3AssertCommon::lowerSequenceEvents(v3Global.rootp());
V3AssertNfa::assertNfaAll(v3Global.rootp());
// V3AssertProp removed: NFA subsumes multi-cycle property lowering.
// Unsupported constructs fall through to V3AssertPre.

18
test_regress/t/t_assert_seq_event.v
View File

@ -14,9 +14,10 @@ module t (
);
int unsigned crc = 32'h1;
bit a, b, c;
bit a1, a2, b1;
bit a1, a2, a3, b1;
int cyc = 0;
int seq_hits = 0, seq_hits2 = 0, ref_hits = 0, one_hits = 0, dc_hits = 0;
int rng_hits = 0, rng_ref = 0;
// verilog_format: off // verible does not support clocking events inside sequence declarations
sequence seq;
@ -26,6 +27,10 @@ module t (
sequence seq_one;
@(posedge clk) a;
endsequence
sequence seq_rng;
@(posedge clk) a ##[1:3] b;
endsequence
// verilog_format: on
// seq_dc has no clocking event, so it inherits the default clocking and must
@ -41,6 +46,9 @@ module t (
// (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.
// rng_hits waits on the ranged form: end points at posedge N when b@N and a@N-d
// for any d in 1..3; simultaneous end points resume a blocked waiter once, so
// rng_ref counts cycles with at least one end point.
initial forever begin
@seq;
seq_hits = seq_hits + 1;
@ -57,9 +65,15 @@ module t (
@seq_dc;
dc_hits = dc_hits + 1;
end
initial forever begin
@seq_rng;
rng_hits = rng_hits + 1;
end
always @(posedge clk) begin
if (a2 && b1 && c) ref_hits = ref_hits + 1;
if (b && (a1 || a2 || a3)) rng_ref = rng_ref + 1;
a3 <= a2;
a2 <= a1;
a1 <= a;
b1 <= b;
@ -84,6 +98,8 @@ module t (
`checkd(ref_hits, 14);
`checkd(one_hits, 30);
`checkd(dc_hits, 14);
`checkd(rng_hits, 26);
`checkd(rng_ref, 26);
$write("*-* All Finished *-*\n");
end
endmodule

17
test_regress/t/t_assert_seq_event_unsup.out
View File

@ -1,11 +1,14 @@
%Error-UNSUPPORTED: t/t_assert_seq_event_unsup.v:28:6: Unsupported: '@' event control on a sequence without a clocking event
28 | @s_clockless;
| ^~~~~~~~~~~
%Error-UNSUPPORTED: t/t_assert_seq_event_unsup.v:25:7: Unsupported: automatic variable as an argument of a sequence used as an event control
: ... note: In instance 't'
25 | @(s_arg(x));
| ^~~~~
... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest
%Error-UNSUPPORTED: t/t_assert_seq_event_unsup.v:19:5: Unsupported: non-edge clocking event on a sequence; use an edge such as @(posedge clk)
19 | @(g) a ##1 b;
%Error-UNSUPPORTED: t/t_assert_seq_event_unsup.v:15:5: Unsupported: non-edge clocking event on a sequence; use an edge such as @(posedge clk)
: ... note: In instance 't'
15 | @(g) a ##1 b;
| ^
%Error-UNSUPPORTED: t/t_assert_seq_event_unsup.v:30:6: Unsupported: this sequence form referenced by an '@' event control
30 | @s_noncons;
%Error-UNSUPPORTED: t/t_assert_seq_event_unsup.v:29:6: Unsupported: Unclocked assertion
: ... note: In instance 't'
29 | @s_nonedge;
| ^~~~~~~~~
%Error: Exiting due to

16
test_regress/t/t_assert_seq_event_unsup.v
View File

@ -11,22 +11,22 @@ module t (
logic g = 0;
// verilog_format: off
sequence s_clockless;
a ##1 b;
endsequence
sequence s_nonedge;
@(g) a ##1 b;
endsequence
sequence s_noncons;
@(posedge clk) a[=2];
sequence s_arg(x);
@(posedge clk) x;
endsequence
// verilog_format: on
task automatic f;
bit x = 1;
@(s_arg(x));
endtask
initial begin
@s_clockless;
@s_nonedge;
@s_noncons;
f();
end
endmodule

15
test_regress/t/t_debug_emitv.out
View File

@ -1318,6 +1318,21 @@ module Vt_debug_emitv_sub;
endfunction
real r;
endmodule
module Vt_debug_emitv_seq_event;
input logic clk;
bit a;
bit b;
bit c;
sequence sq;
@(posedge clk) a##1 b##1 c
endsequence
initial begin
begin
???? // EVENTCONTROL
@( sq())end
end
endmodule
package Vt_debug_emitv_p;
logic pkgvar;
endpackage

11
test_regress/t/t_debug_emitv.v
View File

@ -138,6 +138,7 @@ module t (/*AUTOARG*/
endfunction
sub sub(.*);
seq_event seq_event(.*);
initial begin
int other;
@ -443,6 +444,16 @@ module sub(input logic clk);
real r;
endmodule
module seq_event(input logic clk);
bit a, b, c;
sequence sq;
@(posedge clk) a ##1 b ##1 c;
endsequence
initial begin
@sq;
end
endmodule
package p;
logic pkgvar;
endpackage