diff --git a/src/V3AssertPre.cpp b/src/V3AssertPre.cpp index eb9acb885..6bc153135 100644 --- a/src/V3AssertPre.cpp +++ b/src/V3AssertPre.cpp @@ -27,6 +27,8 @@ #include "V3Task.h" #include "V3UniqueNames.h" +#include + VL_DEFINE_DEBUG_FUNCTIONS; //###################################################################### @@ -59,6 +61,7 @@ private: // Other: V3UniqueNames m_cycleDlyNames{"__VcycleDly"}; // Cycle delay 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 bool m_inAssignDlyLhs = false; // True if in AssignDly's LHS bool m_inSynchDrive = false; // True if in synchronous drive @@ -97,10 +100,14 @@ private: return VN_CAST(bodyp, NodeExpr); } AstPropSpec* getPropertyExprp(const AstProperty* const propp) { - // The only statements possible in AstProperty are AstPropSpec (body) - // and AstVar (arguments). + // Statements in AstProperty: AstVar (ports/local vars), + // AstInitialStaticStmt/AstInitialAutomaticStmt (var init), AstPropSpec (body). AstNode* propExprp = propp->stmtsp(); - while (VN_IS(propExprp, Var)) propExprp = propExprp->nextp(); + while (propExprp + && (VN_IS(propExprp, Var) || VN_IS(propExprp, InitialStaticStmt) + || VN_IS(propExprp, InitialAutomaticStmt))) { + propExprp = propExprp->nextp(); + } return VN_CAST(propExprp, PropSpec); } void substituteSequenceCall(AstFuncRef* funcrefp, AstSequence* seqp) { @@ -110,18 +117,22 @@ private: 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 + // Build substitution map, then do a single traversal to replace all formals + // (textual substitution per IEEE 16.8.2). const V3TaskConnects tconnects = V3Task::taskConnects(funcrefp, seqp->stmtsp()); + std::unordered_map portMap; 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()); + portMap[tconnect.first] = tconnect.second->exprp(); + } + clonedp->foreach([&](AstVarRef* refp) { + const auto it = portMap.find(refp->varp()); + if (it != portMap.end()) { + refp->replaceWith(it->second->cloneTree(false)); + VL_DO_DANGLING(pushDeletep(refp), refp); + } + }); + for (const auto& tconnect : tconnects) { + pushDeletep(tconnect.second->exprp()->unlinkFrBack()); } // Replace the FuncRef with the inlined body funcrefp->replaceWith(clonedp); @@ -139,20 +150,53 @@ private: // Clone subtree after substitution. It is needed, because property might be called // multiple times with different arguments. propExprp = propExprp->cloneTree(false); - // Substitute formal arguments with actual arguments + // Build substitution maps for formal arguments and property-local + // variables, then perform a single foreach to apply all replacements. + // Map port vars to their actual argument expressions const V3TaskConnects tconnects = V3Task::taskConnects(funcrefp, propp->stmtsp()); + std::unordered_map portMap; for (const auto& tconnect : tconnects) { - const AstVar* const portp = tconnect.first; - // cppcheck-suppress constVariablePointer // 'exprp' unlinked below - AstArg* const argp = tconnect.second; - propExprp->foreach([&](AstVarRef* refp) { - if (refp->varp() == portp) { - refp->replaceWith(argp->exprp()->cloneTree(false)); - VL_DO_DANGLING(pushDeletep(refp), refp); - } - }); - pushDeletep(argp->exprp()->unlinkFrBack()); + portMap[tconnect.first] = tconnect.second->exprp(); } + + // Promote property-local variables (non-port vars, IEEE 16.10) to + // module-level __Vpropvar temps. Cross-cycle persistence is handled + // by the match item lowering in visit(AstImplication*). + std::unordered_map localVarMap; + for (AstNode* stmtp = propp->stmtsp(); stmtp; stmtp = stmtp->nextp()) { + if (AstVar* const varp = VN_CAST(stmtp, Var)) { + if (!varp->isIO()) { + const string newName = m_propVarNames.get(varp); + AstVar* const newVarp = new AstVar{ + varp->fileline(), VVarType::MODULETEMP, newName, varp->dtypep()}; + newVarp->lifetime(VLifetime::STATIC_EXPLICIT); + m_modp->addStmtsp(newVarp); + localVarMap[varp] = newVarp; + } + } + } + + // Single traversal: substitute ports and update local var references + propExprp->foreach([&](AstVarRef* refp) { + { + const auto portIt = portMap.find(refp->varp()); + if (portIt != portMap.end()) { + refp->replaceWith(portIt->second->cloneTree(false)); + VL_DO_DANGLING(pushDeletep(refp), refp); + return; + } + } + { + const auto localIt = localVarMap.find(refp->varp()); + if (localIt != localVarMap.end()) { refp->varp(localIt->second); } + } + }); + + // Clean up argument expressions + for (const auto& tconnect : tconnects) { + pushDeletep(tconnect.second->exprp()->unlinkFrBack()); + } + // Handle case with 2 disable iff statement (IEEE 1800-2023 16.12.1) if (nodep->disablep() && propExprp->disablep()) { nodep->v3error("disable iff expression before property call and in its " @@ -684,6 +728,71 @@ private: FileLine* const flp = nodep->fileline(); AstNodeExpr* const rhsp = nodep->rhsp()->unlinkFrBack(); AstNodeExpr* lhsp = nodep->lhsp()->unlinkFrBack(); + + // Lower sequence match items (IEEE 16.11): (expr, var = val, ...) |-> / |=> + if (AstExprStmt* const exprStmtp = VN_CAST(lhsp, ExprStmt)) { + AstNodeExpr* const antExprp = exprStmtp->resultp()->unlinkFrBack(); + + if (nodep->isOverlapped()) { + // |-> : assign to __Vpropvar via always_comb (continuous). + // The assign evaluates RHS once; V3Sampled snapshots the + // result so all consequent refs read the same value. + AstNode* matchAssignsp = nullptr; + for (AstNode* stmtp = exprStmtp->stmtsp(); stmtp;) { + AstNode* const nextp = stmtp->nextp(); + if (AstAssign* const assignp = VN_CAST(stmtp, Assign)) { + assignp->unlinkFrBack(); + if (!matchAssignsp) { + matchAssignsp = assignp; + } else { + matchAssignsp->addNext(assignp); + } + } + stmtp = nextp; + } + VL_DO_DANGLING(pushDeletep(lhsp), lhsp); + lhsp = antExprp; + + if (matchAssignsp) { + AstAlways* const alwaysp + = new AstAlways{flp, VAlwaysKwd::ALWAYS_COMB, nullptr, matchAssignsp}; + m_modp->addStmtsp(alwaysp); + } + } else { + // |=> : assign to __Vpropvar via NBA in a clocked always block. + // The NBA commits before the next cycle's sampled snapshot, + // so the consequent (which already references __Vpropvar) + // sees the captured value. + AstNode* matchAssignsp = nullptr; + for (AstNode* stmtp = exprStmtp->stmtsp(); stmtp;) { + AstNode* const nextp = stmtp->nextp(); + if (AstAssign* const assignp = VN_CAST(stmtp, Assign)) { + assignp->unlinkFrBack(); + AstNodeExpr* const assignLhsp = assignp->lhsp()->unlinkFrBack(); + AstNodeExpr* const assignRhsp = assignp->rhsp()->unlinkFrBack(); + AstAssignDly* const dlyp = new AstAssignDly{flp, assignLhsp, assignRhsp}; + VL_DO_DANGLING(pushDeletep(assignp), assignp); + if (!matchAssignsp) { + matchAssignsp = dlyp; + } else { + matchAssignsp->addNext(dlyp); + } + } + stmtp = nextp; + } + VL_DO_DANGLING(pushDeletep(lhsp), lhsp); + lhsp = antExprp; + + if (matchAssignsp) { + AstIf* const condp + = new AstIf{flp, antExprp->cloneTreePure(false), matchAssignsp}; + AstAlways* const alwaysp + = new AstAlways{flp, VAlwaysKwd::ALWAYS, newSenTree(nodep), condp}; + m_modp->addStmtsp(alwaysp); + } + } + } + if (AstPExpr* const pexprp = VN_CAST(rhsp, PExpr)) { // Implication with sequence expression on RHS (IEEE 1800-2023 16.11, 16.12.7). // The PExpr was already lowered from the property expression by V3AssertProp. diff --git a/src/V3Width.cpp b/src/V3Width.cpp index 2538ae2ea..b0e949f87 100644 --- a/src/V3Width.cpp +++ b/src/V3Width.cpp @@ -6749,6 +6749,10 @@ class WidthVisitor final : public VNVisitor { userIterate(propStmtp, nullptr); } else if (VN_IS(propStmtp, PropSpec)) { iterateCheckSelf(nodep, "PropSpec", propStmtp, SELF, BOTH); + } else if (VN_IS(propStmtp, InitialStaticStmt) + || VN_IS(propStmtp, InitialAutomaticStmt)) { + // Property-local variable initialization -- iterate this node only + userIterate(propStmtp, nullptr); } else { propStmtp->v3fatalSrc("Invalid statement under AstProperty"); } diff --git a/src/verilog.y b/src/verilog.y index 7790b43d9..ba3fc230d 100644 --- a/src/verilog.y +++ b/src/verilog.y @@ -6546,9 +6546,9 @@ property_port_itemDirE: property_declarationBody: // IEEE: part of property_declaration assertion_variable_declarationList property_spec - { $$ = nullptr; BBUNSUP($1->fileline(), "Unsupported: property variable declaration"); DEL($1, $2); } + { $$ = addNextNull($1, $2); } | assertion_variable_declarationList property_spec ';' - { $$ = nullptr; BBUNSUP($1->fileline(), "Unsupported: property variable declaration"); DEL($1, $2); } + { $$ = addNextNull($1, $2); } // // IEEE-2012: Incorrectly has yCOVER ySEQUENCE then property_spec here. // // Fixed in IEEE 1800-2017 | property_spec { $$ = $1; } @@ -6813,7 +6813,7 @@ sexpr: // ==IEEE: sequence_expr (The name sexpr is important as reg // // "'(' sexpr ')' boolean_abbrev" matches "[sexpr:'(' expr ')'] boolean_abbrev" so we can drop it | '(' ~p~sexpr ')' { $$ = $2; } | '(' ~p~sexpr ',' sequence_match_itemList ')' - { $$ = $2; BBUNSUP($3, "Unsupported: sequence match items"); DEL($4); } + { $$ = new AstExprStmt{$3, $4, $2}; } // // // AND/OR are between pexprs OR sexprs | ~p~sexpr yAND ~p~sexpr diff --git a/test_regress/t/t_property_sexpr_parse_unsup.out b/test_regress/t/t_property_sexpr_parse_unsup.out index 0449d4338..6d775621a 100644 --- a/test_regress/t/t_property_sexpr_parse_unsup.out +++ b/test_regress/t/t_property_sexpr_parse_unsup.out @@ -1,23 +1,11 @@ -%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:65:14: Unsupported: sequence match items - 65 | ($rose(a), l_b = b) |-> ##[3:10] q[l_b]; - | ^ - ... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest %Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:65:29: Unsupported: ## range cycle delay range expression 65 | ($rose(a), l_b = b) |-> ##[3:10] q[l_b]; | ^~ -%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:64:13: Unsupported: property variable declaration - 64 | integer l_b; - | ^~~ -%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:82:16: Unsupported: sequence match items - 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:51: Unsupported: [-> boolean abbrev expression 82 | (count == 0, l_t = $realtime) ##1 (count == 7)[->1] |-> $realtime - l_t < 50.5; | ^~~ %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-UNSUPPORTED: t/t_property_sexpr_unsup.v:80:14: Unsupported: property variable declaration - 80 | realtime l_t; - | ^~~ %Error: Exiting due to diff --git a/test_regress/t/t_property_var_unsup.out b/test_regress/t/t_property_var_unsup.out index 5fffe4942..f71fcf0c7 100644 --- a/test_regress/t/t_property_var_unsup.out +++ b/test_regress/t/t_property_var_unsup.out @@ -1,11 +1,5 @@ -%Error-UNSUPPORTED: t/t_property_var_unsup.v:16:11: Unsupported: sequence match items - 16 | (valid, prevcyc = cyc) |=> (cyc == prevcyc + 1); - | ^ - ... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest -%Error-UNSUPPORTED: t/t_property_var_unsup.v:15:9: Unsupported: property variable declaration - 15 | int prevcyc; - | ^~~~~~~ %Error-UNSUPPORTED: t/t_property_var_unsup.v:23:30: Unsupported: property variable default value 23 | property with_def(int nine = 9); | ^ + ... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest %Error: Exiting due to diff --git a/test_regress/t/t_sequence_local_var.py b/test_regress/t/t_sequence_local_var.py new file mode 100755 index 000000000..35e44000c --- /dev/null +++ b/test_regress/t/t_sequence_local_var.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_local_var.v b/test_regress/t/t_sequence_local_var.v new file mode 100644 index 000000000..9ea97ca25 --- /dev/null +++ b/test_regress/t/t_sequence_local_var.v @@ -0,0 +1,82 @@ +// 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 valid; + + // --- Scenario 1: |=> with conditional antecedent --- + // Captures cyc when valid is true, checks cyc == prev+1 next cycle. + property p_nonoverlap; + int prev; + @(posedge clk) + (valid, prev = cyc) |=> (cyc == prev + 1); + endproperty + assert property (p_nonoverlap); + + // --- Scenario 2: |-> overlapped with match item --- + // Captures cyc on same cycle, checks equality immediately. + property p_overlap; + int snap; + @(posedge clk) + (1, snap = cyc) |-> (cyc == snap); + endproperty + assert property (p_overlap); + + // --- Scenario 3: same property referenced twice (isolation test) --- + // Each instance must get its own __Vpropvar variable. + int counter_x = 0; + int counter_y = 1000; + + property p_track(int sig); + int prev; + @(posedge clk) + (1, prev = sig) |=> (sig == prev + 1); + endproperty + assert property (p_track(counter_x)); + assert property (p_track(counter_y)); + + // --- Scenario 4: |-> match item with $urandom (side-effect test) --- + // snap = $urandom() must evaluate once; snap == snap is always true. + int overlap_fail = 0; + property p_overlap_sideeffect; + int snap; + @(posedge clk) + (1, snap = $urandom()) |-> (snap == snap); + endproperty + assert property (p_overlap_sideeffect) + else overlap_fail++; + + // --- Scenario 5: |=> match item with $urandom (side-effect test) --- + int nonoverlap_fail = 0; + property p_nonoverlap_sideeffect; + int snap; + @(posedge clk) + (1, snap = $urandom()) |=> (snap == snap); + endproperty + assert property (p_nonoverlap_sideeffect) + else nonoverlap_fail++; + + always @(posedge clk) begin + cyc <= cyc + 1; + counter_x <= counter_x + 1; + counter_y <= counter_y + 1; + + // valid is true at specific cycles only (not always-true) + valid <= (cyc == 2 || cyc == 5 || cyc == 8); + + if (cyc == 100) begin + if (overlap_fail > 0) $stop; + if (nonoverlap_fail > 0) $stop; + $write("*-* All Finished *-*\n"); + $finish; + end + end + +endmodule