From 86799ace5d8c2085de7751fc81a28a66b988a626 Mon Sep 17 00:00:00 2001 From: Yilou Wang Date: Mon, 25 May 2026 20:13:27 +0800 Subject: [PATCH] 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 --- src/V3AssertNfa.cpp | 112 +++++++++++++++++- test_regress/t/t_property_local_var_delay.py | 18 +++ test_regress/t/t_property_local_var_delay.v | 89 ++++++++++++++ .../t/t_property_local_var_range_unsup.out | 18 +++ .../t/t_property_local_var_range_unsup.py | 18 +++ .../t/t_property_local_var_range_unsup.v | 62 ++++++++++ 6 files changed, 316 insertions(+), 1 deletion(-) create mode 100755 test_regress/t/t_property_local_var_delay.py create mode 100644 test_regress/t/t_property_local_var_delay.v create mode 100644 test_regress/t/t_property_local_var_range_unsup.out create mode 100755 test_regress/t/t_property_local_var_range_unsup.py create mode 100644 test_regress/t/t_property_local_var_range_unsup.v diff --git a/src/V3AssertNfa.cpp b/src/V3AssertNfa.cpp index 22bb39d75..932ad855b 100644 --- a/src/V3AssertNfa.cpp +++ b/src/V3AssertNfa.cpp @@ -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& 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(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& 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 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(, 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 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); diff --git a/test_regress/t/t_property_local_var_delay.py b/test_regress/t/t_property_local_var_delay.py new file mode 100755 index 000000000..35e44000c --- /dev/null +++ b/test_regress/t/t_property_local_var_delay.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_property_local_var_delay.v b/test_regress/t/t_property_local_var_delay.v new file mode 100644 index 000000000..9953ede10 --- /dev/null +++ b/test_regress/t/t_property_local_var_delay.v @@ -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 diff --git a/test_regress/t/t_property_local_var_range_unsup.out b/test_regress/t/t_property_local_var_range_unsup.out new file mode 100644 index 000000000..362c6271d --- /dev/null +++ b/test_regress/t/t_property_local_var_range_unsup.out @@ -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 diff --git a/test_regress/t/t_property_local_var_range_unsup.py b/test_regress/t/t_property_local_var_range_unsup.py new file mode 100755 index 000000000..56c514bc5 --- /dev/null +++ b/test_regress/t/t_property_local_var_range_unsup.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('vlt') + +test.lint(expect_filename=test.golden_filename, + verilator_flags2=['--assert --error-limit 1000'], + fails=True) + +test.passes() diff --git a/test_regress/t/t_property_local_var_range_unsup.v b/test_regress/t/t_property_local_var_range_unsup.v new file mode 100644 index 000000000..518693cb8 --- /dev/null +++ b/test_regress/t/t_property_local_var_range_unsup.v @@ -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