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

Fix wrong false assert for property local variables with cycle-delayed consequents (#7587) (#7651) 

* Fix wrong false assert in property local variable with cycle-delayed consequent

* factor helper for 100 line cov

* add return, should be 100 line cov now
This commit is contained in:
Yilou Wang 2026-05-25 20:13:27 +08:00 committed by GitHub
parent be783e5574
commit 86799ace5d
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
6 changed files with 316 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

112
src/V3AssertNfa.cpp
View File

@ -1985,6 +1985,107 @@ class AssertNfaVisitor final : public VNVisitor {
for (AstNodeExpr* const srcp : requiredStepSrcs) pushDeletep(srcp);
}
// Replace one VarRef to a captured local var with $past(rhs, K)
// (or rhs inline when K == 0). No-op if refp is not in matchMap.
void substituteMatchItemRef(AstVarRef* refp, int K,
const std::unordered_map<const AstVar*, AstNodeExpr*>& matchMap) {
const auto it = matchMap.find(refp->varp());
if (it == matchMap.end()) return;
AstNodeExpr* newp = it->second->cloneTreePure(false);
if (K > 0) {
AstConst* const ticksp = new AstConst{refp->fileline(), AstConst::WidthedValue{}, 32,
static_cast<uint32_t>(K)};
AstPast* const pastp = new AstPast{refp->fileline(), newp, ticksp};
pastp->dtypeFrom(newp);
newp = pastp;
}
refp->replaceWith(newp);
VL_DO_DANGLING(pushDeletep(refp), refp);
return;
}
// Recursively walk a consequent. Returns cycle length consumed and
// substitutes each VarRef to a captured local var with $past(rhs, K)
// (or rhs inline when K == 0). Reports E_UNSUPPORTED on non-constant
// delays or composite sequence operators.
int walkSubstituteMatchItems(AstNodeExpr* nodep, int K,
const std::unordered_map<const AstVar*, AstNodeExpr*>& matchItems,
bool& errorEmitted) {
if (AstSExpr* const sexprp = VN_CAST(nodep, SExpr)) {
// IEEE 1800-2023 16.9.2: cycle_delay's lhsp is a constant_expression
// and the delay form in a sequence is always `##N`, folded by
// V3Const + V3Param before V3AssertNfa. Range form `##[m:n]` is the
// only user-visible reject here.
AstDelay* const delayp = VN_AS(sexprp->delayp(), Delay);
UASSERT_OBJ(delayp->isCycleDelay() && VN_IS(delayp->lhsp(), Const), sexprp,
"SVA cycle delay must have a constant lhsp");
if (delayp->isRangeDelay()) {
sexprp->v3warn(E_UNSUPPORTED, "Unsupported: property local variable used across "
"non-constant cycle delay in consequent"
" (IEEE 1800-2023 16.10)");
errorEmitted = true;
return -1;
}
const int delayCycles = VN_AS(delayp->lhsp(), Const)->toSInt();
int preLen = 0;
if (AstNodeExpr* const prep = sexprp->preExprp()) {
preLen = walkSubstituteMatchItems(prep, K, matchItems, errorEmitted);
if (errorEmitted) return -1;
}
const int bodyLen = walkSubstituteMatchItems(sexprp->exprp(), K + preLen + delayCycles,
matchItems, errorEmitted);
if (errorEmitted) return -1;
return preLen + delayCycles + bodyLen;
}
if (nodep->isMultiCycleSva()) {
nodep->v3warn(E_UNSUPPORTED, "Unsupported: property local variable used across "
"composite sequence operator in consequent"
" (IEEE 1800-2023 16.10)");
errorEmitted = true;
return -1;
}
std::vector<AstVarRef*> refs;
nodep->foreach([&refs](AstVarRef* p) { refs.push_back(p); });
for (AstVarRef* const refp : refs) substituteMatchItemRef(refp, K, matchItems);
return 0;
}
// Lower property-local match-item assignments before NFA construction.
// Without this, the antecedent's AstExprStmt(<x = rhs_expr>, antBool)
// survives into every NFA edge as a continuous-alias side-effect, so the
// local-var temp tracks the current cycle's rhs_expr rather than the
// antecedent-match cycle's value -- wrong for `|-> ##N` and `|=> ##N`
// with N > 0 (issue #7587). Each consequent reference to the local var
// is replaced with `$past(rhs_expr, K)` where K = (overlapped ? 0 : 1)
// plus any accumulated `##N` delay. Returns true if E_UNSUPPORTED was
// emitted; caller must replace the body with BitFalse and bail.
bool liftMatchItemSubstitutions(PropertyParts& parts, AstNodeExpr* seqBodyp) {
if (!parts.hasImplication) return false;
AstExprStmt* const exprStmtp = VN_CAST(parts.triggerExprp, ExprStmt);
if (!exprStmtp) return false;
// IEEE 1800-2023 16.10 BNF requires `(expr, match_item {, match_item})`
// with at least one match item; V3LinkParse only emits ExprStmt for
// this form and only emits AstAssign with VarRef LHS for each item.
std::unordered_map<const AstVar*, AstNodeExpr*> matchItems;
for (AstNode* stmtp = exprStmtp->stmtsp(); stmtp; stmtp = stmtp->nextp()) {
AstAssign* const assignp = VN_AS(stmtp, Assign);
AstVarRef* const lhsRefp = VN_AS(assignp->lhsp(), VarRef);
matchItems[lhsRefp->varp()] = assignp->rhsp();
}
const int startK = parts.isOverlapped ? 0 : 1;
bool errorEmitted = false;
walkSubstituteMatchItems(seqBodyp, startK, matchItems, errorEmitted);
// Match-item substitution / strip mutates ancestor purity. Release
// builds don't auto-clear caches on edits, so refresh here.
VIsCached::clearCacheTree();
if (errorEmitted) return true;
AstNodeExpr* const antBoolp = exprStmtp->resultp()->unlinkFrBack();
exprStmtp->replaceWith(antBoolp);
VL_DO_DANGLING(pushDeletep(exprStmtp), exprStmtp);
parts.triggerExprp = antBoolp;
return false;
}
void processAssertion(AstNodeCoverOrAssert* assertp) {
if (assertp->immediate()) return;
@ -2001,7 +2102,7 @@ class AssertNfaVisitor final : public VNVisitor {
AstNode* const propp = assertp->propp();
if (!hasMultiCycleExpr(propp)) return;
const PropertyParts parts = decomposeProperty(propp);
PropertyParts parts = decomposeProperty(propp);
UASSERT_OBJ(parts.seqExprp, propp, "Property body must be an expression");
// Unwrap `not` (IEEE 1800-2023 16.12.1); odd count -> negated semantics.
@ -2012,6 +2113,15 @@ class AssertNfaVisitor final : public VNVisitor {
seqBodyp = notp->lhsp();
}
// Substitute property-local match-item refs in consequent with
// $past(rhs, K) before NFA build (IEEE 1800-2023 16.10).
if (liftMatchItemSubstitutions(parts, seqBodyp)) {
AstPropSpec* const psp = VN_CAST(assertp->propp(), PropSpec);
UASSERT_OBJ(psp, assertp, "Concurrent assertion must have PropSpec");
replaceBodyOnBuildError(assertp->fileline(), psp, /*errorEmitted=*/true);
return;
}
AstSenTree* senTreep = assertp->sentreep();
bool senTreeOwned = false; // True if we created senTreep locally
AstPropSpec* const propSpecp = VN_CAST(assertp->propp(), PropSpec);

18
test_regress/t/t_property_local_var_delay.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()

89
test_regress/t/t_property_local_var_delay.v Normal file
View File

@ -0,0 +1,89 @@
// 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;
always @(posedge clk) cyc <= cyc + 1;
// |-> ##0 (overlapped, same-cycle, K=0): inlined substitution.
// Captured snap equals live cyc at the same cycle by definition.
property p_overlap_d0;
int snap;
@(posedge clk) (cyc > 0,
snap = cyc
) |-> (snap == cyc);
endproperty
assert property (p_overlap_d0);
// |-> ##5 (overlapped, K=5): captured snap at T must equal cyc - 5
// at maturity T+5. If substitution leaks the live cyc, this fails.
property p_overlap_d5;
int snap;
@(posedge clk) (cyc > 4,
snap = cyc
) |-> ##5 (snap == cyc - 5);
endproperty
assert property (p_overlap_d5);
// |=> (non-overlapped, K=1).
property p_nonoverlap_d1;
int snap;
@(posedge clk) (cyc > 0,
snap = cyc
) |=> (snap == cyc - 1);
endproperty
assert property (p_nonoverlap_d1);
// |=> ##3 (non-overlapped, K=4).
property p_nonoverlap_d4;
int snap;
@(posedge clk) (cyc > 4,
snap = cyc
) |=> ##3 (snap == cyc - 4);
endproperty
assert property (p_nonoverlap_d4);
// |-> with match-item ref inside the SExpr's preExprp: substitution
// is done at K = 0, exercising the inline branch (no $past wrapper).
property p_overlap_pre_ref;
int snap;
@(posedge clk) (cyc > 0,
snap = cyc - 1
) |-> (snap == cyc - 1) ##2 (cyc > 2);
endproperty
assert property (p_overlap_pre_ref);
// Nested SExpr: pre-expr 1'b1 plus ##2 then ##3. Total K = 5.
property p_nested_seq;
int snap;
@(posedge clk) (cyc > 4,
snap = cyc
) |-> ##2 (1'b1 ##3 (snap == cyc - 5));
endproperty
assert property (p_nested_seq);
// Multiple match items on one antecedent must both be substituted.
property p_multi_match;
int snap_a, snap_b;
@(posedge clk) (cyc > 1,
snap_a = cyc
,
snap_b = cyc + 1
) |-> ##2
((snap_a == cyc - 2) && (snap_b == cyc - 1));
endproperty
assert property (p_multi_match);
initial begin
repeat (40) @(posedge clk);
$write("*-* All Finished *-*\n");
$finish;
end
endmodule

18
test_regress/t/t_property_local_var_range_unsup.out Normal file
View File

@ -0,0 +1,18 @@
%Error-UNSUPPORTED: t/t_property_local_var_range_unsup.v:21:11: Unsupported: property local variable used across non-constant cycle delay in consequent (IEEE 1800-2023 16.10)
: ... note: In instance 't'
21 | ) |-> ##[1:3] (cyc > prev);
| ^~
... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest
%Error-UNSUPPORTED: t/t_property_local_var_range_unsup.v:31:25: Unsupported: property local variable used across composite sequence operator in consequent (IEEE 1800-2023 16.10)
: ... note: In instance 't'
31 | ) |-> (cyc == snap) and ##1 (cyc == snap + 1);
| ^~~
%Error-UNSUPPORTED: t/t_property_local_var_range_unsup.v:42:17: Unsupported: property local variable used across non-constant cycle delay in consequent (IEEE 1800-2023 16.10)
: ... note: In instance 't'
42 | ) |-> (1'b1 ##[1:3] (cyc > snap)) ##2 (cyc > snap);
| ^~
%Error-UNSUPPORTED: t/t_property_local_var_range_unsup.v:53:21: Unsupported: property local variable used across non-constant cycle delay in consequent (IEEE 1800-2023 16.10)
: ... note: In instance 't'
53 | ) |-> ##2 (1'b1 ##[1:3] (cyc > snap));
| ^~
%Error: Exiting due to

