From 51ae8e13fbc3f808e26276dd90e1a73f0b6da64b Mon Sep 17 00:00:00 2001 From: Yutetsu TAKATSUKASA Date: Fri, 23 Feb 2024 23:05:53 +0900 Subject: [PATCH] Add --assert-case option (#4919) --- bin/verilator | 1 + docs/guide/exe_verilator.rst | 6 ++- src/V3Assert.cpp | 56 +++++++++++++++++--------- src/V3Options.cpp | 1 + src/V3Options.h | 2 + test_regress/t/t_assert_unique_case.pl | 2 +- 6 files changed, 47 insertions(+), 21 deletions(-) diff --git a/bin/verilator b/bin/verilator index 4f3ef3d89..93e6d11e1 100755 --- a/bin/verilator +++ b/bin/verilator @@ -313,6 +313,7 @@ detailed descriptions of these arguments. +1800-2012ext+ Use SystemVerilog 2012 with file extension +1800-2017ext+ Use SystemVerilog 2017 with file extension --assert Enable all assertions + --assert-case Enable unique/unique0/priority case related checks --autoflush Flush streams after all $displays --bbox-sys Blackbox unknown $system calls --bbox-unsup Blackbox unsupported language features diff --git a/docs/guide/exe_verilator.rst b/docs/guide/exe_verilator.rst index ea564449a..3425701da 100644 --- a/docs/guide/exe_verilator.rst +++ b/docs/guide/exe_verilator.rst @@ -85,7 +85,11 @@ Summary: .. option:: --assert - Enable all assertions. + Enable all assertions. Implies :vlopt:`--assert-case`. + +.. option:: --assert-case + + Enable unique/unique0/priority case related checks. .. option:: --autoflush diff --git a/src/V3Assert.cpp b/src/V3Assert.cpp index a5c584260..682e347b8 100644 --- a/src/V3Assert.cpp +++ b/src/V3Assert.cpp @@ -26,6 +26,13 @@ VL_DEFINE_DEBUG_FUNCTIONS; // Assert class functions class AssertVisitor final : public VNVisitor { + // TYPES + enum assertType_e : uint8_t { + ASSERT_TYPE_INTRINSIC, // AstNodeAssertIntrinsinc + ASSERT_TYPE_SVA, // SVA, PSL + ASSERT_TYPE_CASE, // unique/unique0/priority case related checks + ASSERT_TYPE_IF // unique/unique0/priority if related checks + }; // NODE STATE/TYPES // Cleared on netlist // AstNode::user() -> bool. True if processed @@ -47,6 +54,12 @@ class AssertVisitor final : public VNVisitor { bool m_inSampled = false; // True inside a sampled expression // METHODS + static bool assertTypeOn(assertType_e assertType) { + if (assertType == ASSERT_TYPE_INTRINSIC) return true; + if (v3Global.opt.assertOn()) return true; + if (assertType == ASSERT_TYPE_CASE && v3Global.opt.assertCaseOn()) return true; + return false; + } string assertDisplayMessage(AstNode* nodep, const string& prefix, const string& message, VDisplayType severity) { if (severity == VDisplayType::DT_ERROR || severity == VDisplayType::DT_FATAL) { @@ -99,7 +112,7 @@ class AssertVisitor final : public VNVisitor { varrefp->classOrPackagep(v3Global.rootp()->dollarUnitPkgAddp()); return varrefp; } - AstNode* newIfAssertOn(AstNode* nodep, bool force) { + AstNode* newIfAssertOn(AstNode* nodep, assertType_e assertType) { // Add a internal if to check assertions are on. // Don't make this a AND term, as it's unlikely to need to test this. FileLine* const fl = nodep->fileline(); @@ -107,8 +120,9 @@ class AssertVisitor final : public VNVisitor { // If assertions are off, have constant propagation rip them out later // This allows syntax errors and such to be detected normally. AstNodeExpr* const condp - = force ? static_cast(new AstConst{fl, AstConst::BitTrue{}}) - : v3Global.opt.assertOn() + = assertType == ASSERT_TYPE_INTRINSIC + ? static_cast(new AstConst{fl, AstConst::BitTrue{}}) + : assertTypeOn(assertType) ? static_cast( new AstCExpr{fl, "vlSymsp->_vm_contextp__->assertOn()", 1}) : static_cast(new AstConst{fl, AstConst::BitFalse{}}); @@ -131,9 +145,10 @@ class AssertVisitor final : public VNVisitor { return bodysp; } - AstNode* newFireAssert(AstNode* nodep, const string& message, AstNodeExpr* exprsp = nullptr) { + AstNode* newFireAssert(AstNode* nodep, assertType_e assertType, const string& message, + AstNodeExpr* exprsp = nullptr) { AstNode* bodysp = newFireAssertUnchecked(nodep, message, exprsp); - bodysp = newIfAssertOn(bodysp, false); + bodysp = newIfAssertOn(bodysp, assertType); return bodysp; } @@ -185,16 +200,17 @@ class AssertVisitor final : public VNVisitor { } else { ++m_statAsNotImm; } - const bool force = VN_IS(nodep, AssertIntrinsic); - if (passsp) passsp = newIfAssertOn(passsp, force); - if (failsp) failsp = newIfAssertOn(failsp, force); + const assertType_e assertType + = VN_IS(nodep, AssertIntrinsic) ? ASSERT_TYPE_INTRINSIC : ASSERT_TYPE_SVA; + if (passsp) passsp = newIfAssertOn(passsp, assertType); + if (failsp) failsp = newIfAssertOn(failsp, assertType); if (!passsp && !failsp) failsp = newFireAssertUnchecked(nodep, "'assert' failed."); ifp = new AstIf{nodep->fileline(), propp, passsp, failsp}; ifp->isBoundsCheck(true); // To avoid LATCH warning // It's more LIKELY that we'll take the nullptr if clause // than the sim-killing else clause: ifp->branchPred(VBranchPred::BP_LIKELY); - bodysp = newIfAssertOn(ifp, force); + bodysp = newIfAssertOn(ifp, assertType); } else { nodep->v3fatalSrc("Unknown node type"); } @@ -265,9 +281,9 @@ class AssertVisitor final : public VNVisitor { = ((allow_none || hasDefaultElse) ? static_cast(new AstOneHot0{nodep->fileline(), propp}) : static_cast(new AstOneHot{nodep->fileline(), propp})); - AstIf* const checkifp - = new AstIf{nodep->fileline(), new AstLogNot{nodep->fileline(), ohot}, - newFireAssert(nodep, "'unique if' statement violated"), newifp}; + AstIf* const checkifp = new AstIf{ + nodep->fileline(), new AstLogNot{nodep->fileline(), ohot}, + newFireAssert(nodep, ASSERT_TYPE_IF, "'unique if' statement violated"), newifp}; checkifp->isBoundsCheck(true); // To avoid LATCH warning checkifp->branchPred(VBranchPred::BP_UNLIKELY); nodep->replaceWith(checkifp); @@ -296,9 +312,10 @@ class AssertVisitor final : public VNVisitor { if (!has_default) { nodep->addItemsp(new AstCaseItem{ nodep->fileline(), nullptr /*DEFAULT*/, - newFireAssert( - nodep, nodep->pragmaString() + ", but non-match found" + valFmt, - valFmt.empty() ? nullptr : nodep->exprp()->cloneTreePure(false))}); + newFireAssert(nodep, ASSERT_TYPE_CASE, + nodep->pragmaString() + ", but non-match found" + valFmt, + valFmt.empty() ? nullptr + : nodep->exprp()->cloneTreePure(false))}); } } if (nodep->parallelPragma() || nodep->uniquePragma() || nodep->unique0Pragma()) { @@ -351,11 +368,12 @@ class AssertVisitor final : public VNVisitor { AstNodeExpr* const exprp = nodep->exprp(); const string pragmaStr = nodep->pragmaString(); if (!allow_none) - zeroIfp->addThensp( - newFireAssert(nodep, pragmaStr + ", but none matched" + valFmt, - valFmt.empty() ? nullptr : exprp->cloneTreePure(false))); + zeroIfp->addThensp(newFireAssert( + nodep, ASSERT_TYPE_CASE, pragmaStr + ", but none matched" + valFmt, + valFmt.empty() ? nullptr : exprp->cloneTreePure(false))); zeroIfp->addElsesp( - newFireAssert(nodep, pragmaStr + ", but multiple matches found" + valFmt, + newFireAssert(nodep, ASSERT_TYPE_CASE, + pragmaStr + ", but multiple matches found" + valFmt, valFmt.empty() ? nullptr : exprp->cloneTreePure(false))); ohotIfp->addThensp(zeroIfp); ohotIfp->isBoundsCheck(true); // To avoid LATCH warning diff --git a/src/V3Options.cpp b/src/V3Options.cpp index 50f05f5e6..fc47d3cbd 100644 --- a/src/V3Options.cpp +++ b/src/V3Options.cpp @@ -1105,6 +1105,7 @@ void V3Options::parseOptsList(FileLine* fl, const string& optdir, int argc, // Minus options DECL_OPTION("-assert", OnOff, &m_assert); + DECL_OPTION("-assert-case", OnOff, &m_assertCase); DECL_OPTION("-autoflush", OnOff, &m_autoflush); DECL_OPTION("-bbox-sys", OnOff, &m_bboxSys); diff --git a/src/V3Options.h b/src/V3Options.h index e520826ec..99ba731d1 100644 --- a/src/V3Options.h +++ b/src/V3Options.h @@ -221,6 +221,7 @@ private: bool m_makePhony = false; // main switch: -MP bool m_preprocNoLine = false; // main switch: -P bool m_assert = false; // main switch: --assert + bool m_assertCase = false; // main switch: --assert-case bool m_autoflush = false; // main switch: --autoflush bool m_bboxSys = false; // main switch: --bbox-sys bool m_bboxUnsup = false; // main switch: --bbox-unsup @@ -453,6 +454,7 @@ public: bool std() const { return m_std; } bool structsPacked() const { return m_structsPacked; } bool assertOn() const { return m_assert; } // assertOn as __FILE__ may be defined + bool assertCaseOn() const { return m_assertCase || m_assert; } bool autoflush() const { return m_autoflush; } bool bboxSys() const { return m_bboxSys; } bool bboxUnsup() const { return m_bboxUnsup; } diff --git a/test_regress/t/t_assert_unique_case.pl b/test_regress/t/t_assert_unique_case.pl index 74fab282f..ad2c2c8fc 100755 --- a/test_regress/t/t_assert_unique_case.pl +++ b/test_regress/t/t_assert_unique_case.pl @@ -12,7 +12,7 @@ scenarios(simulator => 1); top_filename("t/t_assert_unique_case_bad.v"); compile( - verilator_flags2 => ["-x-assign 0 --assert --no-stop-fail +define+NO_STOP_FAIL"], + verilator_flags2 => ["-x-assign 0 --assert-case --no-stop-fail +define+NO_STOP_FAIL"], ); execute(