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

Support named sequence declarations and instances in assertions (#7283)

This commit is contained in:
Yilou Wang 2026-03-20 15:24:46 +01:00 committed by GitHub
parent 25c3bc814e
commit a8bccab8e6
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
8 changed files with 149 additions and 97 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

60
src/V3AssertPre.cpp
View File

@ -63,6 +63,7 @@ private:
bool m_inSynchDrive = false; // True if in synchronous drive
std::vector<AstVarXRef*> m_xrefsp; // list of xrefs that need name fixup
bool m_inPExpr = false; // True if in AstPExpr
std::vector<AstSequence*> m_seqsToCleanup; // Sequences to clean up after traversal
// METHODS
@ -88,6 +89,12 @@ private:
}
return newp;
}
AstNodeExpr* getSequenceBodyExprp(const AstSequence* const seqp) const {
// The statements in AstSequence are optional AstVar (ports) followed by body expr.
AstNode* bodyp = seqp->stmtsp();
while (bodyp && VN_IS(bodyp, Var)) bodyp = bodyp->nextp();
return VN_CAST(bodyp, NodeExpr);
}
AstPropSpec* getPropertyExprp(const AstProperty* const propp) {
// The only statements possible in AstProperty are AstPropSpec (body)
// and AstVar (arguments).
@ -95,6 +102,32 @@ private:
while (VN_IS(propExprp, Var)) propExprp = propExprp->nextp();
return VN_CAST(propExprp, PropSpec);
}
void substituteSequenceCall(AstFuncRef* funcrefp, AstSequence* seqp) {
// IEEE 1800-2023 16.7 (sequence declarations), 16.8 (sequence instances)
// Inline the sequence body at the call site, replacing the FuncRef
AstNodeExpr* bodyExprp = getSequenceBodyExprp(seqp);
UASSERT_OBJ(bodyExprp, funcrefp, "Sequence has no body expression");
// Clone the body expression since the sequence may be referenced multiple times
AstNodeExpr* clonedp = bodyExprp->cloneTree(false);
// Substitute formal arguments with actual arguments
const V3TaskConnects tconnects = V3Task::taskConnects(funcrefp, seqp->stmtsp());
for (const auto& tconnect : tconnects) {
const AstVar* const portp = tconnect.first;
AstArg* const argp = tconnect.second;
clonedp->foreach([&](AstVarRef* refp) {
if (refp->varp() == portp) {
refp->replaceWith(argp->exprp()->cloneTree(false));
VL_DO_DANGLING(pushDeletep(refp), refp);
}
});
pushDeletep(argp->exprp()->unlinkFrBack());
}
// Replace the FuncRef with the inlined body
funcrefp->replaceWith(clonedp);
VL_DO_DANGLING(pushDeletep(funcrefp), funcrefp);
// Clear referenced flag; sequences with isReferenced==false are deleted in assertPreAll
seqp->isReferenced(false);
}
AstPropSpec* substitutePropertyCall(AstPropSpec* nodep) {
if (AstFuncRef* const funcrefp = VN_CAST(nodep->propp(), FuncRef)) {
if (const AstProperty* const propp = VN_CAST(funcrefp->taskp(), Property)) {
@ -601,6 +634,17 @@ private:
VL_DO_DANGLING(pushDeletep(nodep), nodep);
}
void visit(AstFuncRef* nodep) override {
// IEEE 1800-2023 16.8: Inline sequence instances wherever they appear
// in the expression tree (inside implications, boolean ops, nested refs, etc.)
if (AstSequence* const seqp = VN_CAST(nodep->taskp(), Sequence)) {
substituteSequenceCall(nodep, seqp);
// The FuncRef has been replaced; do not access nodep after this point.
// The replacement node will be visited by the parent's iterateChildren.
return;
}
iterateChildren(nodep);
}
void visit(AstImplication* nodep) override {
if (nodep->sentreep()) return; // Already processed
@ -790,6 +834,11 @@ private:
// (AstFuncRef)
VL_DO_DANGLING(pushDeletep(nodep->unlinkFrBack()), nodep);
}
void visit(AstSequence* nodep) override {
// Sequence declarations are not visited directly; their bodies are inlined
// at call sites by visit(AstFuncRef*). Collect for post-traversal cleanup.
m_seqsToCleanup.push_back(nodep);
}
void visit(AstNode* nodep) override { iterateChildren(nodep); }
public:
@ -800,6 +849,17 @@ public:
iterate(nodep);
// Fix up varref names
for (AstVarXRef* xrefp : m_xrefsp) xrefp->name(xrefp->varp()->name());
// Clean up sequence declarations after inlining.
// Referenced sequences that were inlined have isReferenced cleared.
// Remaining referenced sequences are in unsupported contexts (e.g. @seq event).
for (AstSequence* seqp : m_seqsToCleanup) {
if (seqp->isReferenced()) {
seqp->v3warn(E_UNSUPPORTED,
"Unsupported: sequence referenced outside assertion property");
} else {
VL_DO_DANGLING(seqp->unlinkFrBack()->deleteTree(), seqp);
}
}
}
~AssertPreVisitor() override = default;
};

