Support property-local variables and sequence match items (#7286)

src/V3AssertPre.cpp

@@ -27,6 +27,8 @@
 #include "V3Task.h"
 #include "V3UniqueNames.h"
 
+#include <unordered_map>
+
 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)
+        // Statements in AstProperty: AstVar (ports/local vars),
-        // and AstVar (arguments).
+        // 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<const AstVar*, AstNodeExpr*> portMap;
         for (const auto& tconnect : tconnects) {
-            const AstVar* const portp = tconnect.first;
+            portMap[tconnect.first] = tconnect.second->exprp();
-            AstArg* const argp = tconnect.second;
+        }
-            clonedp->foreach([&](AstVarRef* refp) {
+        clonedp->foreach([&](AstVarRef* refp) {
-                if (refp->varp() == portp) {
+            const auto it = portMap.find(refp->varp());
-                    refp->replaceWith(argp->exprp()->cloneTree(false));
+            if (it != portMap.end()) {
-                    VL_DO_DANGLING(pushDeletep(refp), refp);
+                refp->replaceWith(it->second->cloneTree(false));
-                }
+                VL_DO_DANGLING(pushDeletep(refp), refp);
-            });
+            }
-            pushDeletep(argp->exprp()->unlinkFrBack());
+        });
+        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<const AstVar*, AstNodeExpr*> portMap;
                 for (const auto& tconnect : tconnects) {
-                    const AstVar* const portp = tconnect.first;
+                    portMap[tconnect.first] = tconnect.second->exprp();
-                    // 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());
                 }
+
+                // 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<const AstVar*, AstVar*> 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.

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");
             }

src/verilog.y

@@ -6546,9 +6546,9 @@ property_port_itemDirE:
 
 property_declarationBody<nodep>:  // 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<nodeExprp>:  // ==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

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
+                    ... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest
-   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;
-      |                ^
 %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

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

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()

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