18
test_regress/t/t_property_local_var_range_unsup.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('vlt')
test.lint(expect_filename=test.golden_filename,
verilator_flags2=['--assert --error-limit 1000'],
fails=True)
test.passes()

62
test_regress/t/t_property_local_var_range_unsup.v Normal file
View File

@ -0,0 +1,62 @@
// 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;
logic valid;
// Range delay (##[1:3]) over a property-local match-item capture is
// not yet supported: per-attempt storage is needed to disambiguate
// overlapping in-flight attempts.
property p_range;
int prev;
@(posedge clk) (valid,
prev = cyc
) |-> ##[1:3] (cyc > prev);
endproperty
assert property (p_range);
// Composite sequence operator (sequence `and`) under a captured local
// variable reference is also out of scope for the v1 substitution.
property p_composite;
int snap;
@(posedge clk) (valid,
snap = cyc
) |-> (cyc == snap) and ##1 (cyc == snap + 1);
endproperty
assert property (p_composite);
// Nested range delay inside the consequent's preExprp -- the outer
// SExpr's recursion into preExprp errors, then the outer caller's
// `if (errorEmitted) return -1;` after preLen recursion is exercised.
property p_nested_in_pre;
int snap;
@(posedge clk) (valid,
snap = cyc
) |-> (1'b1 ##[1:3] (cyc > snap)) ##2 (cyc > snap);
endproperty
assert property (p_nested_in_pre);
// Nested range delay inside the consequent's exprp -- the outer
// SExpr's recursion into exprp errors, then the outer caller's
// `if (errorEmitted) return -1;` after bodyLen recursion is exercised.
property p_nested_in_body;
int snap;
@(posedge clk) (valid,
snap = cyc
) |-> ##2 (1'b1 ##[1:3] (cyc > snap));
endproperty
assert property (p_nested_in_body);
always @(posedge clk) begin
cyc <= cyc + 1;
valid <= (cyc == 2);
end
endmodule