4
src/V3AstNodeOther.h
View File

@ -2454,7 +2454,9 @@ public:
class AstSequence final : public AstNodeFTask {
// A sequence inside a module
// TODO when supported might not want to be a NodeFTask
bool m_referenced = false; // Ever referenced (for unsupported check)
bool m_referenced = false; // Set by V3LinkResolve when referenced; cleared by
// V3AssertPre after inlining; if still set after
// V3AssertPre, the reference is in an unsupported context
public:
AstSequence(FileLine* fl, const string& name, AstNode* stmtp)
: ASTGEN_SUPER_Sequence(fl, name, stmtp) {}

23
src/V3Width.cpp
View File

@ -6758,13 +6758,22 @@ class WidthVisitor final : public VNVisitor {
}
void visit(AstReturn* nodep) override { nodep->v3fatalSrc("'return' missed in LinkJump"); }
void visit(AstSequence* nodep) override {
// UNSUPPORTED message is thrown only where the sequence is referenced
// in order to enable some UVM tests.
// When support more here will need finer-grained UNSUPPORTED if items
// under the sequence are not supported
if (nodep->isReferenced()) nodep->v3warn(E_UNSUPPORTED, "Unsupported: sequence");
userIterateChildren(nodep, nullptr);
if (!nodep->isReferenced()) VL_DO_DANGLING(nodep->unlinkFrBack()->deleteTree(), nodep);
// IEEE 1800-2023 16.7 (sequence declarations), 16.8 (sequence instances)
// Width-check the sequence body so expressions are typed for later inlining.
// Referenced sequences in assertion context will be inlined by V3AssertPre.
if (nodep->didWidth()) return;
nodep->dtypeSetBit();
for (AstNode* stmtp = nodep->stmtsp(); stmtp; stmtp = stmtp->nextp()) {
if (VN_IS(stmtp, Var)) {
userIterate(stmtp, nullptr);
} else if (VN_IS(stmtp, NodeExpr)) {
iterateCheckSelf(nodep, "SeqBody", stmtp, SELF, BOTH);
} else {
stmtp->v3fatalSrc("Invalid statement under AstSequence");
}
}
nodep->didWidth(true);
// Keep all sequences for now; cleanup happens after V3AssertPre inlining.
}
AstPackage* getItemPackage(AstNode* pkgItemp) {

6
src/verilog.y
View File

@ -6568,9 +6568,9 @@ sequence_declaration<nodeFTaskp>: // ==IEEE: sequence_declaration
$$->addStmtsp($2);
$$->addStmtsp($4);
GRAMMARP->endLabel($<fl>6, $$, $6);
// No error on UVM special case with no reference; see t_sequence_unused.v
if (! (!$$->stmtsp() || (VN_IS($$->stmtsp(), Const) && !$$->stmtsp()->nextp())))
$$->v3warn(E_UNSUPPORTED, "Unsupported: sequence");
// Sequence declarations are allowed; they are inlined by V3AssertPre.
// Sequences in unsupported contexts are reported by assertPreAll
// after inlining.
}
;

18
test_regress/t/t_sequence_ref.py Executable file
View File

@ -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('simulator')
test.compile(timing_loop=True, verilator_flags2=['--assert', '--timing'])
test.execute()
test.passes()

47
test_regress/t/t_sequence_ref.v Normal file
View File

@ -0,0 +1,47 @@
// 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
);
int cyc = 0;
logic a, b, c;
// Sequence without arguments
sequence seq_ab;
a && b;
endsequence
// Sequence with formal arguments (default input direction)
sequence seq_check(logic sig1, logic sig2);
sig1 && sig2;
endsequence
// Overlapping implication with sequence ref (no args)
assert property (@(posedge clk) seq_ab |-> c);
// Non-overlapping implication
assert property (@(posedge clk) seq_ab |=> c);
// Sequence with args, multiple references with different actuals
assert property (@(posedge clk) seq_check(a, b) |-> c);
assert property (@(posedge clk) seq_check(b, c) |-> a);
always @(posedge clk) begin
cyc <= cyc + 1;
case (cyc)
2, 5: begin a <= 1'b1; b <= 1'b1; c <= 1'b1; end
3, 6: begin a <= 1'b0; b <= 1'b0; c <= 1'b1; end // c stays high for |=> check
default: begin a <= 1'b0; b <= 1'b0; c <= 1'b0; end
endcase
if (cyc == 10) begin
$write("*-* All Finished *-*\n");
$finish;
end
end
endmodule

