Merge f6228d00d8 into 100c831474

Remove block names
Signed-off-by: Bartłomiej Chmiel <bchmiel@antmicro.com>
2025-11-06 07:10:55 -05:00 · 2025-11-06 13:09:02 +01:00 · 2025-11-06 12:38:47 +01:00 · 2025-11-06 11:54:52 +01:00 · 2025-11-06 11:51:46 +01:00 · 2025-11-06 11:36:56 +01:00
30 changed files with 1107 additions and 553 deletions
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@ -43,6 +43,7 @@ set(HEADERS
    V3ActiveTop.h
    V3Assert.h
    V3AssertPre.h
+    V3AssertProp.h
    V3Ast.h
    V3AstAttr.h
    V3AstInlines.h
@ -207,6 +208,7 @@ set(COMMON_SOURCES
    V3ActiveTop.cpp
    V3Assert.cpp
    V3AssertPre.cpp
+    V3AssertProp.cpp
    V3Ast.cpp
    V3AstNodes.cpp
    V3Begin.cpp
--- a/src/Makefile_obj.in
+++ b/src/Makefile_obj.in
@ -232,6 +232,7 @@ RAW_OBJS_PCH_ASTNOMT = \
  V3ActiveTop.o \
  V3Assert.o \
  V3AssertPre.o \
+  V3AssertProp.o \
  V3Begin.o \
  V3Branch.o \
  V3CCtors.o \
--- a/src/V3Assert.cpp
+++ b/src/V3Assert.cpp
@ -143,6 +143,9 @@ class AssertVisitor final : public VNVisitor {
    VDouble0 m_statPastVars;  // Statistic tracking
    bool m_inSampled = false;  // True inside a sampled expression
    bool m_inRestrict = false;  // True inside restrict assertion
+    AstNode* m_passsp = nullptr;  // Current pass statement
+    AstNode* m_failsp = nullptr;  // Current fail statement
+    bool m_underAssert = false;  // Visited from assert

    // METHODS
    static AstNodeExpr* assertOnCond(FileLine* fl, VAssertType type,
@ -288,25 +291,18 @@ class AssertVisitor final : public VNVisitor {
        return ifp;
    }

-    static AstNode* assertBody(AstNodeCoverOrAssert* nodep, AstNodeExpr* propp, AstNode* passsp,
-                               AstNode* failsp) {
-        if (AstPExpr* const pExpr = VN_CAST(propp, PExpr)) {
-            AstNodeExpr* const condp = pExpr->condp();
-            UASSERT_OBJ(condp, pExpr, "Should have condition");
-            AstIf* const ifp = assertCond(nodep, condp->unlinkFrBack(), passsp, failsp);
-
-            AstNode* const precondps = pExpr->precondp();
-            UASSERT_OBJ(precondps, pExpr, "Should have precondition");
-            precondps->unlinkFrBackWithNext()->addNext(ifp);
-            AstNodeStmt* const aonp = newIfAssertOn(precondps, nodep->directive(), nodep->type());
-            FileLine* const flp = precondps->fileline();
-            AstFork* const forkp = new AstFork{flp, VJoinType::JOIN_NONE};
-            forkp->addForksp(new AstBegin{flp, "", aonp, true});
-            return forkp;
+    AstNode* assertBody(AstNodeCoverOrAssert* nodep, AstNode* propp, AstNode* passsp,
+                        AstNode* failsp) {
+        AstNode* bodyp = nullptr;
+        if (AstPExpr* const pexprp = VN_CAST(propp, PExpr)) {
+            AstFork* const forkp = new AstFork{nodep->fileline(), VJoinType::JOIN_NONE};
+            forkp->addForksp(pexprp->bodyp()->unlinkFrBack());
+            VL_DO_DANGLING(pushDeletep(pexprp), pexprp);
+            bodyp = forkp;
+        } else {
+            bodyp = assertCond(nodep, VN_AS(propp, NodeExpr), passsp, failsp);
        }
-
-        AstIf* const ifp = assertCond(nodep, propp, passsp, failsp);
-        return newIfAssertOn(ifp, nodep->directive(), nodep->type());
+        return newIfAssertOn(bodyp, nodep->directive(), nodep->type());
    }

    AstNodeStmt* newFireAssertUnchecked(const AstNodeStmt* nodep, const string& message,
@ -336,7 +332,6 @@ class AssertVisitor final : public VNVisitor {
        { AssertDeFuture{nodep->propp(), m_modp, m_modPastNum++}; }
        iterateChildren(nodep);

-        AstNodeExpr* const propp = VN_AS(nodep->propp()->unlinkFrBackWithNext(), NodeExpr);
        AstSenTree* const sentreep = nodep->sentreep();
        const string& message = nodep->name();
        AstNode* passsp = nodep->passsp();
@ -384,7 +379,15 @@ class AssertVisitor final : public VNVisitor {
            nodep->v3fatalSrc("Unknown node type");
        }

-        AstNode* bodysp = assertBody(nodep, propp, passsp, failsp);
+        VL_RESTORER(m_passsp);
+        VL_RESTORER(m_failsp);
+        VL_RESTORER(m_underAssert);
+        m_passsp = passsp;
+        m_failsp = failsp;
+        m_underAssert = true;
+        iterate(nodep->propp());
+
+        AstNode* bodysp = assertBody(nodep, nodep->propp()->unlinkFrBack(), passsp, failsp);
        if (sentreep) {
            bodysp = new AstAlways{nodep->fileline(), VAlwaysKwd::ALWAYS, sentreep, bodysp};
        }
@ -631,7 +634,7 @@ class AssertVisitor final : public VNVisitor {
    }
    void visit(AstVarRef* nodep) override {
        iterateChildren(nodep);
-        if (m_inSampled && !VString::startsWith(nodep->name(), "__VpropPrecond")) {
+        if (m_inSampled && !VString::startsWith(nodep->name(), "__VcycleDly")) {
            if (!nodep->access().isReadOnly()) {
                nodep->v3warn(E_UNSUPPORTED,
                              "Unsupported: Write to variable in sampled expression");
@ -651,16 +654,27 @@ class AssertVisitor final : public VNVisitor {
        m_inSampled = false;
        iterateChildren(nodep);
    }
+    void visit(AstPExprClause* nodep) override {
+        if (m_underAssert) {
+            if (nodep->pass() && m_passsp) {
+                // Cover adds COVERINC by AstNode::addNext, thus need to clone next too.
+                nodep->replaceWith(m_passsp->cloneTree(true));
+            } else if (!nodep->pass() && m_failsp) {
+                // Asserts with multiple statements are wrapped in implicit begin/end blocks so no
+                // need to clone next.
+                nodep->replaceWith(m_failsp->cloneTree(false));
+            } else {
+                nodep->unlinkFrBack();
+            }
+            VL_DO_DANGLING(pushDeletep(nodep), nodep);
+        }
+    }
    void visit(AstPExpr* nodep) override {
-        {
+        if (m_underAssert) {
            VL_RESTORER(m_inSampled);
            m_inSampled = false;
-            iterateAndNextNull(nodep->precondp());
-        }
-        iterate(nodep->condp());
-        if (!m_inRestrict) {
-            VL_DO_DANGLING(pushDeletep(nodep), nodep);
-        } else {
+            iterateChildren(nodep);
+        } else if (m_inRestrict) {
            VL_DO_DANGLING(pushDeletep(nodep->unlinkFrBack()), nodep);
        }
    }
--- a/src/V3AssertPre.cpp
+++ b/src/V3AssertPre.cpp
@ -56,15 +56,11 @@ private:
    AstNodeExpr* m_disablep = nullptr;  // Last disable
    // Other:
    V3UniqueNames m_cycleDlyNames{"__VcycleDly"};  // Cycle delay counter name generator
-    V3UniqueNames m_propPrecondNames{"__VpropPrecond"};  // Cycle delay temporaries 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
    std::vector<AstVarXRef*> m_xrefsp;  // list of xrefs that need name fixup
-    AstNodeExpr* m_hasUnsupp = nullptr;  // True if assert has unsupported construct inside
-    AstPExpr* m_pExpr = nullptr;  // Current AstPExpr
-    bool m_hasSExpr = false;  // True if assert has AstSExpr inside
-    bool m_inSExpr = false;  // True if in AstSExpr
+    bool m_inPExpr = false;  // True if in AstPExpr

    // METHODS

@ -343,7 +339,7 @@ private:
        }
        AstSenItem* sensesp = nullptr;
        if (!m_defaultClockingp) {
-            if (!m_pExpr && !m_inSExpr) {
+            if (!m_inPExpr) {
                nodep->v3error("Usage of cycle delays requires default clocking"
                               " (IEEE 1800-2023 14.11)");
                VL_DO_DANGLING(nodep->unlinkFrBack()->deleteTree(), nodep);
@ -419,33 +415,6 @@ private:
                }
            }
            nodep->user1(true);
-        } else if (m_inSExpr && !nodep->user1()) {
-            AstVar* const preVarp
-                = new AstVar{nodep->varp()->fileline(), VVarType::BLOCKTEMP,
-                             m_propPrecondNames.get(nodep->varp()) + "__" + nodep->varp()->name(),
-                             nodep->varp()->dtypep()};
-            preVarp->lifetime(VLifetime::STATIC_EXPLICIT);
-            m_modp->addStmtsp(preVarp);
-            AstVarRef* const origp
-                = new AstVarRef{nodep->fileline(), nodep->varp(), VAccess::READ};
-            origp->user1(true);
-            AstVarRef* const precondp
-                = new AstVarRef{preVarp->fileline(), preVarp, VAccess::WRITE};
-            precondp->user1(true);
-
-            // Pack assignments in sampled as in concurrent assertions they are needed.
-            // Then, in assert's propp, sample only non-precondition variables.
-            AstSampled* const sampledp = new AstSampled{origp->fileline(), origp};
-            sampledp->dtypeFrom(origp);
-            UASSERT(m_pExpr, "Should be under assertion");
-            AstAssign* const assignp = new AstAssign{m_pExpr->fileline(), precondp, sampledp};
-            m_pExpr->addPrecondp(assignp);
-
-            AstVarRef* const precondReadp
-                = new AstVarRef{preVarp->fileline(), preVarp, VAccess::READ};
-            precondReadp->user1(true);
-            nodep->replaceWith(precondReadp);
-            VL_DO_DANGLING(pushDeletep(nodep), nodep);
        }
    }
    void visit(AstMemberSel* nodep) override {
@ -500,32 +469,11 @@ private:
    void visit(AstNodeCoverOrAssert* nodep) override {
        if (nodep->sentreep()) return;  // Already processed

-        VL_RESTORER(m_hasSExpr);
-        VL_RESTORER(m_hasUnsupp);
-
        clearAssertInfo();
-        m_pExpr = new AstPExpr{nodep->propp()->fileline()};
-        m_pExpr->dtypeFrom(nodep->propp());

        // Find Clocking's buried under nodep->exprsp
        iterateChildren(nodep);
        if (!nodep->immediate()) nodep->sentreep(newSenTree(nodep));
-        if (m_hasSExpr && m_hasUnsupp) {
-            if (VN_IS(m_hasUnsupp, Implication)) {
-                m_hasUnsupp->v3warn(E_UNSUPPORTED,
-                                    "Unsupported: Implication with sequence expression");
-            } else {
-                m_hasUnsupp->v3warn(E_UNSUPPORTED,
-                                    "Unsupported: Disable iff with sequence expression");
-            }
-            if (m_pExpr) VL_DO_DANGLING(pushDeletep(m_pExpr), m_pExpr);
-        } else if (m_pExpr && m_pExpr->precondp()) {
-            m_pExpr->condp(VN_AS(nodep->propp()->unlinkFrBackWithNext(), NodeExpr));
-            nodep->propp(m_pExpr);
-            iterateAndNextNull(m_pExpr->precondp());
-        } else if (m_pExpr) {
-            VL_DO_DANGLING(pushDeletep(m_pExpr), m_pExpr);
-        }
        clearAssertInfo();
    }
    void visit(AstFalling* nodep) override {
@ -564,10 +512,6 @@ private:
        if (sentreep) VL_DO_DANGLING(pushDeletep(sentreep->unlinkFrBack()), sentreep);
        nodep->sentreep(newSenTree(nodep));
    }
-    void visit(AstLogNot* nodep) override {
-        if (m_inSExpr) nodep->v3error("Syntax error: unexpected 'not' in sequence expression");
-        iterateChildren(nodep);
-    }
    void visit(AstPast* nodep) override {
        if (nodep->sentreep()) return;  // Already processed
        iterateChildren(nodep);
@ -633,7 +577,6 @@ private:

    void visit(AstImplication* nodep) override {
        if (nodep->sentreep()) return;  // Already processed
-        m_hasUnsupp = nodep;

        iterateChildren(nodep);

@ -685,7 +628,6 @@ private:
        }
        if (AstNodeExpr* const disablep = nodep->disablep()) {
            m_disablep = disablep;
-            m_hasUnsupp = disablep;
            if (VN_IS(nodep->backp(), Cover)) {
                blockp = new AstAnd{disablep->fileline(),
                                    new AstNot{disablep->fileline(), disablep->unlinkFrBack()},
@ -699,17 +641,19 @@ private:
        nodep->replaceWith(blockp);
        VL_DO_DANGLING(pushDeletep(nodep), nodep);
    }
-    void visit(AstSExpr* nodep) override {
-        VL_RESTORER(m_inSExpr);
-        m_inSExpr = true;
-        m_hasSExpr = true;
+    void visit(AstPExpr* nodep) override {
+        VL_RESTORER(m_inPExpr);
+        m_inPExpr = true;

-        UASSERT_OBJ(m_pExpr, nodep, "Should be under assertion");
-        m_pExpr->addPrecondp(nodep->delayp()->unlinkFrBack());
+        if (AstLogNot* const notp = VN_CAST(nodep->backp(), LogNot)) {
+            notp->replaceWith(nodep->unlinkFrBack());
+            VL_DO_DANGLING(pushDeletep(notp), notp);
+            iterate(nodep);
+        } else {
+            iterateChildren(nodep);
+        }

        iterateChildren(nodep);
-        nodep->replaceWith(nodep->exprp()->unlinkFrBack());
-        VL_DO_DANGLING(pushDeletep(nodep), nodep);
    }
    void visit(AstNodeModule* nodep) override {
        VL_RESTORER(m_defaultClockingp);
--- a/src/V3AssertProp.cpp
+++ b/src/V3AssertProp.cpp
@ -0,0 +1,264 @@
+// -*- mode: C++; c-file-style: "cc-mode" -*-
+//*************************************************************************
+// DESCRIPTION: Verilator: Implementation of assertion properties
+//
+// Code available from: https://verilator.org
+//
+//*************************************************************************
+//
+// Copyright 2005-2025 by Wilson Snyder. 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-License-Identifier: LGPL-3.0-only OR Artistic-2.0
+//
+//*************************************************************************
+//  Each sequence is translated into a decision tree in form of deterministic
+//  finite automaton (DFA) with bipartite structure. Each cycle delay is connected
+//  with an expression that depending on an evaluation result, proceeds to the next
+//  evaluation state. The structure is rooted with original sequence expression for
+//  simplifying further transformation back to AST.
+//
+//  The graph consists of the following nodes:
+//
+//  DfaStmtVertex:  Statements to be executed to traverse from one state to another
+//  DfaExprVertex:   Property expression that is checked and based on that a branch
+//                  is taken.
+//  DfaConditionEdge:   Branch edge that connects statements and expressions.
+//
+//  Properties steps:
+//      Ensemble a property decision tree from sequence expressions.
+//      Transform property decision tree into AST, remove source sequence expression
+//          Property blocks are wrapped with AstPExpr that are transformed
+//          further by V3AssertPre and V3Assert.
+//
+//*************************************************************************
+
+#include "V3PchAstNoMT.h"  // VL_MT_DISABLED_CODE_UNIT
+
+#include "V3AssertProp.h"
+
+#include "V3Graph.h"
+
+VL_DEFINE_DEBUG_FUNCTIONS;
+
+//######################################################################
+// Data structures (graph types)
+
+class DfaVertex VL_NOT_FINAL : public V3GraphVertex {
+    VL_RTTI_IMPL(DfaVertex, V3GraphVertex)
+    // STATE
+    AstNode* const m_nodep;  // Underlying node
+
+public:
+    // CONSTRUCTORS
+    explicit DfaVertex(V3Graph* graphp, AstNode* nodep) VL_MT_DISABLED : V3GraphVertex{graphp},
+                                                                         m_nodep{nodep} {}
+    AstNode* nodep() const { return m_nodep; }
+    string name() const override VL_MT_STABLE {
+        return cvtToHex(m_nodep) + "\\n " + cvtToStr(m_nodep->typeName()) + "\\n"s
+               + m_nodep->fileline()->ascii();
+    };
+    string dotShape() const override {
+        if (inEmpty()) return "tripleoctagon";
+        if (outEmpty()) return "doubleoctagon";
+        return "oval";
+    }
+    bool isStart() const { return inEmpty(); }
+};
+
+class DfaStmtVertex final : public DfaVertex {
+    VL_RTTI_IMPL(DfaStmtVertex, V3GraphEdge)
+public:
+    // CONSTRUCTORS
+    explicit DfaStmtVertex(V3Graph* graphp, AstNodeStmt* stmtp) VL_MT_DISABLED
+        : DfaVertex{graphp, stmtp} {}
+    string dotColor() const override { return "green"; }
+};
+
+class DfaExprVertex final : public DfaVertex {
+    VL_RTTI_IMPL(DfaExprVertex, V3GraphEdge)
+public:
+    // CONSTRUCTORS
+    explicit DfaExprVertex(V3Graph* graphp, AstNodeExpr* exprp) VL_MT_DISABLED
+        : DfaVertex{graphp, exprp} {}
+    string dotColor() const override { return "blue"; }
+};
+
+class DfaConditionEdge final : public V3GraphEdge {
+    VL_RTTI_IMPL(DfaConditionEdge, V3GraphEdge)
+    // STATE
+    const bool m_ifBranch;  // Whether this branch is taken for fulfilled condition
+
+public:
+    // CONSTRUCTORS
+    explicit DfaConditionEdge(V3Graph* graphp, DfaVertex* fromp, DfaVertex* top,
+                              bool ifBranch) VL_MT_DISABLED : V3GraphEdge{graphp, fromp, top, 1},
+                                                              m_ifBranch{ifBranch} {}
+    ~DfaConditionEdge() override = default;
+
+    bool ifBranch() const { return m_ifBranch; }
+    string dotColor() const override { return m_ifBranch ? "green" : "red"; }
+};
+
+// Parse properties and ensemble a property tree graph
+class AssertPropBuildVisitor final : public VNVisitorConst {
+    // STATE
+    V3Graph& m_graph;  // Property tree
+    DfaVertex* m_lastVtxp = nullptr;  // Last encountered vertex
+    bool m_underSExpr = false;  // Is under sequence expression, for creating a start node
+    size_t m_underLogNots = 0;  // Number of 'not' operators before sequence
+
+    DfaStmtVertex* makeClause(AstSExpr* nodep, bool pass) {
+        return new DfaStmtVertex{
+            &m_graph,
+            new AstPExprClause{nodep->fileline(), m_underLogNots % 2 == 0 ? pass : !pass}};
+    }
+
+    // VISITORS
+    void visit(AstNodeCoverOrAssert* nodep) override { iterateChildrenConst(nodep); }
+    void visit(AstLogNot* nodep) override {
+        VL_RESTORER(m_underLogNots);
+        ++m_underLogNots;
+        iterateChildrenConst(nodep);
+    }
+    void visit(AstSExpr* nodep) override {
+
+        if (VN_IS(nodep->exprp(), SExpr)) {
+            VL_RESTORER(m_underSExpr);
+            m_underSExpr = true;
+            iterateConst(nodep->exprp());
+        } else {
+            DfaExprVertex* const exprVtxp
+                = new DfaExprVertex{&m_graph, nodep->exprp()->unlinkFrBack()};
+            new DfaConditionEdge{&m_graph, exprVtxp, makeClause(nodep, true), true};
+            new DfaConditionEdge{&m_graph, exprVtxp, makeClause(nodep, false), false};
+            m_lastVtxp = exprVtxp;
+        }
+
+        DfaExprVertex* const startVtxp
+            = m_underSExpr ? nullptr : new DfaExprVertex{&m_graph, nodep};
+
+        DfaStmtVertex* const dlyVtxp
+            = new DfaStmtVertex{&m_graph, nodep->delayp()->unlinkFrBack()};
+
+        if (AstSExpr* const sexprp = VN_CAST(nodep->preExprp(), SExpr)) {
+            UASSERT_OBJ(!sexprp->preExprp() && !VN_IS(sexprp->exprp(), SExpr), sexprp,
+                        "Incorrect sexpr tree");
+            DfaStmtVertex* const sdlyVtxp
+                = new DfaStmtVertex{&m_graph, sexprp->delayp()->unlinkFrBack()};
+            DfaExprVertex* const exprVtxp
+                = new DfaExprVertex{&m_graph, sexprp->exprp()->unlinkFrBack()};
+
+            if (startVtxp) new DfaConditionEdge{&m_graph, startVtxp, sdlyVtxp, true};
+            new DfaConditionEdge{&m_graph, sdlyVtxp, exprVtxp, true};
+            new DfaConditionEdge{&m_graph, exprVtxp, dlyVtxp, true};
+            new DfaConditionEdge{&m_graph, dlyVtxp, m_lastVtxp, true};
+            new DfaConditionEdge{&m_graph, exprVtxp, makeClause(nodep, false), false};
+
+            // This case only occurs when multi-delay sequence starts with an expression,
+            // don't set last as this is never a last expression.
+        } else if (nodep->preExprp()) {
+            DfaExprVertex* const preVtxp
+                = new DfaExprVertex{&m_graph, nodep->preExprp()->unlinkFrBack()};
+            if (startVtxp) new DfaConditionEdge{&m_graph, startVtxp, preVtxp, true};
+            new DfaConditionEdge{&m_graph, preVtxp, dlyVtxp, true};
+            new DfaConditionEdge{&m_graph, dlyVtxp, m_lastVtxp, true};
+            new DfaConditionEdge{&m_graph, preVtxp, makeClause(nodep, false), false};
+            m_lastVtxp = preVtxp;
+        } else {
+            if (startVtxp) new DfaConditionEdge{&m_graph, startVtxp, dlyVtxp, true};
+            new DfaConditionEdge{&m_graph, dlyVtxp, m_lastVtxp, true};
+            m_lastVtxp = dlyVtxp;
+        }
+    }
+    void visit(AstNode* nodep) override { iterateChildrenConst(nodep); }
+    void visit(AstConstPool* nodep) override {}
+
+public:
+    // CONSTRUCTORS
+    explicit AssertPropBuildVisitor(AstNetlist* nodep, V3Graph& graph)
+        : m_graph{graph} {
+        iterateConst(nodep);
+        if (dumpGraphLevel() >= 6) m_graph.dumpDotFilePrefixedAlways("properties", true);
+    }
+    ~AssertPropBuildVisitor() override = default;
+};
+
+// Transform property graph into AST
+class AssertPropTransformer final {
+    // STATE
+    V3Graph& m_graph;  // Property tree
+    AstPExpr* m_pexprp = nullptr;  // Currently built property sequence
+    AstBegin* m_current = nullptr;  // Currently built block
+
+    V3GraphVertex* processVtx(V3GraphVertex* vtxp) {
+        if (DfaStmtVertex* const stmtp = vtxp->cast<DfaStmtVertex>()) return processVtx(stmtp);
+        if (DfaExprVertex* const exprp = vtxp->cast<DfaExprVertex>()) return processVtx(exprp);
+        // TODO use C++17 std::variant and std::visit
+        v3fatalSrc("Unexpected vertex type");
+        return nullptr;
+    }
+    V3GraphVertex* processVtx(DfaStmtVertex* vtxp) {
+        UASSERT_OBJ(!vtxp->isStart(), vtxp->nodep(),
+                    "Starting node should be a property expression");
+        UASSERT_OBJ(m_current, vtxp->nodep(), "Should be under a block");
+        m_current->addStmtsp(vtxp->nodep());
+        return processEdge(vtxp->outEdges().frontp());
+    }
+    V3GraphVertex* processVtx(DfaExprVertex* vtxp) {
+        AstNode* const nodep = vtxp->nodep();
+        if (vtxp->isStart()) {
+            AstBegin* const bodyp = new AstBegin{nodep->fileline(), "", nullptr, true};
+            m_pexprp = new AstPExpr{nodep->fileline(), bodyp, nodep->dtypep()};
+            UASSERT_OBJ(vtxp->outSize1(), nodep, "Starting node must have one out edge");
+            m_current = m_pexprp->bodyp();
+            return processEdge(vtxp->outEdges().frontp());
+        }
+        UASSERT_OBJ(vtxp->outEdges().size() == 2, nodep, "Each expression must have two branches");
+        AstBegin* const passsp = new AstBegin{nodep->fileline(), "", nullptr, true};
+        AstNode* const failsp = vtxp->outEdges().backp()->top()->as<DfaStmtVertex>()->nodep();
+
+        AstSampled* const sampledp
+            = new AstSampled{nodep->fileline(), VN_AS(vtxp->nodep(), NodeExpr)};
+        sampledp->dtypeFrom(vtxp->nodep());
+        AstIf* const ifp = new AstIf{nodep->fileline(), sampledp, passsp, failsp};
+        m_current->addStmtsp(ifp);
+        m_current = passsp;
+        return processEdge(vtxp->outEdges().frontp());
+    }
+    V3GraphVertex* processEdge(V3GraphEdge* edgep) {
+        if (edgep) return processVtx(edgep->top());
+        return nullptr;
+    }
+
+public:
+    // CONSTRUCTORS
+    explicit AssertPropTransformer(V3Graph& graph)
+        : m_graph{graph} {
+        for (V3GraphVertex& vtx : m_graph.vertices()) {
+            if (DfaVertex* const dVtxp = vtx.cast<DfaExprVertex>()) {
+                if (dVtxp->isStart()) {
+                    VL_RESTORER(m_pexprp);
+                    processVtx(&vtx);
+                    AstSExpr* const propp = VN_AS(dVtxp->nodep(), SExpr);
+                    propp->replaceWith(m_pexprp);
+                    VL_DO_DANGLING(propp->deleteTree(), propp);
+                }
+            }
+        }
+    }
+};
+
+//######################################################################
+// Top AssertProp class
+
+void V3AssertProp::assertPropAll(AstNetlist* nodep) {
+    UINFO(2, __FUNCTION__ << ":");
+    {
+        V3Graph graph;
+        { AssertPropBuildVisitor{nodep, graph}; }
+        AssertPropTransformer{graph};
+    }
+    V3Global::dumpCheckGlobalTree("assertproperties", 0, dumpTreeEitherLevel() >= 3);
+}
--- a/src/V3AssertProp.h
+++ b/src/V3AssertProp.h
@ -0,0 +1,32 @@
+// -*- mode: C++; c-file-style: "cc-mode" -*-
+//*************************************************************************
+// DESCRIPTION: Verilator: Implementation of assertion properties
+//
+// Code available from: https://verilator.org
+//
+//*************************************************************************
+//
+// Copyright 2005-2025 by Wilson Snyder. 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-License-Identifier: LGPL-3.0-only OR Artistic-2.0
+//
+//*************************************************************************
+
+#ifndef VERILATOR_V3ASSERTPROP_H_
+#define VERILATOR_V3ASSERTPROP_H_
+
+#include "config_build.h"
+#include "verilatedos.h"
+
+class AstNetlist;
+
+//============================================================================
+
+class V3AssertProp final {
+public:
+    static void assertPropAll(AstNetlist* nodep) VL_MT_DISABLED;
+};
+
+#endif  // Guard
--- a/src/V3AstNodeExpr.h
+++ b/src/V3AstNodeExpr.h
@ -1764,11 +1764,13 @@ public:
 };
 class AstPExpr final : public AstNodeExpr {
    // Property expression
-    // @astgen op1 := precondp : List[AstNode]
-    // @astgen op2 := condp : Optional[AstNodeExpr]
+    // @astgen op1 := bodyp : AstBegin
 public:
-    explicit AstPExpr(FileLine* fl)
-        : ASTGEN_SUPER_PExpr(fl) {}
+    explicit AstPExpr(FileLine* fl, AstBegin* bodyp, AstNodeDType* dtypep)
+        : ASTGEN_SUPER_PExpr(fl) {
+        this->bodyp(bodyp);
+        this->dtypep(dtypep);
+    }
    ASTGEN_MEMBERS_AstPExpr;
    string emitVerilog() override { V3ERROR_NA_RETURN(""); }
    string emitC() override { V3ERROR_NA_RETURN(""); }
@ -1986,11 +1988,19 @@ public:
 };
 class AstSExpr final : public AstNodeExpr {
    // Sequence expression
-    // @astgen op1 := delayp : AstDelay
-    // @astgen op2 := exprp : AstNodeExpr
+    // @astgen op1 := preExprp: Optional[AstNodeExpr]
+    // @astgen op2 := delayp : AstNodeStmt<AstDelay|AstBegin>
+    // @astgen op3 := exprp : AstNodeExpr
 public:
-    explicit AstSExpr(FileLine* fl, AstDelay* delayp, AstNodeExpr* exprp)
+    explicit AstSExpr(FileLine* fl, AstNodeExpr* preExprp, AstNodeStmt* delayp, AstNodeExpr* exprp)
        : ASTGEN_SUPER_SExpr(fl) {
+        this->preExprp(preExprp);
+        this->delayp(delayp);
+        this->exprp(exprp);
+    }
+    explicit AstSExpr(FileLine* fl, AstNodeStmt* delayp, AstNodeExpr* exprp)
+        : ASTGEN_SUPER_SExpr(fl) {
+        this->preExprp(nullptr);
        this->delayp(delayp);
        this->exprp(exprp);
    }
--- a/src/V3AstNodeStmt.h
+++ b/src/V3AstNodeStmt.h
@ -821,6 +821,17 @@ public:
    }
    bool off() const { return m_off; }
 };
+class AstPExprClause final : public AstNodeStmt {
+    const bool m_pass;  // True if will be replaced by passing assertion clause, false for
+                        // assertion failure clause
+
+public:
+    ASTGEN_MEMBERS_AstPExprClause;
+    explicit AstPExprClause(FileLine* fl, bool pass = true)
+        : ASTGEN_SUPER_PExprClause(fl)
+        , m_pass{pass} {}
+    bool pass() const { return m_pass; }
+};
 class AstPrintTimeScale final : public AstNodeStmt {
    // Parents: stmtlist
    string m_name;  // Parent module name
--- a/src/V3EmitV.cpp
+++ b/src/V3EmitV.cpp
@ -365,6 +365,7 @@ class EmitVBaseVisitorConst VL_NOT_FINAL : public VNVisitorConst {
    void visit(AstSFormat* nodep) override {
        visitNodeDisplay(nodep, nodep->lhsp(), nodep->fmtp()->text(), nodep->fmtp()->exprsp());
    }
+    void visit(AstToStringN* nodep) override { iterateConst(nodep->lhsp()); }
    void visit(AstSFormatF* nodep) override {
        visitNodeDisplay(nodep, nullptr, nodep->text(), nodep->exprsp());
    }
@ -799,9 +800,6 @@ class EmitVBaseVisitorConst VL_NOT_FINAL : public VNVisitorConst {
        puts(";\n");
    }
    void visit(AstNodeCoverOrAssert* nodep) override {
-        if (AstPExpr* const pexprp = VN_CAST(nodep->propp(), PExpr)) {
-            iterateAndNextConstNull(pexprp);
-        }
        putfs(nodep, nodep->verilogKwd() + " ");
        if (nodep->type() == VAssertType::OBSERVED_DEFERRED_IMMEDIATE) {
            puts("#0 ");
@ -812,14 +810,10 @@ class EmitVBaseVisitorConst VL_NOT_FINAL : public VNVisitorConst {
        }
        iterateConstNull(nodep->sentreep());
        puts("(");
-        if (const AstPExpr* const pexprp = VN_CAST(nodep->propp(), PExpr)) {
-            iterateAndNextConstNull(pexprp->condp());
+        if (AstSampled* const sampledp = VN_CAST(nodep->propp(), Sampled)) {
+            iterateAndNextConstNull(sampledp->exprp());
        } else {
-            if (AstSampled* const sampledp = VN_CAST(nodep->propp(), Sampled)) {
-                iterateAndNextConstNull(sampledp->exprp());
-            } else {
-                iterateAndNextConstNull(nodep->propp());
-            }
+            iterateAndNextConstNull(nodep->propp());
        }
        if (!VN_IS(nodep, Restrict)) {
            puts(") begin\n");
@ -1052,16 +1046,15 @@ class EmitVBaseVisitorConst VL_NOT_FINAL : public VNVisitorConst {
        iterateConstNull(nodep->propp());
        puts("\n");
    }
-    void visit(AstPExpr* nodep) override {
-        iterateAndNextConstNull(nodep->precondp());  // condp emitted by AstNodeCoverOrAssert
-    }
+    void visit(AstPExpr* nodep) override { iterateConst(nodep->bodyp()); }
    void visit(AstSExpr* nodep) override {
+        iterateConstNull(nodep->preExprp());
        {
            VL_RESTORER(m_suppressSemi);
            m_suppressSemi = true;
-            iterateConstNull(nodep->delayp());
+            iterateConst(nodep->delayp());
        }
-        iterateConstNull(nodep->exprp());
+        iterateConst(nodep->exprp());
    }

    // Terminals
--- a/src/V3Width.cpp
+++ b/src/V3Width.cpp
@ -215,6 +215,9 @@ class WidthVisitor final : public VNVisitor {
    V3TaskConnectState m_taskConnectState;  // State to cache V3Task::taskConnects
    WidthVP* m_vup = nullptr;  // Current node state
    bool m_underFork = false;  // Visiting under a fork
+    bool m_underSExpr = false;  // Visiting under a sequence expression
+    AstNode* m_seqUnsupp = nullptr;  // Property has unsupported node
+    bool m_hasSExpr = false;  // Property has a sequence expression
    const AstCell* m_cellp = nullptr;  // Current cell for arrayed instantiations
    const AstEnumItem* m_enumItemp = nullptr;  // Current enum item
    AstNodeFTask* m_ftaskp = nullptr;  // Current function/task
@ -1539,6 +1542,7 @@ class WidthVisitor final : public VNVisitor {
    }

    void visit(AstImplication* nodep) override {
+        m_seqUnsupp = nodep;
        if (m_vup->prelim()) {
            iterateCheckBool(nodep, "LHS", nodep->lhsp(), BOTH);
            iterateCheckBool(nodep, "RHS", nodep->rhsp(), BOTH);
@ -1557,9 +1561,15 @@ class WidthVisitor final : public VNVisitor {
        }
    }
    void visit(AstSExpr* nodep) override {
+        VL_RESTORER(m_underSExpr);
+        m_underSExpr = true;
+        m_hasSExpr = true;
        if (m_vup->prelim()) {
-            iterateCheckBool(nodep, "exprp", nodep->exprp(), BOTH);
+            if (nodep->preExprp()) {
+                iterateCheckBool(nodep, "preExprp", nodep->preExprp(), BOTH);
+            }
            iterate(nodep->delayp());
+            iterateCheckBool(nodep, "exprp", nodep->exprp(), BOTH);
            nodep->dtypeSetBit();
        }
    }
@ -5338,6 +5348,8 @@ class WidthVisitor final : public VNVisitor {
    }

    void visit(AstPropSpec* nodep) override {
+        VL_RESTORER(m_seqUnsupp);
+        VL_RESTORER(m_hasSExpr);
        if (m_vup->prelim()) {  // First stage evaluation
            iterateCheckBool(nodep, "Property", nodep->propp(), BOTH);
            userIterateAndNext(nodep->sensesp(), nullptr);
@ -5346,6 +5358,20 @@ class WidthVisitor final : public VNVisitor {
                                 BOTH);  // it's like an if() condition.
            }
            nodep->dtypeSetBit();
+            if (m_hasSExpr) {
+                if (VN_IS(m_seqUnsupp, Implication)) {
+                    m_seqUnsupp->v3warn(E_UNSUPPORTED,
+                                        "Unsupported: Implication with sequence expression");
+                    AstConst* const newp = new AstConst{nodep->fileline(), 0};
+                    newp->dtypeFrom(nodep);
+                    nodep->replaceWith(newp);
+                    VL_DO_DANGLING(pushDeletep(nodep), nodep);
+                } else if (nodep->disablep()) {
+                    nodep->disablep()->v3warn(E_UNSUPPORTED,
+                                              "Unsupported: Disable iff with sequence expression");
+                    VL_DO_DANGLING(pushDeletep(nodep->disablep()->unlinkFrBack()), nodep);
+                }
+            }
        }
    }

@ -7008,6 +7034,13 @@ class WidthVisitor final : public VNVisitor {
        if (m_vup->prelim()) {
            iterateCheckBool(nodep, "LHS", nodep->op1p(), BOTH);
            nodep->dtypeSetBit();
+            if (m_underSExpr) {
+                nodep->v3error("Unexpected 'not' in sequence expression context");
+                AstConst* const newp = new AstConst{nodep->fileline(), 0};
+                newp->dtypeFrom(nodep);
+                nodep->replaceWith(newp);
+                VL_DO_DANGLING(pushDeletep(nodep), nodep);
+            }
        }
    }
    void visit_log_and_or(AstNodeBiop* nodep) {
--- a/src/Verilator.cpp
+++ b/src/Verilator.cpp
@ -20,6 +20,7 @@
 #include "V3ActiveTop.h"
 #include "V3Assert.h"
 #include "V3AssertPre.h"
+#include "V3AssertProp.h"
 #include "V3Ast.h"
 #include "V3Begin.h"
 #include "V3Branch.h"
@ -240,6 +241,8 @@ static void process() {

        // Assertion insertion
        //    After we've added block coverage, but before other nasty transforms
+        V3AssertProp::assertPropAll(v3Global.rootp());
+        //
        V3AssertPre::assertPreAll(v3Global.rootp());
        //
        V3Assert::assertAll(v3Global.rootp());
--- a/src/verilog.y
+++ b/src/verilog.y
@ -6534,7 +6534,8 @@ pexpr<nodeExprp>:  // IEEE: property_expr  (The name pexpr is important as regex
        //                      // IEEE: '(' pexpr ')'
        //                      // Expanded below
        //
-                yNOT pexpr %prec prNEGATION             { $$ = new AstLogNot{$1, $2}; }
+                yNOT pexpr
+                        { $$ = new AstLogNot{$1, $2}; }
        |       ySTRONG '(' sexpr ')'
                        { $$ = $3; BBUNSUP($2, "Unsupported: strong (in property expression)"); }
        |       yWEAK '(' sexpr ')'
@ -6624,7 +6625,7 @@ sexpr<nodeExprp>:  // ==IEEE: sequence_expr  (The name sexpr is important as reg
                cycle_delay_range ~p~sexpr  %prec yP_POUNDPOUND
                        { $$ = new AstSExpr{$<fl>1, $1, $2}; }
        |       ~p~sexpr cycle_delay_range sexpr %prec prPOUNDPOUND_MULTI
-                        { $$ = $1; BBUNSUP($2->fileline(), "Unsupported: ## (in sequence expression)"); DEL($2, $3); }
+                        { $$ = new AstSExpr{$<fl>2, $1, $2, $3}; }
        //
        //                      // IEEE: expression_or_dist [ boolean_abbrev ]
        //                      // Note expression_or_dist includes "expr"!
--- a/test_regress/t/t_debug_emitv.out
+++ b/test_regress/t/t_debug_emitv.out
@ -277,6 +277,7 @@ module Vt_debug_emitv_t;
            str = $sformatf("cyc=%~", cyc);
            ;
            $display("str = %@", str);
+            $display("struct = %@", ps);
            $display("%% [%t] [%^] to=%o td=%d", $time, 
                     $realtime, $time, $time);
            $sscanf(40'h666f6f3d35, "foo=%d", i);
@ -365,9 +366,6 @@ module Vt_debug_emitv_t;
    property p1;
    @( clk) sum[0]
    endproperty
-    property p2;
-    @(posedge clk) disable iff (cyc == 'sh1) ##1 sum[0]
-    endproperty
    assert property (@( clk) (! ##1 in)
    ) begin
    end
--- a/test_regress/t/t_debug_emitv.v
+++ b/test_regress/t/t_debug_emitv.v
@ -218,6 +218,7 @@ module t (/*AUTOARG*/

      str = $sformatf("cyc=%d", cyc);
      $display("str = %s", str);
+      $display("struct = %p", ps);
      $display("%% [%t] [%t] to=%o td=%d", $time, $realtime, $time, $time);
      $sscanf("foo=5", "foo=%d", i);
      $printtimescale;
@ -276,9 +277,6 @@ module t (/*AUTOARG*/
   property p1;
      @(clk) sum[0]
   endproperty
-   property p2;
-      @(posedge clk) disable iff (cyc == 1) ##1 sum[0]
-   endproperty

   assert property (@(clk) not ##1 in);

--- a/test_regress/t/t_expect.out
+++ b/test_regress/t/t_expect.out
@ -1,19 +1,10 @@
-%Error-UNSUPPORTED: t/t_expect.v:19:32: Unsupported: ## (in sequence expression)
-   19 |       expect (@(posedge clk) a ##1 b) a = 110;
-      |                                ^~
-                    ... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest
 %Error-UNSUPPORTED: t/t_expect.v:19:7: Unsupported: expect
   19 |       expect (@(posedge clk) a ##1 b) a = 110;
      |       ^~~~~~
-%Error-UNSUPPORTED: t/t_expect.v:21:32: Unsupported: ## (in sequence expression)
-   21 |       expect (@(posedge clk) a ##1 b) else a = 299;
-      |                                ^~
+                    ... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest
 %Error-UNSUPPORTED: t/t_expect.v:21:7: Unsupported: expect
   21 |       expect (@(posedge clk) a ##1 b) else a = 299;
      |       ^~~~~~
-%Error-UNSUPPORTED: t/t_expect.v:23:32: Unsupported: ## (in sequence expression)
-   23 |       expect (@(posedge clk) a ##1 b) a = 300; else a = 399;
-      |                                ^~
 %Error-UNSUPPORTED: t/t_expect.v:23:7: Unsupported: expect
   23 |       expect (@(posedge clk) a ##1 b) a = 300; else a = 399;
      |       ^~~~~~
--- a/test_regress/t/t_property_sexpr.out
+++ b/test_regress/t/t_property_sexpr.out
@ -1,140 +1,134 @@
-[4] single delay with const stmt, fileline:115
-[5] concurrent assert else, fileline:167
-[6] single delay with const stmt, fileline:115
-[7] concurrent assert stmt, fileline:166
-[8] single delay with const stmt, fileline:115
-[9] concurrent assert else, fileline:167
-[11] concurrent assert else, fileline:167
-[12] single delay with var stmt, fileline:118
-[13] concurrent assert else, fileline:167
-[14] single delay with var else, fileline:119
-[15] concurrent assert stmt, fileline:166
-[16] single delay with var stmt, fileline:118
-[17] concurrent assert else, fileline:167
-[18] single delay with var else, fileline:119
-[19] concurrent assert else, fileline:167
-[20] single delay with var stmt, fileline:118
-[21] concurrent assert else, fileline:167
-[23] concurrent assert stmt, fileline:166
-[25] concurrent assert else, fileline:167
-[26] single multi-cycle delay with var else, fileline:123
-[27] concurrent assert else, fileline:167
-[28] single multi-cycle delay with var stmt, fileline:122
-[29] concurrent assert else, fileline:167
-[30] single multi-cycle delay with var else, fileline:123
-[31] concurrent assert stmt, fileline:166
-[33] concurrent assert else, fileline:167
-[34] single delay with var brackets 1 else, fileline:127
-[35] concurrent assert else, fileline:167
-[36] single delay with var brackets 1 stmt, fileline:126
-[37] concurrent assert else, fileline:167
-[38] single delay with var brackets 1 else, fileline:127
-[39] concurrent assert stmt, fileline:166
-[40] single delay with var brackets 1 stmt, fileline:126
-[41] concurrent assert else, fileline:167
-[43] concurrent assert else, fileline:167
-[44] single delay with var brackets 2 stmt, fileline:130
-[45] concurrent assert else, fileline:167
-[46] single delay with var brackets 2 else, fileline:131
-[47] concurrent assert stmt, fileline:166
-[48] single delay with var brackets 2 stmt, fileline:130
-[49] concurrent assert else, fileline:167
-[50] single delay with var brackets 2 else, fileline:131
-[51] concurrent assert else, fileline:167
-[53] concurrent assert else, fileline:167
-[54] single delay with negated var else, fileline:135
-[55] concurrent assert stmt, fileline:166
-[56] single delay with negated var stmt, fileline:134
-[57] concurrent assert else, fileline:167
-[58] single delay with negated var else, fileline:135
-[59] concurrent assert else, fileline:167
-[60] single delay with negated var else, fileline:135
-[61] concurrent assert else, fileline:167
-[63] concurrent assert stmt, fileline:166
-[64] single delay with negated var else, fileline:139
-[65] concurrent assert else, fileline:167
-[66] single delay with negated var stmt, fileline:138
-[67] concurrent assert else, fileline:167
-[68] single delay with negated var else, fileline:139
-[69] concurrent assert else, fileline:167
-[70] single delay with negated var stmt, fileline:138
-[71] concurrent assert stmt, fileline:166
-[73] concurrent assert else, fileline:167
-[74] single delay with negated var brackets stmt, fileline:142
-[75] concurrent assert else, fileline:167
-[76] single delay with negated var brackets else, fileline:144
-[77] concurrent assert else, fileline:167
-[78] single delay with negated var brackets stmt, fileline:142
-[79] concurrent assert stmt, fileline:166
-[80] single delay with negated var brackets else, fileline:144
-[81] concurrent assert else, fileline:167
-[83] concurrent assert else, fileline:167
-[84] single delay with negated var brackets else, fileline:148
-[85] concurrent assert else, fileline:167
-[87] concurrent assert stmt, fileline:166
-[88] single delay with negated var brackets else, fileline:148
-[89] concurrent assert else, fileline:167
-[91] concurrent assert else, fileline:167
-[93] concurrent assert else, fileline:167
-[94] single delay with nested not else, fileline:152
-[95] concurrent assert stmt, fileline:166
-[96] single delay with nested not stmt, fileline:151
-[97] concurrent assert else, fileline:167
-[98] single delay with nested not else, fileline:152
-[99] concurrent assert else, fileline:167
-[100] single delay with nested not stmt, fileline:151
-[101] concurrent assert else, fileline:167
-[103] concurrent assert stmt, fileline:166
-[105] concurrent assert else, fileline:167
-[107] concurrent assert else, fileline:167
-[109] concurrent assert else, fileline:167
-[111] concurrent assert stmt, fileline:166
-[113] concurrent assert else, fileline:167
-[114] property, fileline:162
-[115] concurrent assert else, fileline:167
-[116] property, fileline:163
-[117] concurrent assert else, fileline:167
-[118] property, fileline:162
-[119] concurrent assert stmt, fileline:166
-[120] property, fileline:163
-[121] concurrent assert else, fileline:167
-[123] concurrent assert else, fileline:167
-[125] concurrent assert else, fileline:167
-[127] concurrent assert stmt, fileline:166
-[129] concurrent assert else, fileline:167
-[131] concurrent assert else, fileline:167
-[133] concurrent assert else, fileline:167
-[135] concurrent assert stmt, fileline:166
-[137] concurrent assert else, fileline:167
-[139] concurrent assert else, fileline:167
-[141] concurrent assert else, fileline:167
-[143] concurrent assert stmt, fileline:166
-[145] concurrent assert else, fileline:167
-[147] concurrent assert else, fileline:167
-[149] concurrent assert else, fileline:167
-[151] concurrent assert stmt, fileline:166
-[153] concurrent assert else, fileline:167
-[155] concurrent assert else, fileline:167
-[157] concurrent assert else, fileline:167
-[159] concurrent assert stmt, fileline:166
-[161] concurrent assert else, fileline:167
-[163] concurrent assert else, fileline:167
-[165] concurrent assert else, fileline:167
-[167] concurrent assert stmt, fileline:166
-[169] concurrent assert else, fileline:167
-[171] concurrent assert else, fileline:167
-[173] concurrent assert else, fileline:167
-[175] concurrent assert stmt, fileline:166
-[177] concurrent assert else, fileline:167
-[179] concurrent assert else, fileline:167
-[181] concurrent assert else, fileline:167
-[183] concurrent assert stmt, fileline:166
-[185] concurrent assert else, fileline:167
-[187] concurrent assert else, fileline:167
-[189] concurrent assert else, fileline:167
-[191] concurrent assert stmt, fileline:166
-[193] concurrent assert else, fileline:167
-[195] concurrent assert else, fileline:167
-[197] concurrent assert else, fileline:167
-[199] concurrent assert stmt, fileline:166
+[2] triggered e1
+[4] triggered e1
+[4] single delay with const stmt, fileline:99
+[6] triggered e1
+[6] single delay with const stmt, fileline:99
+[8] triggered e2
+[10] triggered e2
+[10] single delay with var stmt, fileline:102
+[12] triggered e2
+[12] single delay with var else, fileline:103
+[14] triggered e2
+[14] single delay with var stmt, fileline:102
+[16] triggered e2
+[16] single delay with var else, fileline:103
+[18] triggered e2
+[18] single delay with var stmt, fileline:102
+[20] triggered e3
+[22] triggered e3
+[22] stmt1, fileline:106
+[22] stmt2, fileline:107
+[24] triggered e3
+[24] else1, fileline:110
+[24] else2, fileline:111
+[26] triggered e3
+[26] stmt1, fileline:106
+[26] stmt2, fileline:107
+[28] triggered e3
+[28] else1, fileline:110
+[28] else2, fileline:111
+[30] triggered e4
+[32] triggered e4
+[34] triggered e4
+[34] single multi-cycle delay with var stmt, fileline:115
+[36] triggered e4
+[36] single multi-cycle delay with var else, fileline:116
+[38] triggered e4
+[38] single multi-cycle delay with var stmt, fileline:115
+[40] triggered e5
+[42] triggered e5
+[42] single delay with var brackets 1 stmt, fileline:119
+[44] triggered e5
+[44] single delay with var brackets 1 else, fileline:120
+[46] triggered e5
+[46] single delay with var brackets 1 stmt, fileline:119
+[48] triggered e5
+[48] single delay with var brackets 1 else, fileline:120
+[50] triggered e6
+[52] triggered e6
+[52] single delay with var brackets 2 else, fileline:124
+[54] triggered e6
+[54] single delay with var brackets 2 stmt, fileline:123
+[56] triggered e6
+[56] single delay with var brackets 2 else, fileline:124
+[58] triggered e6
+[58] single delay with var brackets 2 stmt, fileline:123
+[60] triggered e7
+[62] triggered e7
+[62] single delay with and var stmt, fileline:127
+[64] triggered e7
+[64] single delay with and var else, fileline:128
+[66] triggered e7
+[66] single delay with and var else, fileline:128
+[68] triggered e7
+[68] single delay with and var else, fileline:128
+[70] triggered e8
+[72] triggered e8
+[72] single delay with negated var stmt, fileline:131
+[74] triggered e8
+[74] single delay with negated var else, fileline:132
+[76] triggered e8
+[76] single delay with negated var stmt, fileline:131
+[78] triggered e8
+[78] single delay with negated var else, fileline:132
+[80] triggered e9
+[82] triggered e9
+[82] single delay with negated var brackets else, fileline:137
+[84] triggered e9
+[84] single delay with negated var brackets stmt, fileline:135
+[86] triggered e9
+[86] single delay with negated var brackets else, fileline:137
+[88] triggered e9
+[88] single delay with negated var brackets stmt, fileline:135
+[90] triggered e10
+[92] triggered e10
+[94] triggered e10
+[94] single delay with negated var brackets else, fileline:141
+[96] triggered e10
+[98] triggered e10
+[98] single delay with negated var brackets else, fileline:141
+[100] triggered e11
+[102] triggered e11
+[102] single delay with nested not stmt, fileline:144
+[104] triggered e11
+[104] single delay with nested not else, fileline:145
+[106] triggered e11
+[106] single delay with nested not stmt, fileline:144
+[108] triggered e11
+[108] single delay with nested not else, fileline:145
+[110] triggered e12
+[112] triggered e12
+[114] triggered e12
+[114] stmt, fileline:        148
+[116] triggered e12
+[116] else, fileline:        150
+[118] triggered e12
+[118] stmt, fileline:        148
+[120] triggered e13
+[122] triggered e13
+[122] property, fileline:161
+[124] triggered e13
+[124] property, fileline:160
+[126] triggered e13
+[126] property, fileline:161
+[128] triggered e13
+[128] property, fileline:160
+[130] triggered e14
+[132] triggered e14
+[132] else, fileline:        166
+[134] triggered e14
+[134] stmt, fileline:        164
+[136] triggered e14
+[136] else, fileline:        166
+[138] triggered e14
+[138] else, fileline:        166
+[140] triggered e15
+[140] else, fileline:        171
+[142] triggered e15
+[144] triggered e15
+[144] else, fileline:        171
+[144] else, fileline:        171
+[146] triggered e15
+[148] triggered e15
+[148] else, fileline:        171
 *-* All Finished *-*
--- a/test_regress/t/t_property_sexpr.v
+++ b/test_regress/t/t_property_sexpr.v
@ -4,6 +4,9 @@
 // without warranty, 2025 by Antmicro.
 // SPDX-License-Identifier: CC0-1.0

+`define STRINGIFY(x) `"x`"
+`define TRIGGER(e) ->e; $display("[%0t] triggered %s", $time, `STRINGIFY(e))
+
 module t (  /*AUTOARG*/
    // Inputs
    clk
@ -11,7 +14,7 @@ module t (  /*AUTOARG*/

  input clk;

-  bit [3:0] val = 0;
+  bit [1:0] val = 0;
  event e1;
  event e2;
  event e3;
@ -24,92 +27,73 @@ module t (  /*AUTOARG*/
  event e10;
  event e11;
  event e12;
+  event e13;
+  event e14;
+  event e15;
+
  integer cyc = 1;

-  always @(negedge clk) begin
-    val <= 4'(cyc % 4);
-
-    if (cyc >= 0 && cyc <= 4) begin
-      ->e1;
+  always @(posedge clk) begin
+    ++val;
+    ++cyc;
 `ifdef TEST_VERBOSE
-      $display("[%0t] triggered e1", $time);
+    $display("[%0t] cyc=%0d val=%0d", $time, cyc, val);
 `endif
-    end
-    if (cyc >= 5 && cyc <= 10) begin
-      ->e2;
-`ifdef TEST_VERBOSE
-      $display("[%0t] triggered e2", $time);
-`endif
-    end
-    if (cyc >= 11 && cyc <= 15) begin
-      ->e3;
-`ifdef TEST_VERBOSE
-      $display("[%0t] triggered e3", $time);
-`endif
-    end
-    if (cyc >= 16 && cyc <= 20) begin
-      ->e4;
-`ifdef TEST_VERBOSE
-      $display("[%0t] triggered e4", $time);
-`endif
-    end
-    if (cyc >= 21 && cyc <= 25) begin
-      ->e5;
-`ifdef TEST_VERBOSE
-      $display("[%0t] triggered e5", $time);
-`endif
-    end
-    if (cyc >= 26 && cyc <= 30) begin
-      ->e6;
-`ifdef TEST_VERBOSE
-      $display("[%0t] triggered e6", $time);
-`endif
-    end
-    if (cyc >= 31 && cyc <= 35) begin
-      ->e7;
-`ifdef TEST_VERBOSE
-      $display("[%0t] triggered e7", $time);
-`endif
-    end
-    if (cyc >= 36 && cyc <= 40) begin
-      ->e8;
-`ifdef TEST_VERBOSE
-      $display("[%0t] triggered e8", $time);
-`endif
-    end
-    if (cyc >= 41 && cyc <= 45) begin
-      ->e9;
-`ifdef TEST_VERBOSE
-      $display("[%0t] triggered e9", $time);
-`endif
-    end
-    if (cyc >= 46 && cyc <= 50) begin
-      ->e10;
-`ifdef TEST_VERBOSE
-      $display("[%0t] triggered e10", $time);
-`endif
-    end
-    if (cyc >= 51 && cyc <= 55) begin
-      ->e11;
-`ifdef TEST_VERBOSE
-      $display("[%0t] triggered e11", $time);
-`endif
-    end
-    if (cyc >= 56 && cyc <= 60) begin
-      ->e12;
-`ifdef TEST_VERBOSE
-      $display("[%0t] triggered e12", $time);
-`endif
-    end
-`ifdef TEST_VERBOSE
-    $display("cyc=%0d val=%0d", cyc, val);
-`endif
-    cyc <= cyc + 1;
    if (cyc == 100) begin
      $write("*-* All Finished *-*\n");
      $finish;
    end
  end
+  always @(negedge clk) begin
+    if (cyc >= 0 && cyc <= 4) begin
+      `TRIGGER(e1);
+    end
+    if (cyc >= 5 && cyc <= 10) begin
+      `TRIGGER(e2);
+    end
+    if (cyc >= 11 && cyc <= 15) begin
+      `TRIGGER(e3);
+    end
+    if (cyc >= 16 && cyc <= 20) begin
+      `TRIGGER(e4);
+    end
+    if (cyc >= 21 && cyc <= 25) begin
+      `TRIGGER(e5);
+    end
+    if (cyc >= 26 && cyc <= 30) begin
+      `TRIGGER(e6);
+    end
+    if (cyc >= 31 && cyc <= 35) begin
+      `TRIGGER(e7);
+    end
+    if (cyc >= 36 && cyc <= 40) begin
+      `TRIGGER(e8);
+    end
+    if (cyc >= 41 && cyc <= 45) begin
+      `TRIGGER(e9);
+    end
+    if (cyc >= 46 && cyc <= 50) begin
+      `TRIGGER(e10);
+    end
+    if (cyc >= 51 && cyc <= 55) begin
+      `TRIGGER(e11);
+    end
+    if (cyc >= 56 && cyc <= 60) begin
+      `TRIGGER(e12);
+    end
+    if (cyc >= 61 && cyc <= 65) begin
+      `TRIGGER(e13);
+    end
+    if (cyc >= 66 && cyc <= 70) begin
+      `TRIGGER(e14);
+    end
+    if (cyc >= 71 && cyc <= 75) begin
+      `TRIGGER(e15);
+    end
+  end
+
+
+  assert property (@(e1) ##1 1);

  assert property (@(e1) ##1 1)
    $display("[%0t] single delay with const stmt, fileline:%0d", $time, `__LINE__);
@ -118,51 +102,71 @@ module t (  /*AUTOARG*/
    $display("[%0t] single delay with var stmt, fileline:%0d", $time, `__LINE__);
  else $display("[%0t] single delay with var else, fileline:%0d", $time, `__LINE__);

-  assert property (@(e3) ##2 val[0])
+  assert property (@(e3) ##1 val[0]) begin
+    $display("[%0t] stmt1, fileline:%0d", $time, `__LINE__);
+    $display("[%0t] stmt2, fileline:%0d", $time, `__LINE__);
+  end
+  else begin
+    $display("[%0t] else1, fileline:%0d", $time, `__LINE__);
+    $display("[%0t] else2, fileline:%0d", $time, `__LINE__);
+  end
+
+  assert property (@(e4) ##2 val[0])
    $display("[%0t] single multi-cycle delay with var stmt, fileline:%0d", $time, `__LINE__);
  else $display("[%0t] single multi-cycle delay with var else, fileline:%0d", $time, `__LINE__);

-  assert property (@(e4) ##1 (val[0]))
+  assert property (@(e5) ##1 (val[0]))
    $display("[%0t] single delay with var brackets 1 stmt, fileline:%0d", $time, `__LINE__);
  else $display("[%0t] single delay with var brackets 1 else, fileline:%0d", $time, `__LINE__);

-  assert property (@(e5) (##1 (val[0])))
+  assert property (@(e6) (##1 (val[0])))
    $display("[%0t] single delay with var brackets 2 stmt, fileline:%0d", $time, `__LINE__);
  else $display("[%0t] single delay with var brackets 2 else, fileline:%0d", $time, `__LINE__);

-  assert property (@(e6) (##1 val[0] && val[1]))
+  assert property (@(e7) (##1 val[0] && val[1]))
+    $display("[%0t] single delay with and var stmt, fileline:%0d", $time, `__LINE__);
+  else $display("[%0t] single delay with and var else, fileline:%0d", $time, `__LINE__);
+
+  assert property (@(e8) not not not ##1 val[0])
    $display("[%0t] single delay with negated var stmt, fileline:%0d", $time, `__LINE__);
  else $display("[%0t] single delay with negated var else, fileline:%0d", $time, `__LINE__);

-  assert property (@(e7) not ##1 val[0])
-    $display("[%0t] single delay with negated var stmt, fileline:%0d", $time, `__LINE__);
-  else $display("[%0t] single delay with negated var else, fileline:%0d", $time, `__LINE__);
-
-  assume property (@(e8) not (##1 val[0]))
+  assume property (@(e9) not (##1 val[0]))
    $display("[%0t] single delay with negated var brackets stmt, fileline:%0d", $time, `__LINE__);
  else
    $display("[%0t] single delay with negated var brackets else, fileline:%0d", $time, `__LINE__);

-  assume property (@(e9) not (##1 val[0]))
+  assume property (@(e10) not (##1 val[0]))
  else
    $display("[%0t] single delay with negated var brackets else, fileline:%0d", $time, `__LINE__);

-  assert property (@(e10) not (not ##1 val[0]))
+  assert property (@(e11) not (not ##1 val[0]))
    $display("[%0t] single delay with nested not stmt, fileline:%0d", $time, `__LINE__);
  else $display("[%0t] single delay with nested not else, fileline:%0d", $time, `__LINE__);

-  restrict property (@(e11) ##1 val[0]);
-
-  restrict property (@(e11) not ##1 val[0]);
+  assert property (@(e12) not (not ##2 val[0] && val[0]))
+    $display("[%0t] stmt, fileline:%d", $time, `__LINE__);
+  else
+    $display("[%0t] else, fileline:%d", $time, `__LINE__);
+`ifdef VERILATOR
+  restrict property (@(e12) ##1 val[0]);

+  restrict property (@(e12) not ##1 val[0]);
+`endif
  property prop;
-    @(e12) not ##1 val[0]
+    @(e13) not ##1 val[0]
  endproperty

  assert property (prop) $display("[%0t] property, fileline:%0d", $time, `__LINE__);
  else $display("[%0t] property, fileline:%0d", $time, `__LINE__);

-  assert property (@(posedge clk) not (not ##2 val[0] && val[1]))
-    $display("[%0t] concurrent assert stmt, fileline:%0d", $time, `__LINE__);
-  else $display("[%0t] concurrent assert else, fileline:%0d", $time, `__LINE__);
+  assert property (@(e14) val[0] ##2 val[1])
+    $display("[%0t] stmt, fileline:%d", $time, `__LINE__);
+  else
+    $display("[%0t] else, fileline:%d", $time, `__LINE__);
+
+  assert property (@(e15) val[0] ##1 val[1] ##1 val[0])
+    $display("[%0t] stmt, fileline:%d", $time, `__LINE__);
+  else
+    $display("[%0t] else, fileline:%d", $time, `__LINE__);
 endmodule
--- a/test_regress/t/t_property_sexpr_bad.out
+++ b/test_regress/t/t_property_sexpr_bad.out
@ -1,6 +1,6 @@
-%Error: t/t_property_sexpr_bad.v:20:39: Syntax error: unexpected 'not' in sequence expression
+%Error: t/t_property_sexpr_bad.v:20:39: Unexpected 'not' in sequence expression context
                                      : ... note: In instance 't'
-   20 |   assert property (@(posedge clk) ##1 not val) $display("[%0t] single delay with negated var stmt, fileline:%d", $time, 20);
+   20 |   assert property (@(posedge clk) ##1 not val);
      |                                       ^~~
        ... See the manual at https://verilator.org/verilator_doc.html?v=latest for more assistance.
 %Error: Exiting due to
--- a/test_regress/t/t_property_sexpr_bad.v
+++ b/test_regress/t/t_property_sexpr_bad.v
@ -12,10 +12,10 @@ module t (  /*AUTOARG*/
  input clk;
  bit val;

-  always @(negedge clk) begin
+  always @(posedge clk) begin
    $write("*-* All Finished *-*\n");
    $finish;
  end

-  assert property (@(posedge clk) ##1 not val) $display("[%0t] single delay with negated var stmt, fileline:%d", $time, `__LINE__);
+  assert property (@(posedge clk) ##1 not val);
 endmodule
--- a/test_regress/t/t_property_sexpr_cov.dat.out
+++ b/test_regress/t/t_property_sexpr_cov.dat.out
@ -0,0 +1,5 @@
+# SystemC::Coverage-3
+C 'ft/t_property_sexpr_cov.vl44n3tuserpagev_user/tocoverhtop.t' 2
+C 'ft/t_property_sexpr_cov.vl47n3tuserpagev_user/tocoverhtop.t' 2
+C 'ft/t_property_sexpr_cov.vl50n3tuserpagev_user/tocoverhtop.t' 3
+C 'ft/t_property_sexpr_cov.vl53n3tuserpagev_user/tocoverhtop.t' 25
--- a/test_regress/t/t_property_sexpr_cov.out
+++ b/test_regress/t/t_property_sexpr_cov.out
@ -1,31 +1,33 @@
 [4] cover property, fileline:45
-[7] concurrent cover, fileline:51
+[4] cover property, fileline:48
+[7] concurrent cover, fileline:54
 [8] cover property, fileline:45
-[12] not cover property, fileline:48
-[15] concurrent cover, fileline:51
-[18] not cover property, fileline:48
-[20] not cover property, fileline:48
-[23] concurrent cover, fileline:51
-[31] concurrent cover, fileline:51
-[39] concurrent cover, fileline:51
-[47] concurrent cover, fileline:51
-[55] concurrent cover, fileline:51
-[63] concurrent cover, fileline:51
-[71] concurrent cover, fileline:51
-[79] concurrent cover, fileline:51
-[87] concurrent cover, fileline:51
-[95] concurrent cover, fileline:51
-[103] concurrent cover, fileline:51
-[111] concurrent cover, fileline:51
-[119] concurrent cover, fileline:51
-[127] concurrent cover, fileline:51
-[135] concurrent cover, fileline:51
-[143] concurrent cover, fileline:51
-[151] concurrent cover, fileline:51
-[159] concurrent cover, fileline:51
-[167] concurrent cover, fileline:51
-[175] concurrent cover, fileline:51
-[183] concurrent cover, fileline:51
-[191] concurrent cover, fileline:51
-[199] concurrent cover, fileline:51
+[8] cover property, fileline:48
+[12] not cover property, fileline:51
+[15] concurrent cover, fileline:54
+[18] not cover property, fileline:51
+[20] not cover property, fileline:51
+[23] concurrent cover, fileline:54
+[31] concurrent cover, fileline:54
+[39] concurrent cover, fileline:54
+[47] concurrent cover, fileline:54
+[55] concurrent cover, fileline:54
+[63] concurrent cover, fileline:54
+[71] concurrent cover, fileline:54
+[79] concurrent cover, fileline:54
+[87] concurrent cover, fileline:54
+[95] concurrent cover, fileline:54
+[103] concurrent cover, fileline:54
+[111] concurrent cover, fileline:54
+[119] concurrent cover, fileline:54
+[127] concurrent cover, fileline:54
+[135] concurrent cover, fileline:54
+[143] concurrent cover, fileline:54
+[151] concurrent cover, fileline:54
+[159] concurrent cover, fileline:54
+[167] concurrent cover, fileline:54
+[175] concurrent cover, fileline:54
+[183] concurrent cover, fileline:54
+[191] concurrent cover, fileline:54
+[199] concurrent cover, fileline:54
 *-* All Finished *-*
--- a/test_regress/t/t_property_sexpr_cov.py
+++ b/test_regress/t/t_property_sexpr_cov.py
@ -14,5 +14,6 @@ test.scenarios('simulator')
 test.compile(timing_loop=True, verilator_flags2=['--assert', '--timing', '--coverage-user'])

 test.execute(expect_filename=test.golden_filename)
+test.files_identical(test.obj_dir + "/coverage.dat", "t/t_property_sexpr_cov.dat.out")

 test.passes()
--- a/test_regress/t/t_property_sexpr_cov.v
+++ b/test_regress/t/t_property_sexpr_cov.v
@ -41,6 +41,9 @@ module t (  /*AUTOARG*/
    end
  end

+  cover property (@(e1) ##1 val[0])
+    $display("[%0t] cover property, fileline:%0d", $time, `__LINE__);
+
  cover property (@(e1) ##1 val[0])
    $display("[%0t] cover property, fileline:%0d", $time, `__LINE__);

--- a/test_regress/t/t_property_sexpr_multi.py
+++ b/test_regress/t/t_property_sexpr_multi.py
@ -0,0 +1,18 @@
+#!/usr/bin/env python3
+# DESCRIPTION: Verilator: Verilog Test driver/expect definition
+#
+# Copyright 2025 by Wilson Snyder. 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-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', '--dumpi-V3AssertProp 6'])
+
+test.execute()
+
+test.passes()
--- a/test_regress/t/t_property_sexpr_multi.v
+++ b/test_regress/t/t_property_sexpr_multi.v
@ -0,0 +1,249 @@
+// DESCRIPTION: Verilator: Verilog Test module
+//
+// This file ONLY is placed into the Public Domain, for any use,
+// without warranty, 2025 by Antmicro.
+// SPDX-License-Identifier: CC0-1.0
+
+`define STRINGIFY(x) `"x`"
+`define TRIGGER(e) ->e; $display("[cyc=%0d, val=%0d] triggered %s", cyc, val, `STRINGIFY(e))
+
+`define stop $stop
+`define checkh(gotv,expv) do if ((gotv) !== (expv)) begin $write("%%Error: %s:%0d:  got='h%p exp='h%p\n", `__FILE__,`__LINE__, (gotv), (expv)); `stop; end while(0)
+`define checkd(gotv,expv) do if ((gotv) !== (expv)) begin $write("%%Error: %s:%0d:  got=%0d exp=%0d (%s !== %s)\n", `__FILE__,`__LINE__, (gotv), (expv), `"gotv`", `"expv`"); `stop; end while(0);
+
+module t (  /*AUTOARG*/
+    // Inputs
+    clk
+);
+
+  input clk;
+
+  bit [1:0] val = 0;
+  event e1;
+  event e2;
+  event e3;
+  event e4;
+  event e5;
+  event e6;
+  event e7;
+  event e8;
+  event e9;
+  event e10;
+  event e11;
+  event e12;
+  integer cyc = 1;
+
+  typedef struct {
+    bit fails;
+    bit passs;
+  } result_t;
+
+  result_t results [int];
+  result_t expected [int];
+
+  localparam MAX = 66;
+  always @(posedge clk) begin
+    ++val;
+    ++cyc;
+
+    if (cyc == MAX + 1) begin
+      expected[6] = '{1, 0};
+      expected[7] = '{1, 0};
+      expected[8] = '{1, 1};
+
+      expected[11] = '{1, 0};
+      expected[12] = '{1, 0};
+      expected[13] = '{1, 0};
+      expected[15] = '{1, 0};
+      expected[16] = '{1, 1};
+      expected[17] = '{1, 0};
+
+      expected[20] = '{1, 0};
+      expected[21] = '{1, 0};
+      expected[23] = '{1, 0};
+      expected[24] = '{1, 0};
+      expected[25] = '{1, 0};
+      expected[27] = '{1, 1};
+
+      expected[29] = '{1, 0};
+      expected[30] = '{1, 0};
+
+      expected[32] = '{1, 0};
+      expected[33] = '{1, 0};
+
+      expected[35] = '{1, 0};
+      expected[36] = '{1, 0};
+
+      expected[39] = '{1, 1};
+      expected[40] = '{0, 1};
+      expected[41] = '{0, 1};
+
+      expected[43] = '{1, 0};
+      expected[44] = '{1, 0};
+      expected[45] = '{1, 0};
+
+      expected[48] = '{0, 1};
+      expected[49] = '{0, 1};
+      expected[51] = '{1, 1};
+
+      expected[52] = '{0, 1};
+      expected[54] = '{0, 1};
+      expected[55] = '{1, 1};
+      expected[56] = '{0, 1};
+
+      expected[58] = '{1, 0};
+      expected[59] = '{1, 1};
+      expected[60] = '{1, 0};
+
+      expected[62] = '{0, 1};
+      expected[63] = '{0, 1};
+      expected[64] = '{0, 1};
+      expected[66] = '{0, 1};
+      `checkh(results, expected);
+      $write("*-* All Finished *-*\n");
+      $finish;
+    end
+  end
+
+  always @(negedge clk) begin
+    if (cyc >= 5 && cyc <= 9) begin
+      `TRIGGER(e1);
+    end
+    if (cyc >= 10 && cyc <= 18) begin
+      `TRIGGER(e2);
+    end
+    if (cyc >= 19 && cyc <= 27) begin
+      `TRIGGER(e3);
+    end
+    if (cyc >= 28 && cyc <= 30) begin
+      `TRIGGER(e4);
+    end
+    if (cyc >= 31 && cyc <= 33) begin
+      `TRIGGER(e5);
+    end
+    if (cyc >= 34 && cyc <= 36) begin
+      `TRIGGER(e6);
+    end
+    if (cyc >= 37 && cyc <= 41) begin
+      `TRIGGER(e7);
+    end
+    if (cyc >= 42 && cyc <= 46) begin
+      `TRIGGER(e8);
+    end
+    if (cyc >= 47 && cyc <= 51) begin
+      `TRIGGER(e9);
+    end
+    if (cyc >= 52 && cyc <= 56) begin
+      `TRIGGER(e10);
+    end
+    if (cyc >= 57 && cyc <= 61) begin
+      `TRIGGER(e11);
+    end
+    if (cyc >= 62 && cyc <= MAX) begin
+      `TRIGGER(e12);
+    end
+  end
+
+  assert property (@(e1) ##1 1 ##1 1);
+
+  assert property (@(e1) val == 0 ##1 val == 1 ##1 val == 2 ##1 val == 3)
+    results[cyc].passs = 1;
+  else
+    results[cyc].fails = 1;
+
+  assert property (@(e2) ##1 val == 1 ##2 val == 3)
+    results[cyc].passs = 1;
+  else
+    results[cyc].fails = 1;
+
+  assert property (@(e3) ##1 val == 1 ##2 val == 3 ##3 val == 2)
+    results[cyc].passs = 1;
+  else
+    results[cyc].fails = 1;
+
+  // Test failure at each step
+  assert property (@(e4) cyc == 28 ##1 cyc == 0 ##1 cyc == 30)
+    results[cyc].passs = 1;
+  else
+    results[cyc].fails = 1;
+
+  assert property (@(e5) cyc == 31 ##1 cyc == 32 ##1 cyc == 0)
+    results[cyc].passs = 1;
+  else
+    results[cyc].fails = 1;
+
+  assert property (@(e6) ##1 cyc == 34 ##1 cyc == 0)
+    results[cyc].passs = 1;
+  else
+    results[cyc].fails = 1;
+
+  assert property (@(e7) not ##1 val == 1 ##1 val == 2)
+    results[cyc].passs = 1;
+  else
+    results[cyc].fails = 1;
+
+  assert property (@(e8) not not ##1 val == 1 ##1 val == 2)
+    results[cyc].passs = 1;
+  else
+    results[cyc].fails = 1;
+
+  assert property (@(e9) not not not ##1 val == 1 ##1 val == 2)
+    results[cyc].passs = 1;
+  else
+    results[cyc].fails = 1;
+
+  assert property (@(e10) not val == 0 ##1 val == 1 ##1 val == 2)
+    results[cyc].passs = 1;
+  else
+    results[cyc].fails = 1;
+
+  assert property (@(e11) not not val == 0 ##1 val == 1 ##1 val == 2)
+    results[cyc].passs = 1;
+  else
+    results[cyc].fails = 1;
+
+  assert property (@(e12) not not not val == 0 ##1 val == 1 ##1 val == 2)
+    results[cyc].passs = 1;
+  else
+    results[cyc].fails = 1;
+
+  empty_body_tests empty_body_tests(.clk(clk));
+endmodule
+
+module empty_body_tests(input clk);
+  event e;
+  int cyc = 0;
+  bit[7:0] hit = 0;
+  always @(posedge clk) begin
+    ++cyc;
+    if (cyc < 5) ->e;
+    else `checkd(hit, 'b1111111);
+  end
+
+  assert property (@(e) ##1 1 ##1 1);
+  assert property (@(e) 1 ##1 1 ##1 1);
+  assert property (@(e) 1 ##1 1);
+
+  assert property (@(e) ##1 1 ##1 1) begin
+    hit |= 'b1;
+  end
+  assert property (@(e) 1 ##1 1 ##1 1) begin
+    hit |= 'b10;
+  end
+  assert property (@(e) 1 ##1 1) begin
+    hit |= 'b100;
+  end
+
+  assert property (@(e) ##1 1 ##1 0) else begin
+    hit |= 'b1000;
+  end
+  assert property (@(e) ##1 0) else begin
+    hit |= 'b10000;
+  end
+  assert property (@(e) 1 ##1 1 ##1 0) else begin
+    hit |= 'b100000;
+  end
+  assert property (@(e) 1 ##1 0) else begin
+    hit |= 'b1000000;
+  end
+endmodule
--- a/test_regress/t/t_property_sexpr_parse_unsup.out
+++ b/test_regress/t/t_property_sexpr_parse_unsup.out
@ -1,35 +1,23 @@
-%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:29:39: Unsupported: ## (in sequence expression)
-   29 |   assert property (@(posedge clk) val ##1 val) $display("[%0t] var with single delay stmt, fileline:%d", $time, 29);
-      |                                       ^~
-                    ... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest
-%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:30:43: Unsupported: ## (in sequence expression)
-   30 |   assert property (@(posedge clk) ##1 val ##2 val) $display("[%0t] sequence stmt, fileline:%d", $time, 30);
-      |                                           ^~
-%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:71:14: Unsupported: sequence match items
-   71 |     ($rose(a), l_b = b) |-> ##[3:10] q[l_b];
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:75:14: Unsupported: sequence match items
+   75 |     ($rose(a), l_b = b) |-> ##[3:10] q[l_b];
      |              ^
-%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:71:29: Unsupported: ## range cycle delay range expression
-   71 |     ($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:75:29: Unsupported: ## range cycle delay range expression
+   75 |     ($rose(a), l_b = b) |-> ##[3:10] q[l_b];
      |                             ^~
-%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:70:13: Unsupported: property variable declaration
-   70 |     integer l_b;
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:74:13: Unsupported: property variable declaration
+   74 |     integer l_b;
      |             ^~~
-%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:88:16: Unsupported: sequence match items
-   88 |     (count == 0, l_t = $realtime) ##1 (count == 7)[->1] |-> $realtime - l_t < 50.5;
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:92:16: Unsupported: sequence match items
+   92 |     (count == 0, l_t = $realtime) ##1 (count == 7)[->1] |-> $realtime - l_t < 50.5;
      |                ^
-%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:88:51: Unsupported: [-> boolean abbrev expression
-   88 |     (count == 0, l_t = $realtime) ##1 (count == 7)[->1] |-> $realtime - l_t < 50.5;
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:92:51: Unsupported: [-> boolean abbrev expression
+   92 |     (count == 0, l_t = $realtime) ##1 (count == 7)[->1] |-> $realtime - l_t < 50.5;
      |                                                   ^~~
-%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:88:54: Unsupported: boolean abbrev (in sequence expression)
-   88 |     (count == 0, l_t = $realtime) ##1 (count == 7)[->1] |-> $realtime - l_t < 50.5;
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:92:54: Unsupported: boolean abbrev (in sequence expression)
+   92 |     (count == 0, l_t = $realtime) ##1 (count == 7)[->1] |-> $realtime - l_t < 50.5;
      |                                                      ^
-%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:88:35: Unsupported: ## (in sequence expression)
-   88 |     (count == 0, l_t = $realtime) ##1 (count == 7)[->1] |-> $realtime - l_t < 50.5;
-      |                                   ^~
-%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:86:14: Unsupported: property variable declaration
-   86 |     realtime l_t;
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:90:14: Unsupported: property variable declaration
+   90 |     realtime l_t;
      |              ^~~
-%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:92:31: Unsupported: ## (in sequence expression)
-   92 |   assert property (@clk not a ##1 b);
-      |                               ^~
 %Error: Exiting due to
--- a/test_regress/t/t_property_sexpr_unsup.out
+++ b/test_regress/t/t_property_sexpr_unsup.out
@ -1,35 +1,50 @@
-%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:32:41: Unsupported: Implication with sequence expression
-   32 |   assert property (@(posedge clk) ##1 1 |-> 1) $display("[%0t] single delay with const implication stmt, fileline:%d", $time, 32);
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:29:41: Unsupported: Implication with sequence expression
+                                                    : ... note: In instance 't'
+   29 |   assert property (@(posedge clk) ##1 1 |-> 1) $display("[%0t] single delay with const implication stmt, fileline:%d", $time, 29);
      |                                         ^~~
                    ... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest
-%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:34:41: Unsupported: Implication with sequence expression
-   34 |   assert property (@(posedge clk) ##1 1 |-> not (val)) $display("[%0t] single delay implication with negated var stmt, fileline:%d", $time, 34);
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:31:41: Unsupported: Implication with sequence expression
+                                                    : ... note: In instance 't'
+   31 |   assert property (@(posedge clk) ##1 1 |-> not (val)) $display("[%0t] single delay implication with negated var stmt, fileline:%d", $time, 31);
      |                                         ^~~
-%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:36:37: Unsupported: Implication with sequence expression
-   36 |   assert property (@(posedge clk) 1 |-> ##1 val) $display("[%0t] single delay implication with negated var stmt, fileline:%d", $time, 36);
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:33:37: Unsupported: Implication with sequence expression
+                                                    : ... note: In instance 't'
+   33 |   assert property (@(posedge clk) 1 |-> ##1 val) $display("[%0t] single delay implication with negated var stmt, fileline:%d", $time, 33);
      |                                     ^~~
-%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:38:45: Unsupported: Implication with sequence expression
-   38 |   assert property (@(posedge clk) (##1 val) |-> (not val)) $display("[%0t] single delay with negated implication stmt, fileline:%d", $time, 38);
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:35:45: Unsupported: Implication with sequence expression
+                                                    : ... note: In instance 't'
+   35 |   assert property (@(posedge clk) (##1 val) |-> (not val)) $display("[%0t] single delay with negated implication stmt, fileline:%d", $time, 35);
      |                                             ^~~
-%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:40:45: Unsupported: Implication with sequence expression
-   40 |   assert property (@(posedge clk) ##1 (val) |-> not (val)) $display("[%0t] single delay with negated implication brackets stmt, fileline:%d", $time, 40);
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:37:45: Unsupported: Implication with sequence expression
+                                                    : ... note: In instance 't'
+   37 |   assert property (@(posedge clk) ##1 (val) |-> not (val)) $display("[%0t] single delay with negated implication brackets stmt, fileline:%d", $time, 37);
      |                                             ^~~
-%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:44:41: Unsupported: Implication with sequence expression
-   44 |   assert property (@(posedge clk) ##1 1 |-> 0) $display("[%0t] disable iff with cond implication stmt, fileline:%d", $time, 44);
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:41:41: Unsupported: Implication with sequence expression
+                                                    : ... note: In instance 't'
+   41 |   assert property (@(posedge clk) ##1 1 |-> 0) $display("[%0t] disable iff with cond implication stmt, fileline:%d", $time, 41);
      |                                         ^~~
-%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:46:45: Unsupported: Implication with sequence expression
-   46 |   assert property (@(posedge clk) (##1 val) |-> (##1 val)) $display("[%0t] two delays implication stmt, fileline:%d", $time, 46);
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:43:45: Unsupported: Implication with sequence expression
+                                                    : ... note: In instance 't'
+   43 |   assert property (@(posedge clk) (##1 val) |-> (##1 val)) $display("[%0t] two delays implication stmt, fileline:%d", $time, 43);
      |                                             ^~~
-%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:48:52: Unsupported: Disable iff with sequence expression
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:45:52: Unsupported: Disable iff with sequence expression
                                                    : ... note: In instance 't'
-   48 |   assert property (@(posedge clk) disable iff (cyc != 5) ##1 0) $display("[%0t] disable iff stmt, fileline:%d", $time, 48);
+   45 |   assert property (@(posedge clk) disable iff (cyc != 5) ##1 0) $display("[%0t] disable iff stmt, fileline:%d", $time, 45);
      |                                                    ^~
-%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:50:52: Unsupported: Disable iff with sequence expression
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:47:52: Unsupported: Disable iff with sequence expression
                                                    : ... note: In instance 't'
-   50 |   assume property (@(posedge clk) disable iff (cyc != 5) ##1 0) $display("[%0t] disable iff stmt, fileline:%d", $time, 50);
+   47 |   assume property (@(posedge clk) disable iff (cyc != 5) ##1 0) $display("[%0t] disable iff stmt, fileline:%d", $time, 47);
      |                                                    ^~
-%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:52:51: Unsupported: Disable iff with sequence expression
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:49:51: Unsupported: Disable iff with sequence expression
                                                    : ... note: In instance 't'
-   52 |   cover property (@(posedge clk) disable iff (cyc != 5) ##1 0) $display("[%0t] disable iff stmt, fileline:%d", $time, 52);
+   49 |   cover property (@(posedge clk) disable iff (cyc != 5) ##1 0) $display("[%0t] disable iff stmt, fileline:%d", $time, 49);
      |                                                   ^~
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:52:37: Unsupported: Disable iff with sequence expression
+                                                    : ... note: In instance 't'
+   52 |     @(posedge clk) disable iff (cyc != 5) ##1 0;
+      |                                     ^~
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:56:18: Unsupported: Implication with sequence expression
+                                                    : ... note: In instance 't'
+   56 |     ##1 cyc == 4 |-> 1;
+      |                  ^~~
 %Error: Exiting due to
--- a/test_regress/t/t_property_sexpr_unsup.v
+++ b/test_regress/t/t_property_sexpr_unsup.v
@ -25,10 +25,7 @@ module t (  /*AUTOARG*/
      end
    end
  end
-`ifdef PARSING_TIME
-  assert property (@(posedge clk) val ##1 val) $display("[%0t] var with single delay stmt, fileline:%d", $time, `__LINE__);
-  assert property (@(posedge clk) ##1 val ##2 val) $display("[%0t] sequence stmt, fileline:%d", $time, `__LINE__);
-`else
+
  assert property (@(posedge clk) ##1 1 |-> 1) $display("[%0t] single delay with const implication stmt, fileline:%d", $time, `__LINE__);

  assert property (@(posedge clk) ##1 1 |-> not (val)) $display("[%0t] single delay implication with negated var stmt, fileline:%d", $time, `__LINE__);
@ -50,7 +47,14 @@ module t (  /*AUTOARG*/
  assume property (@(posedge clk) disable iff (cyc != 5) ##1 0) $display("[%0t] disable iff stmt, fileline:%d", $time, `__LINE__);

  cover property (@(posedge clk) disable iff (cyc != 5) ##1 0) $display("[%0t] disable iff stmt, fileline:%d", $time, `__LINE__);
-`endif
+
+  property prop_disableiff;
+    @(posedge clk) disable iff (cyc != 5) ##1 0;
+  endproperty
+
+  property prop_implication;
+    ##1 cyc == 4 |-> 1;
+  endproperty
 endmodule

 // Test parsing only
--- a/test_regress/t/t_sequence_sexpr_unsup.out
+++ b/test_regress/t/t_sequence_sexpr_unsup.out
@ -66,152 +66,131 @@
   68 |       ## [+] b;
      |       ^~
 %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:71:4: Unsupported: sequence
-   71 |    sequence s_cycdelay_int;
+   71 |    sequence s_cycdelay_id;
      |    ^~~~~~~~
-%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:72:9: Unsupported: ## (in sequence expression)
-   72 |       a ## 1 b;
+%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:72:9: Unsupported: ## id cycle delay range expression
+   72 |       a ## DELAY b;
      |         ^~
 %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:74:4: Unsupported: sequence
-   74 |    sequence s_cycdelay_id;
+   74 |    sequence s_cycdelay_pid;
      |    ^~~~~~~~
-%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:75:9: Unsupported: ## id cycle delay range expression
-   75 |       a ## DELAY b;
-      |         ^~
-%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:75:9: Unsupported: ## (in sequence expression)
-   75 |       a ## DELAY b;
+%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:75:9: Unsupported: ## () cycle delay range expression
+   75 |       a ## ( DELAY ) b;
      |         ^~
 %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:77:4: Unsupported: sequence
-   77 |    sequence s_cycdelay_pid;
+   77 |    sequence s_cycdelay_range;
      |    ^~~~~~~~
-%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:78:9: Unsupported: ## () cycle delay range expression
-   78 |       a ## ( DELAY ) b;
-      |         ^~
-%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:78:9: Unsupported: ## (in sequence expression)
-   78 |       a ## ( DELAY ) b;
+%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:78:9: Unsupported: ## range cycle delay range expression
+   78 |       a ## [1:2] b;
      |         ^~
 %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:80:4: Unsupported: sequence
-   80 |    sequence s_cycdelay_range;
+   80 |    sequence s_cycdelay_star;
      |    ^~~~~~~~
-%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:81:9: Unsupported: ## range cycle delay range expression
-   81 |       a ## [1:2] b;
-      |         ^~
-%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:81:9: Unsupported: ## (in sequence expression)
-   81 |       a ## [1:2] b;
+%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:81:9: Unsupported: ## [*] cycle delay range expression
+   81 |       a ## [*] b;
      |         ^~
 %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:83:4: Unsupported: sequence
-   83 |    sequence s_cycdelay_star;
+   83 |    sequence s_cycdelay_plus;
      |    ^~~~~~~~
-%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:84:9: Unsupported: ## [*] cycle delay range expression
-   84 |       a ## [*] b;
+%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:84:9: Unsupported: ## [+] cycle delay range expression
+   84 |       a ## [+] b;
      |         ^~
-%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:84:9: Unsupported: ## (in sequence expression)
-   84 |       a ## [*] b;
-      |         ^~
-%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:86:4: Unsupported: sequence
-   86 |    sequence s_cycdelay_plus;
+%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:87:4: Unsupported: sequence
+   87 |    sequence s_booleanabbrev_brastar_int;
      |    ^~~~~~~~
-%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:87:9: Unsupported: ## [+] cycle delay range expression
-   87 |       a ## [+] b;
-      |         ^~
-%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:87:9: Unsupported: ## (in sequence expression)
-   87 |       a ## [+] b;
+%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:88:9: Unsupported: [*] boolean abbrev expression
+   88 |       a [* 1 ];
      |         ^~
+%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:88:12: Unsupported: boolean abbrev (in sequence expression)
+   88 |       a [* 1 ];
+      |            ^
 %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:90:4: Unsupported: sequence
-   90 |    sequence s_booleanabbrev_brastar_int;
+   90 |    sequence s_booleanabbrev_brastar;
      |    ^~~~~~~~
 %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:91:9: Unsupported: [*] boolean abbrev expression
-   91 |       a [* 1 ];
+   91 |       a [*];
+      |         ^~
+%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:91:9: Unsupported: boolean abbrev (in sequence expression)
+   91 |       a [*];
      |         ^~
-%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:91:12: Unsupported: boolean abbrev (in sequence expression)
-   91 |       a [* 1 ];
-      |            ^
 %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:93:4: Unsupported: sequence
-   93 |    sequence s_booleanabbrev_brastar;
+   93 |    sequence s_booleanabbrev_plus;
      |    ^~~~~~~~
-%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:94:9: Unsupported: [*] boolean abbrev expression
-   94 |       a [*];
-      |         ^~
+%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:94:9: Unsupported: [+] boolean abbrev expression
+   94 |       a [+];
+      |         ^~~
 %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:94:9: Unsupported: boolean abbrev (in sequence expression)
-   94 |       a [*];
-      |         ^~
+   94 |       a [+];
+      |         ^~~
 %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:96:4: Unsupported: sequence
-   96 |    sequence s_booleanabbrev_plus;
+   96 |    sequence s_booleanabbrev_eq;
      |    ^~~~~~~~
-%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:97:9: Unsupported: [+] boolean abbrev expression
-   97 |       a [+];
-      |         ^~~
-%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:97:9: Unsupported: boolean abbrev (in sequence expression)
-   97 |       a [+];
-      |         ^~~
+%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:97:9: Unsupported: [= boolean abbrev expression
+   97 |       a [= 1];
+      |         ^~
+%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:97:12: Unsupported: boolean abbrev (in sequence expression)
+   97 |       a [= 1];
+      |            ^
 %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:99:4: Unsupported: sequence
-   99 |    sequence s_booleanabbrev_eq;
+   99 |    sequence s_booleanabbrev_eq_range;
      |    ^~~~~~~~
 %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:100:9: Unsupported: [= boolean abbrev expression
-  100 |       a [= 1];
+  100 |       a [= 1:2];
      |         ^~
 %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:100:12: Unsupported: boolean abbrev (in sequence expression)
-  100 |       a [= 1];
+  100 |       a [= 1:2];
      |            ^
 %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:102:4: Unsupported: sequence
-  102 |    sequence s_booleanabbrev_eq_range;
+  102 |    sequence s_booleanabbrev_minusgt;
      |    ^~~~~~~~
-%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:103:9: Unsupported: [= boolean abbrev expression
-  103 |       a [= 1:2];
-      |         ^~
-%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:103:12: Unsupported: boolean abbrev (in sequence expression)
-  103 |       a [= 1:2];
-      |            ^
+%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:103:9: Unsupported: [-> boolean abbrev expression
+  103 |       a [-> 1];
+      |         ^~~
+%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:103:13: Unsupported: boolean abbrev (in sequence expression)
+  103 |       a [-> 1];
+      |             ^
 %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:105:4: Unsupported: sequence
-  105 |    sequence s_booleanabbrev_minusgt;
+  105 |    sequence s_booleanabbrev_minusgt_range;
      |    ^~~~~~~~
 %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:106:9: Unsupported: [-> boolean abbrev expression
-  106 |       a [-> 1];
+  106 |       a [-> 1:2];
      |         ^~~
 %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:106:13: Unsupported: boolean abbrev (in sequence expression)
-  106 |       a [-> 1];
+  106 |       a [-> 1:2];
      |             ^
-%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:108:4: Unsupported: sequence
-  108 |    sequence s_booleanabbrev_minusgt_range;
+%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:109:4: Unsupported: sequence
+  109 |    sequence p_arg_seqence(sequence inseq);
      |    ^~~~~~~~
-%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:109:9: Unsupported: [-> boolean abbrev expression
-  109 |       a [-> 1:2];
-      |         ^~~
-%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:109:13: Unsupported: boolean abbrev (in sequence expression)
-  109 |       a [-> 1:2];
-      |             ^
-%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:112:4: Unsupported: sequence
-  112 |    sequence p_arg_seqence(sequence inseq);
-      |    ^~~~~~~~
-%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:112:27: Unsupported: sequence argument data type
-  112 |    sequence p_arg_seqence(sequence inseq);
+%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:109:27: Unsupported: sequence argument data type
+  109 |    sequence p_arg_seqence(sequence inseq);
      |                           ^~~~~~~~
+%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:113:4: Unsupported: sequence
+  113 |    sequence s_firstmatch_a;
+      |    ^~~~~~~~
+%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:114:7: Unsupported: first_match (in sequence expression)
+  114 |       first_match (a);
+      |       ^~~~~~~~~~~
 %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:116:4: Unsupported: sequence
-  116 |    sequence s_firstmatch_a;
+  116 |    sequence s_firstmatch_ab;
      |    ^~~~~~~~
 %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:117:7: Unsupported: first_match (in sequence expression)
-  117 |       first_match (a);
+  117 |       first_match (a, res0 = 1);
      |       ^~~~~~~~~~~
 %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:119:4: Unsupported: sequence
-  119 |    sequence s_firstmatch_ab;
+  119 |    sequence s_firstmatch_abc;
      |    ^~~~~~~~
 %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:120:7: Unsupported: first_match (in sequence expression)
-  120 |       first_match (a, res0 = 1);
+  120 |       first_match (a, res0 = 1, res1 = 2);
      |       ^~~~~~~~~~~
-%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:122:4: Unsupported: sequence
-  122 |    sequence s_firstmatch_abc;
-      |    ^~~~~~~~
-%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:123:7: Unsupported: first_match (in sequence expression)
-  123 |       first_match (a, res0 = 1, res1 = 2);
-      |       ^~~~~~~~~~~
-%Warning-COVERIGN: t/t_sequence_sexpr_unsup.v:126:10: Ignoring unsupported: cover sequence
-  126 |    cover sequence (s_a) $display("");
+%Warning-COVERIGN: t/t_sequence_sexpr_unsup.v:123:10: Ignoring unsupported: cover sequence
+  123 |    cover sequence (s_a) $display("");
      |          ^~~~~~~~
                   ... For warning description see https://verilator.org/warn/COVERIGN?v=latest
                   ... Use "/* verilator lint_off COVERIGN */" and lint_on around source to disable this message.
-%Warning-COVERIGN: t/t_sequence_sexpr_unsup.v:127:10: Ignoring unsupported: cover sequence
-  127 |    cover sequence (@(posedge a) disable iff (b) s_a) $display("");
+%Warning-COVERIGN: t/t_sequence_sexpr_unsup.v:124:10: Ignoring unsupported: cover sequence
+  124 |    cover sequence (@(posedge a) disable iff (b) s_a) $display("");
      |          ^~~~~~~~
-%Warning-COVERIGN: t/t_sequence_sexpr_unsup.v:128:10: Ignoring unsupported: cover sequence
-  128 |    cover sequence (disable iff (b) s_a) $display("");
+%Warning-COVERIGN: t/t_sequence_sexpr_unsup.v:125:10: Ignoring unsupported: cover sequence
+  125 |    cover sequence (disable iff (b) s_a) $display("");
      |          ^~~~~~~~
 %Error: Exiting due to
--- a/test_regress/t/t_sequence_sexpr_unsup.v
+++ b/test_regress/t/t_sequence_sexpr_unsup.v
@ -68,9 +68,6 @@ module t (/*AUTOARG*/
      ## [+] b;
   endsequence

-   sequence s_cycdelay_int;
-      a ## 1 b;
-   endsequence
   sequence s_cycdelay_id;
      a ## DELAY b;
   endsequence
Author	SHA1	Message	Date
Bartłomiej Chmiel	dcdc6e087d	Merge `f6228d00d8` into `100c831474`	2025-11-06 07:10:55 -05:00
Bartłomiej Chmiel	f6228d00d8	Remove block names Signed-off-by: Bartłomiej Chmiel <bchmiel@antmicro.com>	2025-11-06 13:09:02 +01:00
Bartłomiej Chmiel	82fbb446ed	Improve coverage Signed-off-by: Bartłomiej Chmiel <bchmiel@antmicro.com>	2025-11-06 12:38:47 +01:00
Bartłomiej Chmiel	4815ef662c	Fixup Signed-off-by: Bartłomiej Chmiel <bchmiel@antmicro.com>	2025-11-06 11:54:52 +01:00
Bartłomiej Chmiel	4b31bdb08c	Simplify processVtx Signed-off-by: Bartłomiej Chmiel <bchmiel@antmicro.com>	2025-11-06 11:51:46 +01:00
Bartłomiej Chmiel	129a88fc70	V3AssertProp Commentary Signed-off-by: Bartłomiej Chmiel <bchmiel@antmicro.com>	2025-11-06 11:36:56 +01:00
Bartłomiej Chmiel	459333d835	Fix emitv Signed-off-by: Bartłomiej Chmiel <bchmiel@antmicro.com>	2025-11-06 10:55:17 +01:00
Bartłomiej Chmiel	129ccb44ae	Pass graph by reference Signed-off-by: Bartłomiej Chmiel <bchmiel@antmicro.com>	2025-11-06 10:54:05 +01:00
Bartłomiej Chmiel	b0d5c85c06	Dump graph test Signed-off-by: Bartłomiej Chmiel <bchmiel@antmicro.com>	2025-11-06 10:48:19 +01:00
Bartłomiej Chmiel	3104f89665	Handle unexpected not in sequence Signed-off-by: Bartłomiej Chmiel <bchmiel@antmicro.com>	2025-11-06 10:41:30 +01:00
Bartłomiej Chmiel	4719eb9739	Renames, remove lambda Signed-off-by: Bartłomiej Chmiel <bchmiel@antmicro.com>	2025-11-06 10:19:49 +01:00
Bartłomiej Chmiel	1528a02395	Missing VL_DO_DANGLING Signed-off-by: Bartłomiej Chmiel <bchmiel@antmicro.com>	2025-11-06 10:13:58 +01:00
Bartłomiej Chmiel	4ea29d7069	Handling unexpected vertex Signed-off-by: Bartłomiej Chmiel <bchmiel@antmicro.com>	2025-11-06 10:12:23 +01:00
Bartłomiej Chmiel	d9654fa2c6	Simplify pexpr clause delete Signed-off-by: Bartłomiej Chmiel <bchmiel@antmicro.com>	2025-11-06 10:08:36 +01:00
Bartłomiej Chmiel	6789cbb3bd	VL_RESTORER for m_inSampled Signed-off-by: Bartłomiej Chmiel <bchmiel@antmicro.com>	2025-11-06 10:07:00 +01:00
Bartłomiej Chmiel	29749b0c42	Remove __Vassert check Signed-off-by: Bartłomiej Chmiel <bchmiel@antmicro.com>	2025-11-06 10:05:31 +01:00
Bartłomiej Chmiel	fad3bdcd7e	Move unsup checks to V3Width, handle standalone properties Signed-off-by: Bartłomiej Chmiel <bchmiel@antmicro.com>	2025-11-06 10:03:26 +01:00
Bartłomiej Chmiel	b2b65472ad	Renames and review fixes Signed-off-by: Bartłomiej Chmiel <bchmiel@antmicro.com>	2025-11-05 14:43:02 +01:00
Bartłomiej Chmiel	37f0bd87d3	Apply autofix suggestions from code review Co-authored-by: Wilson Snyder <wsnyder@wsnyder.org>	2025-11-05 08:25:10 -05:00
Bartłomiej Chmiel	61a1dd9531	Implement multi-expression inline sequences Signed-off-by: Bartłomiej Chmiel <bchmiel@antmicro.com>	2025-11-04 16:53:00 +01:00