Remove block names

Signed-off-by: Bartłomiej Chmiel <bchmiel@antmicro.com>

src/V3Assert.cpp

@@ -294,9 +294,10 @@ class AssertVisitor final : public VNVisitor {
     AstNode* assertBody(AstNodeCoverOrAssert* nodep, AstNode* propp, AstNode* passsp,
                         AstNode* failsp) {
         AstNode* bodyp = nullptr;
-        if (VString::startsWith(propp->name(), "__Vassert")) {
+        if (AstPExpr* const pexprp = VN_CAST(propp, PExpr)) {
             AstFork* const forkp = new AstFork{nodep->fileline(), VJoinType::JOIN_NONE};
-            forkp->addForksp(new AstBegin{nodep->fileline(), "", propp, true});
+            forkp->addForksp(pexprp->bodyp()->unlinkFrBack());
+            VL_DO_DANGLING(pushDeletep(pexprp), pexprp);
             bodyp = forkp;
         } else {
             bodyp = assertCond(nodep, VN_AS(propp, NodeExpr), passsp, failsp);
@@ -658,23 +659,21 @@ class AssertVisitor final : public VNVisitor {
             if (nodep->pass() && m_passsp) {
                 // Cover adds COVERINC by AstNode::addNext, thus need to clone next too.
                 nodep->replaceWith(m_passsp->cloneTree(true));
-                VL_DO_DANGLING(pushDeletep(nodep), nodep);
             } 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));
-                VL_DO_DANGLING(pushDeletep(nodep), nodep);
             } else {
-                VL_DO_DANGLING(pushDeletep(nodep->unlinkFrBack()), nodep);
+                nodep->unlinkFrBack();
             }
+            VL_DO_DANGLING(pushDeletep(nodep), nodep);
         }
     }
     void visit(AstPExpr* nodep) override {
-        m_inSampled = false;
         if (m_underAssert) {
+            VL_RESTORER(m_inSampled);
+            m_inSampled = false;
             iterateChildren(nodep);
-            nodep->replaceWith(nodep->bodyp()->unlinkFrBack());
-            VL_DO_DANGLING(pushDeletep(nodep), nodep);
         } else if (m_inRestrict) {
             VL_DO_DANGLING(pushDeletep(nodep->unlinkFrBack()), nodep);
         }

src/V3AssertPre.cpp

@@ -60,8 +60,6 @@ private:
     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
-    bool m_hasPExpr = false;  // True if assert has AstPExpr inside
     bool m_inPExpr = false;  // True if in AstPExpr
 
     // METHODS
@@ -471,24 +469,11 @@ private:
     void visit(AstNodeCoverOrAssert* nodep) override {
         if (nodep->sentreep()) return;  // Already processed
 
-        VL_RESTORER(m_hasPExpr);
-        VL_RESTORER(m_hasUnsupp);
-
         clearAssertInfo();
 
         // Find Clocking's buried under nodep->exprsp
         iterateChildren(nodep);
         if (!nodep->immediate()) nodep->sentreep(newSenTree(nodep));
-        if (m_hasPExpr && 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");
-            }
-            VL_DO_DANGLING(nodep->unlinkFrBack()->deleteTree(), nodep);
-        }
         clearAssertInfo();
     }
     void visit(AstFalling* nodep) override {
@@ -592,7 +577,6 @@ private:
 
     void visit(AstImplication* nodep) override {
         if (nodep->sentreep()) return;  // Already processed
-        m_hasUnsupp = nodep;
 
         iterateChildren(nodep);
 
@@ -644,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()},
@@ -661,7 +644,6 @@ private:
     void visit(AstPExpr* nodep) override {
         VL_RESTORER(m_inPExpr);
         m_inPExpr = true;
-        m_hasPExpr = true;
 
         if (AstLogNot* const notp = VN_CAST(nodep->backp(), LogNot)) {
             notp->replaceWith(nodep->unlinkFrBack());

src/V3AssertProp.cpp

@@ -13,15 +13,23 @@
 // 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.
-//          Property decision tree is a tree rooted with source sequence
-//          expression. It has a bipartite structure
-//          (Expr -> Stmt -> Expr ...). Sequence states are represented
-//          as a deterministic finite automaton (DFA).
-//      Transform property decision tree into AST, remove source sequence
-//      expression
-//          Each property is wrapped with AstPExpr that is transformed
+//      Transform property decision tree into AST, remove source sequence expression
+//          Property blocks are wrapped with AstPExpr that are transformed
 //          further by V3AssertPre and V3Assert.
 //
 //*************************************************************************
@@ -31,7 +39,6 @@
 #include "V3AssertProp.h"
 
 #include "V3Graph.h"
-#include "V3UniqueNames.h"
 
 VL_DEFINE_DEBUG_FUNCTIONS;
 
@@ -48,7 +55,6 @@ public:
     explicit DfaVertex(V3Graph* graphp, AstNode* nodep) VL_MT_DISABLED : V3GraphVertex{graphp},
                                                                          m_nodep{nodep} {}
     AstNode* nodep() const { return m_nodep; }
-    // LCOV_EXCL_START // Debug code
     string name() const override VL_MT_STABLE {
         return cvtToHex(m_nodep) + "\\n " + cvtToStr(m_nodep->typeName()) + "\\n"s
                + m_nodep->fileline()->ascii();
@@ -58,7 +64,6 @@ public:
         if (outEmpty()) return "doubleoctagon";
         return "oval";
     }
-    // LCOV_EXCL_STOP
     bool isStart() const { return inEmpty(); }
 };
 
@@ -68,9 +73,7 @@ public:
     // CONSTRUCTORS
     explicit DfaStmtVertex(V3Graph* graphp, AstNodeStmt* stmtp) VL_MT_DISABLED
         : DfaVertex{graphp, stmtp} {}
-    // LCOV_EXCL_START // Debug code
     string dotColor() const override { return "green"; }
-    // LCOV_EXCL_STOP
 };
 
 class DfaExprVertex final : public DfaVertex {
@@ -79,9 +82,7 @@ public:
     // CONSTRUCTORS
     explicit DfaExprVertex(V3Graph* graphp, AstNodeExpr* exprp) VL_MT_DISABLED
         : DfaVertex{graphp, exprp} {}
-    // LCOV_EXCL_START // Debug code
     string dotColor() const override { return "blue"; }
-    // LCOV_EXCL_STOP
 };
 
 class DfaConditionEdge final : public V3GraphEdge {
@@ -97,19 +98,23 @@ public:
     ~DfaConditionEdge() override = default;
 
     bool ifBranch() const { return m_ifBranch; }
-    // LCOV_EXCL_START // Debug code
     string dotColor() const override { return m_ifBranch ? "green" : "red"; }
-    // LCOV_EXCL_STOP
 };
 
 // Parse properties and ensemble a property tree graph
 class AssertPropBuildVisitor final : public VNVisitorConst {
     // STATE
-    std::unique_ptr<V3Graph> m_graphp = std::make_unique<V3Graph>();  // Property tree
-    DfaVertex* m_lastp = nullptr;  // Last encountered vertex
+    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 {
@@ -118,11 +123,6 @@ class AssertPropBuildVisitor final : public VNVisitorConst {
         iterateChildrenConst(nodep);
     }
     void visit(AstSExpr* nodep) override {
-        const auto makeClause = [this, nodep](bool pass) {
-            return new DfaStmtVertex{
-                m_graphp.get(),
-                new AstPExprClause{nodep->fileline(), m_underLogNots % 2 == 0 ? pass : !pass}};
-        };
 
         if (VN_IS(nodep->exprp(), SExpr)) {
             VL_RESTORER(m_underSExpr);
@@ -130,46 +130,46 @@ class AssertPropBuildVisitor final : public VNVisitorConst {
             iterateConst(nodep->exprp());
         } else {
             DfaExprVertex* const exprVtxp
-                = new DfaExprVertex{m_graphp.get(), nodep->exprp()->unlinkFrBack()};
-            new DfaConditionEdge{m_graphp.get(), exprVtxp, makeClause(true), true};
-            new DfaConditionEdge{m_graphp.get(), exprVtxp, makeClause(false), false};
-            m_lastp = 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 startp
-            = m_underSExpr ? nullptr : new DfaExprVertex{m_graphp.get(), nodep};
+        DfaExprVertex* const startVtxp
+            = m_underSExpr ? nullptr : new DfaExprVertex{&m_graph, nodep};
 
         DfaStmtVertex* const dlyVtxp
-            = new DfaStmtVertex{m_graphp.get(), nodep->delayp()->unlinkFrBack()};
+            = 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_graphp.get(), sexprp->delayp()->unlinkFrBack()};
+                = new DfaStmtVertex{&m_graph, sexprp->delayp()->unlinkFrBack()};
             DfaExprVertex* const exprVtxp
-                = new DfaExprVertex{m_graphp.get(), sexprp->exprp()->unlinkFrBack()};
+                = new DfaExprVertex{&m_graph, sexprp->exprp()->unlinkFrBack()};
 
-            if (startp) new DfaConditionEdge{m_graphp.get(), startp, sdlyVtxp, true};
-            new DfaConditionEdge{m_graphp.get(), sdlyVtxp, exprVtxp, true};
-            new DfaConditionEdge{m_graphp.get(), exprVtxp, dlyVtxp, true};
-            new DfaConditionEdge{m_graphp.get(), dlyVtxp, m_lastp, true};
-            new DfaConditionEdge{m_graphp.get(), exprVtxp, makeClause(false), false};
+            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_graphp.get(), nodep->preExprp()->unlinkFrBack()};
-            if (startp) new DfaConditionEdge{m_graphp.get(), startp, preVtxp, true};
-            new DfaConditionEdge{m_graphp.get(), preVtxp, dlyVtxp, true};
-            new DfaConditionEdge{m_graphp.get(), dlyVtxp, m_lastp, true};
-            new DfaConditionEdge{m_graphp.get(), preVtxp, makeClause(false), false};
-            m_lastp = 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 (startp) new DfaConditionEdge{m_graphp.get(), startp, dlyVtxp, true};
-            new DfaConditionEdge{m_graphp.get(), dlyVtxp, m_lastp, true};
-            m_lastp = dlyVtxp;
+            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); }
@@ -177,19 +177,18 @@ class AssertPropBuildVisitor final : public VNVisitorConst {
 
 public:
     // CONSTRUCTORS
-    explicit AssertPropBuildVisitor(AstNetlist* nodep) {
+    explicit AssertPropBuildVisitor(AstNetlist* nodep, V3Graph& graph)
+        : m_graph{graph} {
         iterateConst(nodep);
-        if (dumpGraphLevel() >= 6) m_graphp->dumpDotFilePrefixedAlways("properties", true);
+        if (dumpGraphLevel() >= 6) m_graph.dumpDotFilePrefixedAlways("properties", true);
     }
-    std::unique_ptr<V3Graph> graphp() { return std::move(m_graphp); }
     ~AssertPropBuildVisitor() override = default;
 };
 
 // Transform property graph into AST
 class AssertPropTransformer final {
     // STATE
-    V3UniqueNames m_assertCycleDelayNames{"__Vassert"};  // Names for assertion properties
-    const std::unique_ptr<V3Graph> m_graph;  // Property tree
+    V3Graph& m_graph;  // Property tree
     AstPExpr* m_pexprp = nullptr;  // Currently built property sequence
     AstBegin* m_current = nullptr;  // Currently built block
 
@@ -197,11 +196,8 @@ class AssertPropTransformer final {
         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
-        // LCOV_EXCL_START
-        assert(0);
-        VL_UNREACHABLE;
+        v3fatalSrc("Unexpected vertex type");
         return nullptr;
-        // LCOV_EXCL_STOP
     }
     V3GraphVertex* processVtx(DfaStmtVertex* vtxp) {
         UASSERT_OBJ(!vtxp->isStart(), vtxp->nodep(),
@@ -213,25 +209,15 @@ class AssertPropTransformer final {
     V3GraphVertex* processVtx(DfaExprVertex* vtxp) {
         AstNode* const nodep = vtxp->nodep();
         if (vtxp->isStart()) {
-            AstBegin* const bodyp = new AstBegin{
-                nodep->fileline(), m_assertCycleDelayNames.get(nodep) + "__block", nullptr, true};
+            AstBegin* const bodyp = new AstBegin{nodep->fileline(), "", nullptr, true};
             m_pexprp = new AstPExpr{nodep->fileline(), bodyp, nodep->dtypep()};
-            UASSERT_OBJ(vtxp->outSize1() && vtxp->outEdges().frontp()->is<DfaConditionEdge>(),
-                        nodep, "Incorrect property graph");
+            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() > 0 && vtxp->outEdges().size() <= 2, nodep,
-                    "Incorrect edges");
-        AstBegin* const passsp = new AstBegin{
-            nodep->fileline(), m_assertCycleDelayNames.get(nodep) + "__block_pass", nullptr, true};
-        AstNode* const failsp = [vtxp]() -> AstNode* {
-            if (!vtxp->outSize1()) {
-                V3GraphVertex* const failVtxp = vtxp->outEdges().backp()->top();
-                return failVtxp->as<DfaStmtVertex>()->nodep();
-            }
-            return nullptr;
-        }();
+        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)};
@@ -248,16 +234,16 @@ class AssertPropTransformer final {
 
 public:
     // CONSTRUCTORS
-    explicit AssertPropTransformer(std::unique_ptr<V3Graph> graph)
-        : m_graph{std::move(graph)} {
-        for (V3GraphVertex& vtx : m_graph->vertices()) {
+    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);
-                    propp->deleteTree();
+                    VL_DO_DANGLING(propp->deleteTree(), propp);
                 }
             }
         }
@@ -270,8 +256,9 @@ public:
 void V3AssertProp::assertPropAll(AstNetlist* nodep) {
     UINFO(2, __FUNCTION__ << ":");
     {
-        std::unique_ptr<V3Graph> graphp = AssertPropBuildVisitor{nodep}.graphp();
-        AssertPropTransformer{std::move(graphp)};
+        V3Graph graph;
+        { AssertPropBuildVisitor{nodep, graph}; }
+        AssertPropTransformer{graph};
     }
     V3Global::dumpCheckGlobalTree("assertproperties", 0, dumpTreeEitherLevel() >= 3);
 }

src/V3Width.cpp

@@ -216,6 +216,8 @@ class WidthVisitor final : public VNVisitor {
     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
@@ -1540,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);
@@ -1560,6 +1563,7 @@ class WidthVisitor final : public VNVisitor {
     void visit(AstSExpr* nodep) override {
         VL_RESTORER(m_underSExpr);
         m_underSExpr = true;
+        m_hasSExpr = true;
         if (m_vup->prelim()) {
             if (nodep->preExprp()) {
                 iterateCheckBool(nodep, "preExprp", nodep->preExprp(), BOTH);
@@ -5344,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);
@@ -5352,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);
+                }
+            }
         }
     }
 

src/verilog.y

@@ -6623,11 +6623,7 @@ sexpr<nodeExprp>:  // ==IEEE: sequence_expr  (The name sexpr is important as reg
         //                      // IEEE: "sequence_expr cycle_delay_range sequence_expr { cycle_delay_range sequence_expr }"
         //                      // Both rules basically mean we can repeat sequences, so make it simpler:
                 cycle_delay_range ~p~sexpr  %prec yP_POUNDPOUND
-                        { $$ = new AstSExpr{$<fl>1, $1, $2};
-                            if (VN_IS($2, LogNot)) {
-                                BBUNSUP($2->fileline(), "Unexpected not in sequence expression context");
-                            }
-                        }
+                        { $$ = new AstSExpr{$<fl>1, $1, $2}; }
         |       ~p~sexpr cycle_delay_range sexpr %prec prPOUNDPOUND_MULTI
                         { $$ = new AstSExpr{$<fl>2, $1, $2, $3}; }
         //

test_regress/t/t_debug_emitv.out

@@ -366,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

test_regress/t/t_debug_emitv.v

@@ -277,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);
 

test_regress/t/t_property_sexpr_bad.out

@@ -1,5 +1,6 @@
-%Error-UNSUPPORTED: t/t_property_sexpr_bad.v:20:39: Unexpected not in sequence expression context
+%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);
       |                                       ^~~
-                    ... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest
+        ... See the manual at https://verilator.org/verilator_doc.html?v=latest for more assistance.
 %Error: Exiting due to

test_regress/t/t_property_sexpr_multi.py

@@ -11,7 +11,7 @@ import vltest_bootstrap
 
 test.scenarios('simulator')
 
-test.compile(timing_loop=True, verilator_flags2=['--assert', '--timing'])
+test.compile(timing_loop=True, verilator_flags2=['--assert', '--timing', '--dumpi-V3AssertProp 6'])
 
 test.execute()
 

test_regress/t/t_property_sexpr_parse_unsup.out

@@ -1,23 +1,23 @@
-%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:67:14: Unsupported: sequence match items
-   67 |     ($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];
       |              ^
                     ... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest
-%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:67:29: Unsupported: ## range cycle delay range expression
-   67 |     ($rose(a), l_b = b) |-> ##[3:10] q[l_b];
+%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:66:13: Unsupported: property variable declaration
-   66 |     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:84:16: Unsupported: sequence match items
-   84 |     (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:84:51: Unsupported: [-> boolean abbrev expression
-   84 |     (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:84:54: Unsupported: boolean abbrev (in sequence expression)
-   84 |     (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:82:14: Unsupported: property variable declaration
-   82 |     realtime l_t;
+%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:90:14: Unsupported: property variable declaration
+   90 |     realtime l_t;
       |              ^~~
 %Error: Exiting due to

test_regress/t/t_property_sexpr_unsup.out

@@ -1,23 +1,30 @@
 %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: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: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: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: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: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: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:45:52: Unsupported: Disable iff with sequence expression
@@ -32,4 +39,12 @@
                                                     : ... note: In instance 't'
    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

test_regress/t/t_property_sexpr_unsup.v

@@ -47,6 +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__);
+
+  property prop_disableiff;
+    @(posedge clk) disable iff (cyc != 5) ##1 0;
+  endproperty
+
+  property prop_implication;
+    ##1 cyc == 4 |-> 1;
+  endproperty
 endmodule
 
 // Test parsing only