Renames and review fixes

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

src/CMakeLists.txt

@@ -43,7 +43,7 @@ set(HEADERS
     V3ActiveTop.h
     V3Assert.h
     V3AssertPre.h
-    V3AssertProperties.h
+    V3AssertProp.h
     V3Ast.h
     V3AstAttr.h
     V3AstInlines.h
@@ -208,7 +208,7 @@ set(COMMON_SOURCES
     V3ActiveTop.cpp
     V3Assert.cpp
     V3AssertPre.cpp
-    V3AssertProperties.cpp
+    V3AssertProp.cpp
     V3Ast.cpp
     V3AstNodes.cpp
     V3Begin.cpp

src/Makefile_obj.in

@@ -232,7 +232,7 @@ RAW_OBJS_PCH_ASTNOMT = \
   V3ActiveTop.o \
   V3Assert.o \
   V3AssertPre.o \
-  V3AssertProperties.o \
+  V3AssertProp.o \
   V3Begin.o \
   V3Branch.o \
   V3CCtors.o \

src/V3Assert.cpp

@@ -655,11 +655,11 @@ class AssertVisitor final : public VNVisitor {
     }
     void visit(AstPExprClause* nodep) override {
         if (m_underAssert) {
-            if (nodep->passs() && m_passsp) {
+            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->passs() && m_failsp) {
+            } 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));

src/V3AssertProp.cpp

@@ -1,6 +1,6 @@
 // -*- mode: C++; c-file-style: "cc-mode" -*-
 //*************************************************************************
-// DESCRIPTION: Verilator: Transform sequences into properties
+// DESCRIPTION: Verilator: Implementation of assertion properties
 //
 // Code available from: https://verilator.org
 //
@@ -17,7 +17,8 @@
 //      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 ...).
+//          (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
@@ -27,15 +28,13 @@
 
 #include "V3PchAstNoMT.h"  // VL_MT_DISABLED_CODE_UNIT
 
-#include "V3AssertProperties.h"
+#include "V3AssertProp.h"
 
 #include "V3Graph.h"
 #include "V3UniqueNames.h"
 
 VL_DEFINE_DEBUG_FUNCTIONS;
 
-namespace {
-
 //######################################################################
 // Data structures (graph types)
 
@@ -63,39 +62,39 @@ public:
     bool isStart() const { return inEmpty(); }
 };
 
-class StmtVertex final : public DfaVertex {
-    VL_RTTI_IMPL(StmtVertex, V3GraphEdge)
+class DfaStmtVertex final : public DfaVertex {
+    VL_RTTI_IMPL(DfaStmtVertex, V3GraphEdge)
 public:
     // CONSTRUCTORS
-    explicit StmtVertex(V3Graph* graphp, AstNodeStmt* stmtp) VL_MT_DISABLED
+    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 ExprVertex final : public DfaVertex {
-    VL_RTTI_IMPL(ExprVertex, V3GraphEdge)
+class DfaExprVertex final : public DfaVertex {
+    VL_RTTI_IMPL(DfaExprVertex, V3GraphEdge)
 public:
     // CONSTRUCTORS
-    explicit ExprVertex(V3Graph* graphp, AstNodeExpr* exprp) VL_MT_DISABLED
+    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 ConditionEdge final : public V3GraphEdge {
-    VL_RTTI_IMPL(ConditionEdge, V3GraphEdge)
+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 ConditionEdge(V3Graph* graphp, DfaVertex* fromp, DfaVertex* top,
-                           bool ifBranch) VL_MT_DISABLED : V3GraphEdge{graphp, fromp, top, 1},
-                                                           m_ifBranch{ifBranch} {}
-    ~ConditionEdge() override = default;
+    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; }
     // LCOV_EXCL_START // Debug code
@@ -104,13 +103,12 @@ public:
 };
 
 // Parse properties and ensemble a property tree graph
-class AssertPropertiesParser final : public VNVisitorConst {
+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
-    bool m_underSExpr
-        = false;  // Whether it is under sequence expression for creating a start node
-    size_t m_underLogNots = 0;  // Number of not operators before sequence
+    bool m_underSExpr = false;  // Is under sequence expression, for creating a start node
+    size_t m_underLogNots = 0;  // Number of 'not' operators before sequence
 
     // VISITORS
     void visit(AstNodeCoverOrAssert* nodep) override { iterateChildrenConst(nodep); }
@@ -121,7 +119,7 @@ class AssertPropertiesParser final : public VNVisitorConst {
     }
     void visit(AstSExpr* nodep) override {
         const auto makeClause = [this, nodep](bool pass) {
-            return new StmtVertex{
+            return new DfaStmtVertex{
                 m_graphp.get(),
                 new AstPExprClause{nodep->fileline(), m_underLogNots % 2 == 0 ? pass : !pass}};
         };
@@ -131,45 +129,46 @@ class AssertPropertiesParser final : public VNVisitorConst {
             m_underSExpr = true;
             iterateConst(nodep->exprp());
         } else {
-            ExprVertex* const exprVtxp
-                = new ExprVertex{m_graphp.get(), nodep->exprp()->unlinkFrBack()};
-            new ConditionEdge{m_graphp.get(), exprVtxp, makeClause(true), true};
-            new ConditionEdge{m_graphp.get(), exprVtxp, makeClause(false), false};
+            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;
         }
 
-        ExprVertex* const startp = m_underSExpr ? nullptr : new ExprVertex{m_graphp.get(), nodep};
+        DfaExprVertex* const startp
+            = m_underSExpr ? nullptr : new DfaExprVertex{m_graphp.get(), nodep};
 
-        StmtVertex* const dlyVtxp
-            = new StmtVertex{m_graphp.get(), nodep->delayp()->unlinkFrBack()};
+        DfaStmtVertex* const dlyVtxp
+            = new DfaStmtVertex{m_graphp.get(), 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");
-            StmtVertex* const sdlyVtxp
-                = new StmtVertex{m_graphp.get(), sexprp->delayp()->unlinkFrBack()};
-            ExprVertex* const exprVtxp
-                = new ExprVertex{m_graphp.get(), sexprp->exprp()->unlinkFrBack()};
+            DfaStmtVertex* const sdlyVtxp
+                = new DfaStmtVertex{m_graphp.get(), sexprp->delayp()->unlinkFrBack()};
+            DfaExprVertex* const exprVtxp
+                = new DfaExprVertex{m_graphp.get(), sexprp->exprp()->unlinkFrBack()};
 
-            if (startp) new ConditionEdge{m_graphp.get(), startp, sdlyVtxp, true};
-            new ConditionEdge{m_graphp.get(), sdlyVtxp, exprVtxp, true};
-            new ConditionEdge{m_graphp.get(), exprVtxp, dlyVtxp, true};
-            new ConditionEdge{m_graphp.get(), dlyVtxp, m_lastp, true};
-            new ConditionEdge{m_graphp.get(), exprVtxp, makeClause(false), false};
+            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};
 
             // 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()) {
-            ExprVertex* const preVtxp
-                = new ExprVertex{m_graphp.get(), nodep->preExprp()->unlinkFrBack()};
-            if (startp) new ConditionEdge{m_graphp.get(), startp, preVtxp, true};
-            new ConditionEdge{m_graphp.get(), preVtxp, dlyVtxp, true};
-            new ConditionEdge{m_graphp.get(), dlyVtxp, m_lastp, true};
-            new ConditionEdge{m_graphp.get(), preVtxp, makeClause(false), false};
+            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;
         } else {
-            if (startp) new ConditionEdge{m_graphp.get(), startp, dlyVtxp, true};
-            new ConditionEdge{m_graphp.get(), dlyVtxp, m_lastp, true};
+            if (startp) new DfaConditionEdge{m_graphp.get(), startp, dlyVtxp, true};
+            new DfaConditionEdge{m_graphp.get(), dlyVtxp, m_lastp, true};
             m_lastp = dlyVtxp;
         }
     }
@@ -178,16 +177,16 @@ class AssertPropertiesParser final : public VNVisitorConst {
 
 public:
     // CONSTRUCTORS
-    explicit AssertPropertiesParser(AstNetlist* nodep) {
+    explicit AssertPropBuildVisitor(AstNetlist* nodep) {
         iterateConst(nodep);
         if (dumpGraphLevel() >= 6) m_graphp->dumpDotFilePrefixedAlways("properties", true);
     }
     std::unique_ptr<V3Graph> graphp() { return std::move(m_graphp); }
-    ~AssertPropertiesParser() override = default;
+    ~AssertPropBuildVisitor() override = default;
 };
 
 // Transform property graph into AST
-class AssertPropertiesTransformer final {
+class AssertPropTransformer final {
     // STATE
     V3UniqueNames m_assertCycleDelayNames{"__Vassert"};  // Names for assertion properties
     const std::unique_ptr<V3Graph> m_graph;  // Property tree
@@ -195,8 +194,8 @@ class AssertPropertiesTransformer final {
     AstBegin* m_current = nullptr;  // Currently built block
 
     V3GraphVertex* processVtx(V3GraphVertex* vtxp) {
-        if (StmtVertex* const stmtp = vtxp->cast<StmtVertex>()) return processVtx(stmtp);
-        if (ExprVertex* const exprp = vtxp->cast<ExprVertex>()) return processVtx(exprp);
+        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);
@@ -204,21 +203,21 @@ class AssertPropertiesTransformer final {
         return nullptr;
         // LCOV_EXCL_STOP
     }
-    V3GraphVertex* processVtx(StmtVertex* vtxp) {
+    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(ExprVertex* vtxp) {
+    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};
             m_pexprp = new AstPExpr{nodep->fileline(), bodyp, nodep->dtypep()};
-            UASSERT_OBJ(vtxp->outSize1() && vtxp->outEdges().frontp()->is<ConditionEdge>(), nodep,
-                        "Incorrect property graph");
+            UASSERT_OBJ(vtxp->outSize1() && vtxp->outEdges().frontp()->is<DfaConditionEdge>(),
+                        nodep, "Incorrect property graph");
             m_current = m_pexprp->bodyp();
             return processEdge(vtxp->outEdges().frontp());
         }
@@ -229,7 +228,7 @@ class AssertPropertiesTransformer final {
         AstNode* const failsp = [vtxp]() -> AstNode* {
             if (!vtxp->outSize1()) {
                 V3GraphVertex* const failVtxp = vtxp->outEdges().backp()->top();
-                return failVtxp->as<StmtVertex>()->nodep();
+                return failVtxp->as<DfaStmtVertex>()->nodep();
             }
             return nullptr;
         }();
@@ -249,10 +248,10 @@ class AssertPropertiesTransformer final {
 
 public:
     // CONSTRUCTORS
-    explicit AssertPropertiesTransformer(std::unique_ptr<V3Graph> graph)
+    explicit AssertPropTransformer(std::unique_ptr<V3Graph> graph)
         : m_graph{std::move(graph)} {
         for (V3GraphVertex& vtx : m_graph->vertices()) {
-            if (DfaVertex* const dVtxp = vtx.cast<ExprVertex>()) {
+            if (DfaVertex* const dVtxp = vtx.cast<DfaExprVertex>()) {
                 if (dVtxp->isStart()) {
                     VL_RESTORER(m_pexprp);
                     processVtx(&vtx);
@@ -265,16 +264,14 @@ public:
     }
 };
 
-}  //namespace
-
 //######################################################################
-// Top AssertProperties class
+// Top AssertProp class
 
-void V3AssertProperties::assertPropertiesAll(AstNetlist* nodep) {
+void V3AssertProp::assertPropAll(AstNetlist* nodep) {
     UINFO(2, __FUNCTION__ << ":");
     {
-        std::unique_ptr<V3Graph> graphp = AssertPropertiesParser{nodep}.graphp();
-        AssertPropertiesTransformer{std::move(graphp)};
+        std::unique_ptr<V3Graph> graphp = AssertPropBuildVisitor{nodep}.graphp();
+        AssertPropTransformer{std::move(graphp)};
     }
     V3Global::dumpCheckGlobalTree("assertproperties", 0, dumpTreeEitherLevel() >= 3);
 }

src/V3AssertProp.h

@@ -1,6 +1,6 @@
 // -*- mode: C++; c-file-style: "cc-mode" -*-
 //*************************************************************************
-// DESCRIPTION: Verilator: Transform sequences into properties
+// DESCRIPTION: Verilator: Implementation of assertion properties
 //
 // Code available from: https://verilator.org
 //
@@ -14,8 +14,8 @@
 //
 //*************************************************************************
 
-#ifndef VERILATOR_V3ASSERTPROPERTIES_H_
-#define VERILATOR_V3ASSERTPROPERTIES_H_
+#ifndef VERILATOR_V3ASSERTPROP_H_
+#define VERILATOR_V3ASSERTPROP_H_
 
 #include "config_build.h"
 #include "verilatedos.h"
@@ -24,9 +24,9 @@ class AstNetlist;
 
 //============================================================================
 
-class V3AssertProperties final {
+class V3AssertProp final {
 public:
-    static void assertPropertiesAll(AstNetlist* nodep) VL_MT_DISABLED;
+    static void assertPropAll(AstNetlist* nodep) VL_MT_DISABLED;
 };
 
 #endif  // Guard

src/V3AstNodeStmt.h

@@ -822,14 +822,15 @@ public:
     bool off() const { return m_off; }
 };
 class AstPExprClause final : public AstNodeStmt {
-    const bool m_passs;
+    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 passs = true)
+    explicit AstPExprClause(FileLine* fl, bool pass = true)
         : ASTGEN_SUPER_PExprClause(fl)
-        , m_passs{passs} {}
-    bool passs() const { return m_passs; }
+        , m_pass{pass} {}
+    bool pass() const { return m_pass; }
 };
 class AstPrintTimeScale final : public AstNodeStmt {
     // Parents: stmtlist

src/V3Width.cpp

@@ -7015,7 +7015,7 @@ class WidthVisitor final : public VNVisitor {
             iterateCheckBool(nodep, "LHS", nodep->op1p(), BOTH);
             nodep->dtypeSetBit();
             if (m_underSExpr) {
-                nodep->v3error("Unexpected not in sequence expression context");
+                nodep->v3error("Unexpected 'not' in sequence expression context");
                 AstConst* const newp = new AstConst{nodep->fileline(), 0};
                 newp->dtypeFrom(nodep);
                 nodep->replaceWith(newp);

src/Verilator.cpp

@@ -20,7 +20,7 @@
 #include "V3ActiveTop.h"
 #include "V3Assert.h"
 #include "V3AssertPre.h"
-#include "V3AssertProperties.h"
+#include "V3AssertProp.h"
 #include "V3Ast.h"
 #include "V3Begin.h"
 #include "V3Branch.h"
@@ -241,7 +241,7 @@ static void process() {
 
         // Assertion insertion
         //    After we've added block coverage, but before other nasty transforms
-        V3AssertProperties::assertPropertiesAll(v3Global.rootp());
+        V3AssertProp::assertPropAll(v3Global.rootp());
         //
         V3AssertPre::assertPreAll(v3Global.rootp());
         //

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 { $$ = new AstLogNot{$1, $2}; }
+                yNOT pexpr
+                        { $$ = new AstLogNot{$1, $2}; }
         |       ySTRONG '(' sexpr ')'
                         { $$ = $3; BBUNSUP($2, "Unsupported: strong (in property expression)"); }
         |       yWEAK '(' sexpr ')'
@@ -6622,15 +6623,13 @@ 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};
+                        { $$ = new AstSExpr{$<fl>1, $1, $2};
                             if (VN_IS($2, LogNot)) {
                                 BBUNSUP($2->fileline(), "Unexpected not in sequence expression context");
                             }
                         }
         |       ~p~sexpr cycle_delay_range sexpr %prec prPOUNDPOUND_MULTI
-                        {
-                            $$ = new AstSExpr{$<fl>2, $1, $2, $3};
-                        }
+                        { $$ = new AstSExpr{$<fl>2, $1, $2, $3}; }
         //
         //                      // IEEE: expression_or_dist [ boolean_abbrev ]
         //                      // Note expression_or_dist includes "expr"!