2
test_regress/t/t_sequence_ref_unsup.out
View File

@ -1,4 +1,4 @@
%Error-UNSUPPORTED: t/t_sequence_ref_unsup.v:9:12: Unsupported: sequence
%Error-UNSUPPORTED: t/t_sequence_ref_unsup.v:9:12: Unsupported: sequence referenced outside assertion property
: ... note: In instance 't'
9 | sequence s_one;
| ^~~~~

86
test_regress/t/t_sequence_sexpr_unsup.out
View File

@ -1,175 +1,91 @@
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:25:12: Unsupported: sequence
25 | sequence s_a;
| ^~~
... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:28:12: Unsupported: sequence
28 | sequence s_var;
| ^~~~~
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:34:7: Unsupported: within (in sequence expression)
34 | a within(b);
| ^~~~~~
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:33:12: Unsupported: sequence
33 | sequence s_within;
| ^~~~~~~~
... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:38:7: Unsupported: and (in sequence expression)
38 | a and b;
| ^~~
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:37:12: Unsupported: sequence
37 | sequence s_and;
| ^~~~~
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:42:7: Unsupported: or (in sequence expression)
42 | a or b;
| ^~
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:41:12: Unsupported: sequence
41 | sequence s_or;
| ^~~~
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:46:7: Unsupported: throughout (in sequence expression)
46 | a throughout b;
| ^~~~~~~~~~
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:45:12: Unsupported: sequence
45 | sequence s_throughout;
| ^~~~~~~~~~~~
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:50:7: Unsupported: intersect (in sequence expression)
50 | a intersect b;
| ^~~~~~~~~
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:49:12: Unsupported: sequence
49 | sequence s_intersect;
| ^~~~~~~~~~~
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:53:12: Unsupported: sequence
53 | sequence s_uni_cycdelay_id;
| ^~~~~~~~~~~~~~~~~
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:56:12: Unsupported: sequence
56 | sequence s_uni_cycdelay_pid;
| ^~~~~~~~~~~~~~~~~~
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:60:5: Unsupported: ## range cycle delay range expression
60 | ## [1:2] b;
| ^~
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:59:12: Unsupported: sequence
59 | sequence s_uni_cycdelay_range;
| ^~~~~~~~~~~~~~~~~~~~
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:63:5: Unsupported: ## [*] cycle delay range expression
63 | ## [*] b;
| ^~
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:62:12: Unsupported: sequence
62 | sequence s_uni_cycdelay_star;
| ^~~~~~~~~~~~~~~~~~~
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:66:5: Unsupported: ## [+] cycle delay range expression
66 | ## [+] b;
| ^~
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:65:12: Unsupported: sequence
65 | sequence s_uni_cycdelay_plus;
| ^~~~~~~~~~~~~~~~~~~
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:69:12: Unsupported: sequence
69 | sequence s_cycdelay_id;
| ^~~~~~~~~~~~~
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:72:12: Unsupported: sequence
72 | sequence s_cycdelay_pid;
| ^~~~~~~~~~~~~~
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:76:7: Unsupported: ## range cycle delay range expression
76 | a ## [1:2] b;
| ^~
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:75:12: Unsupported: sequence
75 | sequence s_cycdelay_range;
| ^~~~~~~~~~~~~~~~
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:79:7: Unsupported: ## [*] cycle delay range expression
79 | a ## [*] b;
| ^~
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:78:12: Unsupported: sequence
78 | sequence s_cycdelay_star;
| ^~~~~~~~~~~~~~~
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:82:7: Unsupported: ## [+] cycle delay range expression
82 | a ## [+] b;
| ^~
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:81:12: Unsupported: sequence
81 | sequence s_cycdelay_plus;
| ^~~~~~~~~~~~~~~
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:86:7: Unsupported: [*] boolean abbrev expression
86 | a [* 1 ];
| ^~
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:86:10: Unsupported: boolean abbrev (in sequence expression)
86 | a [* 1 ];
| ^
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:85:12: Unsupported: sequence
85 | sequence s_booleanabbrev_brastar_int;
| ^~~~~~~~~~~~~~~~~~~~~~~~~~~
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:89:7: Unsupported: [*] boolean abbrev expression
89 | a [*];
| ^~
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:89:7: Unsupported: boolean abbrev (in sequence expression)
89 | a [*];
| ^~
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:88:12: Unsupported: sequence
88 | sequence s_booleanabbrev_brastar;
| ^~~~~~~~~~~~~~~~~~~~~~~
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:92:7: Unsupported: [+] boolean abbrev expression
92 | a [+];
| ^~~
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:92:7: Unsupported: boolean abbrev (in sequence expression)
92 | a [+];
| ^~~
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:91:12: Unsupported: sequence
91 | sequence s_booleanabbrev_plus;
| ^~~~~~~~~~~~~~~~~~~~
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:95:7: Unsupported: [= boolean abbrev expression
95 | a [= 1];
| ^~
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:95:10: Unsupported: boolean abbrev (in sequence expression)
95 | a [= 1];
| ^
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:94:12: Unsupported: sequence
94 | sequence s_booleanabbrev_eq;
| ^~~~~~~~~~~~~~~~~~
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:98:7: Unsupported: [= boolean abbrev expression
98 | a [= 1:2];
| ^~
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:98:10: Unsupported: boolean abbrev (in sequence expression)
98 | a [= 1:2];
| ^
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:97:12: Unsupported: sequence
97 | sequence s_booleanabbrev_eq_range;
| ^~~~~~~~~~~~~~~~~~~~~~~~
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:101:7: Unsupported: [-> boolean abbrev expression
101 | a [-> 1];
| ^~~
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:101:11: Unsupported: boolean abbrev (in sequence expression)
101 | a [-> 1];
| ^
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:100:12: Unsupported: sequence
100 | sequence s_booleanabbrev_minusgt;
| ^~~~~~~~~~~~~~~~~~~~~~~
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:104:7: Unsupported: [-> boolean abbrev expression
104 | a [-> 1:2];
| ^~~
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:104:11: Unsupported: boolean abbrev (in sequence expression)
104 | a [-> 1:2];
| ^
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:103:12: Unsupported: sequence
103 | sequence s_booleanabbrev_minusgt_range;
| ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:107:26: Unsupported: sequence argument data type
107 | sequence p_arg_seqence(sequence inseq);
| ^~~~~~~~
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:107:12: Unsupported: sequence
107 | sequence p_arg_seqence(sequence inseq);
| ^~~~~~~~~~~~~
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:112:5: Unsupported: first_match (in sequence expression)
112 | first_match (a);
| ^~~~~~~~~~~
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:111:12: Unsupported: sequence
111 | sequence s_firstmatch_a;
| ^~~~~~~~~~~~~~
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:115:5: Unsupported: first_match (in sequence expression)
115 | first_match (a, res0 = 1);
| ^~~~~~~~~~~
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:114:12: Unsupported: sequence
114 | sequence s_firstmatch_ab;
| ^~~~~~~~~~~~~~~
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:118:5: Unsupported: first_match (in sequence expression)
118 | first_match (a, res0 = 1, res1 = 2);
| ^~~~~~~~~~~
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:117:12: Unsupported: sequence
117 | sequence s_firstmatch_abc;
| ^~~~~~~~~~~~~~~~
%Warning-COVERIGN: t/t_sequence_sexpr_unsup.v:121:9: Ignoring unsupported: cover sequence
121 | cover sequence (s_a) $display("");
| ^~~~~~~~