From a8bccab8e6eb91b2d0924f3f475c31fc9a603522 Mon Sep 17 00:00:00 2001 From: Yilou Wang Date: Fri, 20 Mar 2026 15:24:46 +0100 Subject: [PATCH] Support named sequence declarations and instances in assertions (#7283) --- src/V3AssertPre.cpp | 60 ++++++++++++++++ src/V3AstNodeOther.h | 4 +- src/V3Width.cpp | 23 ++++-- src/verilog.y | 6 +- test_regress/t/t_sequence_ref.py | 18 +++++ test_regress/t/t_sequence_ref.v | 47 +++++++++++++ test_regress/t/t_sequence_ref_unsup.out | 2 +- test_regress/t/t_sequence_sexpr_unsup.out | 86 +---------------------- 8 files changed, 149 insertions(+), 97 deletions(-) create mode 100755 test_regress/t/t_sequence_ref.py create mode 100644 test_regress/t/t_sequence_ref.v diff --git a/src/V3AssertPre.cpp b/src/V3AssertPre.cpp index 024e91fd9..441447b72 100644 --- a/src/V3AssertPre.cpp +++ b/src/V3AssertPre.cpp @@ -63,6 +63,7 @@ private: bool m_inSynchDrive = false; // True if in synchronous drive std::vector m_xrefsp; // list of xrefs that need name fixup bool m_inPExpr = false; // True if in AstPExpr + std::vector 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; }; diff --git a/src/V3AstNodeOther.h b/src/V3AstNodeOther.h index d161d572e..ba0d51cf3 100644 --- a/src/V3AstNodeOther.h +++ b/src/V3AstNodeOther.h @@ -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) {} diff --git a/src/V3Width.cpp b/src/V3Width.cpp index fe0502087..2538ae2ea 100644 --- a/src/V3Width.cpp +++ b/src/V3Width.cpp @@ -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) { diff --git a/src/verilog.y b/src/verilog.y index 39684d8f0..7790b43d9 100644 --- a/src/verilog.y +++ b/src/verilog.y @@ -6568,9 +6568,9 @@ sequence_declaration: // ==IEEE: sequence_declaration $$->addStmtsp($2); $$->addStmtsp($4); GRAMMARP->endLabel($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. } ; diff --git a/test_regress/t/t_sequence_ref.py b/test_regress/t/t_sequence_ref.py new file mode 100755 index 000000000..35e44000c --- /dev/null +++ b/test_regress/t/t_sequence_ref.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('simulator') + +test.compile(timing_loop=True, verilator_flags2=['--assert', '--timing']) + +test.execute() + +test.passes() diff --git a/test_regress/t/t_sequence_ref.v b/test_regress/t/t_sequence_ref.v new file mode 100644 index 000000000..6358bae1f --- /dev/null +++ b/test_regress/t/t_sequence_ref.v @@ -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 diff --git a/test_regress/t/t_sequence_ref_unsup.out b/test_regress/t/t_sequence_ref_unsup.out index 414375621..41fb50aad 100644 --- a/test_regress/t/t_sequence_ref_unsup.out +++ b/test_regress/t/t_sequence_ref_unsup.out @@ -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; | ^~~~~ diff --git a/test_regress/t/t_sequence_sexpr_unsup.out b/test_regress/t/t_sequence_sexpr_unsup.out index fdd39486f..ae547a2d0 100644 --- a/test_regress/t/t_sequence_sexpr_unsup.out +++ b/test_regress/t/t_sequence_sexpr_unsup.out @@ -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(""); | ^~~~~~~~