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

Support SVA goto repetition [->N] in concurrent assertions (#7310)

This commit is contained in:
Yilou Wang 2026-03-27 15:31:15 +01:00 committed by GitHub
parent 9ed7a9f98b
commit 55e5f01758
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
11 changed files with 304 additions and 22 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

111
src/V3AssertPre.cpp
View File

@ -60,6 +60,7 @@ private:
AstIf* m_disableSeqIfp = nullptr; // Used for handling disable iff in sequences
// Other:
V3UniqueNames m_cycleDlyNames{"__VcycleDly"}; // Cycle delay counter name generator
V3UniqueNames m_gotoRepNames{"__VgotoRep"}; // Goto repetition counter name generator
V3UniqueNames m_disableCntNames{"__VdisableCnt"}; // Disable condition counter name generator
V3UniqueNames m_propVarNames{"__Vpropvar"}; // Property-local variable name generator
bool m_inAssign = false; // True if in an AssignNode
@ -709,6 +710,99 @@ private:
VL_DO_DANGLING(pushDeletep(nodep), nodep);
}
// Validate goto repetition count: must be a positive elaboration-time constant.
// On error, replaces nodep with BitFalse placeholder and returns nullptr.
const AstConst* validateGotoRepCount(AstNode* nodep, AstNodeExpr*& countp) {
countp = V3Const::constifyEdit(countp);
const AstConst* const constp = VN_CAST(countp, Const);
if (!constp) {
nodep->v3error("Goto repetition count is not an elaboration-time constant"
" (IEEE 1800-2023 16.9.2)");
VL_DO_DANGLING(pushDeletep(countp), countp);
nodep->replaceWith(new AstConst{nodep->fileline(), AstConst::BitFalse{}});
VL_DO_DANGLING(pushDeletep(nodep), nodep);
return nullptr;
}
if (constp->isZero()) {
nodep->v3error("Goto repetition count must be greater than zero"
" (IEEE 1800-2023 16.9.2)");
VL_DO_DANGLING(pushDeletep(countp), countp);
nodep->replaceWith(new AstConst{nodep->fileline(), AstConst::BitFalse{}});
VL_DO_DANGLING(pushDeletep(nodep), nodep);
return nullptr;
}
return constp;
}
// Lower goto repetition expr[->N] to a counter-based PExpr loop.
// Generated structure:
// begin
// automatic uint32 cnt = 0;
// loop { test(cnt < N); if (sampled(expr)) cnt++; if (cnt < N) @(clk); }
// // consequent check (if rhsp) or pass clause
// end
AstPExpr* createGotoRepPExpr(FileLine* flp, AstNodeExpr* exprp, AstNodeExpr* countp,
AstNodeExpr* rhsp, bool isOverlapped) {
AstSenItem* const sensesp = m_senip;
UASSERT_OBJ(sensesp, exprp, "Goto repetition requires a clock");
const std::string name = m_gotoRepNames.get(exprp);
AstVar* const cntVarp = new AstVar{flp, VVarType::BLOCKTEMP, name + "__counter",
exprp->findBasicDType(VBasicDTypeKwd::UINT32)};
cntVarp->lifetime(VLifetime::AUTOMATIC_EXPLICIT);
AstBegin* const beginp = new AstBegin{flp, name + "__block", cntVarp, true};
beginp->addStmtsp(
new AstAssign{flp, new AstVarRef{flp, cntVarp, VAccess::WRITE}, new AstConst{flp, 0}});
AstLoop* const loopp = new AstLoop{flp};
// Loop test: continue while cnt < N
loopp->addStmtsp(new AstLoopTest{flp, loopp,
new AstLt{flp, new AstVarRef{flp, cntVarp, VAccess::READ},
countp->cloneTreePure(false)}});
// if ($sampled(expr)) cnt++
AstSampled* const sampledp = new AstSampled{flp, exprp};
sampledp->dtypeFrom(exprp);
loopp->addStmtsp(
new AstIf{flp, sampledp,
new AstAssign{flp, new AstVarRef{flp, cntVarp, VAccess::WRITE},
new AstAdd{flp, new AstVarRef{flp, cntVarp, VAccess::READ},
new AstConst{flp, 1}}}});
// if (cnt < N) @(clk) -- only wait if not yet matched
loopp->addStmtsp(new AstIf{
flp, new AstLt{flp, new AstVarRef{flp, cntVarp, VAccess::READ}, countp},
new AstEventControl{flp, new AstSenTree{flp, sensesp->cloneTree(false)}, nullptr}});
beginp->addStmtsp(loopp);
if (rhsp) {
if (!isOverlapped) {
beginp->addStmtsp(new AstEventControl{
flp, new AstSenTree{flp, sensesp->cloneTree(false)}, nullptr});
}
AstSampled* const sampledRhsp = new AstSampled{flp, rhsp};
sampledRhsp->dtypeFrom(rhsp);
beginp->addStmtsp(new AstIf{flp, sampledRhsp, new AstPExprClause{flp, true},
new AstPExprClause{flp, false}});
} else {
beginp->addStmtsp(new AstPExprClause{flp, true});
}
return new AstPExpr{flp, beginp, exprp->findBitDType()};
}
void visit(AstSExprGotoRep* nodep) override {
// Standalone goto rep (not inside implication antecedent)
iterateChildren(nodep);
FileLine* const flp = nodep->fileline();
AstNodeExpr* countp = nodep->countp()->unlinkFrBack();
if (!validateGotoRepCount(nodep, countp)) return;
AstNodeExpr* const exprp = nodep->exprp()->unlinkFrBack();
AstPExpr* const pexprp = createGotoRepPExpr(flp, exprp, countp, nullptr, true);
nodep->replaceWith(pexprp);
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.)
@ -723,6 +817,23 @@ private:
void visit(AstImplication* nodep) override {
if (nodep->sentreep()) return; // Already processed
// Handle goto repetition as antecedent before iterateChildren,
// so the standalone AstSExprGotoRep visitor doesn't process it
if (AstSExprGotoRep* const gotop = VN_CAST(nodep->lhsp(), SExprGotoRep)) {
iterateChildren(gotop);
iterateAndNextNull(nodep->rhsp());
FileLine* const flp = nodep->fileline();
AstNodeExpr* countp = gotop->countp()->unlinkFrBack();
if (!validateGotoRepCount(nodep, countp)) return;
AstNodeExpr* const exprp = gotop->exprp()->unlinkFrBack();
AstNodeExpr* const rhsp = nodep->rhsp()->unlinkFrBack();
AstPExpr* const pexprp
= createGotoRepPExpr(flp, exprp, countp, rhsp, nodep->isOverlapped());
nodep->replaceWith(pexprp);
VL_DO_DANGLING(pushDeletep(nodep), nodep);
return;
}
iterateChildren(nodep);
FileLine* const flp = nodep->fileline();

16
src/V3AstNodeExpr.h
View File

@ -2153,6 +2153,22 @@ public:
bool cleanOut() const override { V3ERROR_NA_RETURN(""); }
int instrCount() const override { return widthInstrs(); }
};
class AstSExprGotoRep final : public AstNodeExpr {
// Goto repetition: expr [-> count]
// IEEE 1800-2023 16.9.2
// @astgen op1 := exprp : AstNodeExpr
// @astgen op2 := countp : AstNodeExpr
public:
explicit AstSExprGotoRep(FileLine* fl, AstNodeExpr* exprp, AstNodeExpr* countp)
: ASTGEN_SUPER_SExprGotoRep(fl) {
this->exprp(exprp);
this->countp(countp);
}
ASTGEN_MEMBERS_AstSExprGotoRep;
string emitVerilog() override { V3ERROR_NA_RETURN(""); }
string emitC() override { V3ERROR_NA_RETURN(""); }
bool cleanOut() const override { V3ERROR_NA_RETURN(""); }
};
class AstSFormatArg final : public AstNodeExpr {
// Information for formatting each argument to AstSFormat,
// used to pass to (potentially) runtime decoding of format arguments

8
src/V3Width.cpp
View File

@ -1624,6 +1624,14 @@ class WidthVisitor final : public VNVisitor {
if (nodep->seedp()) iterateCheckSigned32(nodep, "seed", nodep->seedp(), BOTH);
}
}
void visit(AstSExprGotoRep* nodep) override {
assertAtExpr(nodep);
if (m_vup->prelim()) {
iterateCheckBool(nodep, "exprp", nodep->exprp(), BOTH);
userIterateAndNext(nodep->countp(), WidthVP{SELF, BOTH}.p());
nodep->dtypeSetBit();
}
}
void visit(AstSExpr* nodep) override {
VL_RESTORER(m_underSExpr);
m_underSExpr = true;

12
src/verilog.y
View File

@ -6805,6 +6805,12 @@ sexpr<nodeExprp>: // ==IEEE: sequence_expr (The name sexpr is important as reg
// // IEEE: expression_or_dist [ boolean_abbrev ]
// // Note expression_or_dist includes "expr"!
// // sexpr/*sexpression_or_dist*/ --- Hardcoded below
// // IEEE: goto_repetition (single count form)
| ~p~sexpr/*sexpression_or_dist*/ yP_BRAMINUSGT constExpr ']'
{ $$ = new AstSExprGotoRep{$<fl>2, $1, $3}; }
// // IEEE: goto_repetition (range form -- unsupported)
| ~p~sexpr/*sexpression_or_dist*/ yP_BRAMINUSGT constExpr ':' constExpr ']'
{ $$ = $1; BBUNSUP($<fl>2, "Unsupported: [-> range goto repetition"); DEL($3); DEL($5); }
| ~p~sexpr/*sexpression_or_dist*/ boolean_abbrev
{ $$ = $1; BBUNSUP($2->fileline(), "Unsupported: boolean abbrev (in sequence expression)"); DEL($2); }
//
@ -6906,10 +6912,8 @@ boolean_abbrev<nodeExprp>: // ==IEEE: boolean_abbrev
| yP_BRAEQ constExpr ':' constExpr ']'
{ $$ = $2; BBUNSUP($<fl>1, "Unsupported: [= boolean abbrev expression"); DEL($4); }
// // IEEE: goto_repetition
| yP_BRAMINUSGT constExpr ']'
{ $$ = $2; BBUNSUP($<fl>1, "Unsupported: [-> boolean abbrev expression"); }
| yP_BRAMINUSGT constExpr ':' constExpr ']'
{ $$ = $2; BBUNSUP($<fl>1, "Unsupported: [-> boolean abbrev expression"); DEL($4); }
// // Goto repetition [->N] handled in sexpr rule (AstSExprGotoRep)
// // Range form [->M:N] also handled there (unsupported)
;
//************************************************

18
test_regress/t/t_assert_goto_rep.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(verilator_flags2=['--timing', '--assert'])
test.execute()
test.passes()

67
test_regress/t/t_assert_goto_rep.v Normal file
View File

@ -0,0 +1,67 @@
// 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 checkh(gotv,expv) do if ((gotv) !== (expv)) begin $write("%%Error: %s:%0d: got=%0x exp=%0x (%s !== %s)\n", `__FILE__,`__LINE__, (gotv), (expv), `"gotv`", `"expv`"); `stop; end while(0);
`define checkd(gotv,expv) do if ((gotv) !== (expv)) begin $write("%%Error: %s:%0d: got=%0d exp=%0d\n", `__FILE__,`__LINE__, (gotv), (expv)); `stop; end while(0);
// verilog_format: on
module t (
input clk
);
int cyc;
reg [63:0] crc;
// Derive signals from non-adjacent CRC bits (lesson 17: avoid shift correlation)
wire a = crc[0];
wire b = crc[4];
wire c = crc[8];
wire d = crc[12];
int count_fail1 = 0;
int count_fail2 = 0;
int count_fail3 = 0;
int count_fail4 = 0;
// Test 1: a[->2] |-> b (overlapping implication, 2 non-consecutive occurrences)
assert property (@(posedge clk) a[->2] |-> b)
else count_fail1 <= count_fail1 + 1;
// Test 2: a[->1] |-> c (single occurrence, overlapping)
assert property (@(posedge clk) a[->1] |-> c)
else count_fail2 <= count_fail2 + 1;
// Test 3: a[->3] |=> d (3 occurrences, non-overlapping implication)
assert property (@(posedge clk) a[->3] |=> d)
else count_fail3 <= count_fail3 + 1;
// Test 4: standalone goto rep (no implication) -- exercises standalone visitor
assert property (@(posedge clk) b[->2])
else count_fail4 <= count_fail4 + 1;
always @(posedge clk) begin
`ifdef TEST_VERBOSE
$write("[%0t] cyc==%0d crc=%x a=%b b=%b c=%b d=%b\n",
$time, cyc, crc, a, b, c, d);
`endif
cyc <= cyc + 1;
crc <= {crc[62:0], crc[63] ^ crc[2] ^ crc[0]};
if (cyc == 0) begin
crc <= 64'h5aef0c8d_d70a4497;
end
else if (cyc == 99) begin
`checkh(crc, 64'hc77bb9b3784ea091);
`checkd(count_fail1, 20);
`checkd(count_fail2, 40);
`checkd(count_fail3, 19);
`checkd(count_fail4, 0);
$write("*-* All Finished *-*\n");
$finish;
end
end
endmodule

10
test_regress/t/t_assert_goto_rep_bad_count.out Normal file
View File

@ -0,0 +1,10 @@
%Error: t/t_assert_goto_rep_bad_count.v:16:42: Goto repetition count is not an elaboration-time constant (IEEE 1800-2023 16.9.2)
: ... note: In instance 't'
16 | assert property (@(posedge clk) a[->n] |-> b)
| ^~~
... See the manual at https://verilator.org/verilator_doc.html?v=latest for more assistance.
%Error: t/t_assert_goto_rep_bad_count.v:20:42: Goto repetition count must be greater than zero (IEEE 1800-2023 16.9.2)
: ... note: In instance 't'
20 | assert property (@(posedge clk) a[->0] |-> b)
| ^~~
%Error: Exiting due to

16
test_regress/t/t_assert_goto_rep_bad_count.py Executable file
View File

@ -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('linter')
test.lint(fails=True, expect_filename=test.golden_filename)
test.passes()

30
test_regress/t/t_assert_goto_rep_bad_count.v Normal file
View File

@ -0,0 +1,30 @@
// 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;
logic clk = 0;
always #5 clk = ~clk;
int cyc = 0;
logic a, b;
int n;
// Error: non-constant count
assert property (@(posedge clk) a[->n] |-> b)
else $error("FAIL");
// Error: zero count
assert property (@(posedge clk) a[->0] |-> b)
else $error("FAIL");
always @(posedge clk) begin
cyc <= cyc + 1;
if (cyc == 5) begin
$write("*-* All Finished *-*\n");
$finish;
end
end
endmodule

27
test_regress/t/t_property_sexpr_parse_unsup.out
View File

@ -1,8 +1,19 @@
%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:82:51: Unsupported: [-> boolean abbrev expression
82 | (count == 0, l_t = $realtime) ##1 (count == 7)[->1] |-> $realtime - l_t < 50.5;
| ^~~
... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest
%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:82:54: Unsupported: boolean abbrev (in sequence expression)
82 | (count == 0, l_t = $realtime) ##1 (count == 7)[->1] |-> $realtime - l_t < 50.5;
| ^
%Error: Exiting due to
%Warning-WIDTHTRUNC: t/t_property_sexpr_unsup.v:60:14: Logical operator IMPLICATION expects 1 bit on the RHS, but RHS's CMETHODHARD 'at' generates 8 bits.
: ... note: In instance 't.ieee'
60 | $rose(a) |-> q[0];
| ^~~
... For warning description see https://verilator.org/warn/WIDTHTRUNC?v=latest
... Use "/* verilator lint_off WIDTHTRUNC */" and lint_on around source to disable this message.
%Warning-WIDTHTRUNC: t/t_property_sexpr_unsup.v:65:29: Logical operator SEXPR expects 1 bit on the exprp, but exprp's CMETHODHARD 'at' generates 8 bits.
: ... note: In instance 't.ieee'
65 | ($rose(a), l_b = b) |-> ##[3:10] q[l_b];
| ^~
%Warning-WIDTHTRUNC: t/t_property_sexpr_unsup.v:86:31: Logical operator SEXPR expects 1 bit on the exprp, but exprp's VARREF 'b' generates 32 bits.
: ... note: In instance 't.ieee'
86 | assert property (@clk not a ##1 b);
| ^~
%Error: Internal Error: t/t_property_sexpr_unsup.v:65:29: ../V3AssertProp.cpp:#: Range delay SExpr without clocking event
: ... note: In instance 't.ieee'
65 | ($rose(a), l_b = b) |-> ##[3:10] q[l_b];
| ^~
... See the manual at https://verilator.org/verilator_doc.html?v=latest for more assistance.

11
test_regress/t/t_sequence_sexpr_unsup.out
View File

@ -50,18 +50,9 @@
%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: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:104:7: Unsupported: [-> boolean abbrev expression
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:104:7: Unsupported: [-> range goto repetition
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:107:26: Unsupported: sequence argument data type
107 | sequence p_arg_seqence(sequence inseq);
| ^~~~~~~~