diff --git a/include/verilated.cpp b/include/verilated.cpp index fcfbab58a..c58dde7f4 100644 --- a/include/verilated.cpp +++ b/include/verilated.cpp @@ -3035,20 +3035,7 @@ void VerilatedContext::assertOn(bool flag) VL_MT_SAFE { } bool VerilatedContext::assertOnGet(VerilatedAssertType_t type, VerilatedAssertDirectiveType_t directive) const VL_MT_SAFE { - // Check if selected directive type bit in the assertOn is enabled for assertion type. - // Note: it is assumed that this is checked only for one type at the time. - - // Flag unspecified assertion types as disabled. - if (type == 0) return false; - - // Get index of 3-bit group guarding assertion type status. - // Since the assertOnGet is generated __always__ for a single assert type, we assume that only - // a single bit will be set. Thus, ceil log2 will work fine. - VL_DEBUG_IFDEF(assert((type & (type - 1)) == 0);); - const IData typeMaskPosition = VL_CLOG2_I(type); - - // Check if directive type bit is enabled in corresponding assertion type bits. - return m_s.m_assertOn & (directive << (typeMaskPosition * ASSERT_DIRECTIVE_TYPE_MASK_WIDTH)); + return assertCtlGet(VerilatedAssertCtlQuery::ASSERT_CTL_ON, type, directive); } uint32_t VerilatedContext::assertOnMask(VerilatedAssertType_t types, VerilatedAssertDirectiveType_t directives) VL_PURE { @@ -3072,6 +3059,7 @@ void VerilatedContext::assertCtl(uint32_t controlType, VerilatedAssertType_t typ // IEEE 1800-2023 Table 20-5 control_type. Lock freezes the On/Off state of the // selected bits until Unlock; On/Off/Kill leave locked bits unchanged. const uint32_t mask = assertOnMask(types, directives); + const uint32_t lockedMask = mask & ~m_s.m_assertLock; switch (controlType) { case 1: // Lock m_s.m_assertLock |= mask; @@ -3080,15 +3068,64 @@ void VerilatedContext::assertCtl(uint32_t controlType, VerilatedAssertType_t typ m_s.m_assertLock &= ~mask; break; case 3: // On - m_s.m_assertOn |= mask & ~m_s.m_assertLock; + m_s.m_assertOn |= lockedMask; break; case 4: // Off - case 5: // Kill - m_s.m_assertOn &= ~(mask & ~m_s.m_assertLock); + m_s.m_assertOn &= ~lockedMask; break; - default: // 6..11 (Pass/Fail/Vacuous action control) are not modeled; ignore + case 5: { // Kill + m_s.m_assertOn &= ~lockedMask; + for (int slot = 0; slot < static_cast(ASSERT_CONTROL_SLOT_COUNT); ++slot) { + if (VL_BITISSET_I(lockedMask, slot)) { m_s.m_assertKill[slot]++; } + } break; } + case 6: // PassOn + m_s.m_assertPassOnVacuous |= lockedMask; + m_s.m_assertPassOnNonvacuous |= lockedMask; + break; + case 7: // PassOff + m_s.m_assertPassOnVacuous &= ~lockedMask; + m_s.m_assertPassOnNonvacuous &= ~lockedMask; + break; + case 8: // FailOn + m_s.m_assertFailOn |= lockedMask; + break; + case 9: // FailOff + m_s.m_assertFailOn &= ~lockedMask; + break; + case 10: // NonvacuousOn + m_s.m_assertPassOnNonvacuous |= lockedMask; + break; + case 11: // VacuousOff + m_s.m_assertPassOnVacuous &= ~lockedMask; + break; + default: + VL_WARN_MT("", 0, "", + ("Bad $assertcontrol control_type '" + std::to_string(controlType) + + "' (IEEE 1800-2023 Table 20-5)") + .c_str()); + } +} +uint32_t +VerilatedContext::assertCtlGet(VerilatedAssertCtlQuery query, VerilatedAssertType_t type, + VerilatedAssertDirectiveType_t directive) const VL_MT_SAFE { + const uint32_t mask = assertOnMask(type, directive); + if (!mask) return 0; + switch (query) { // LCOV_EXCL_BR_LINE + case VerilatedAssertCtlQuery::ASSERT_CTL_ON: return (m_s.m_assertOn & mask) != 0; + case VerilatedAssertCtlQuery::ASSERT_CTL_KILL: + assert(mask && (mask & (mask - 1)) == 0); + return m_s.m_assertKill[VL_CLOG2_I(mask)]; + case VerilatedAssertCtlQuery::ASSERT_CTL_PASS_ON_VACUOUS: + return (m_s.m_assertPassOnVacuous & mask) != 0; + case VerilatedAssertCtlQuery::ASSERT_CTL_PASS_ON_NONVACUOUS: + return (m_s.m_assertPassOnNonvacuous & mask) != 0; + case VerilatedAssertCtlQuery::ASSERT_CTL_FAIL_ON: return (m_s.m_assertFailOn & mask) != 0; + default: // LCOV_EXCL_START + VL_FATAL_MT("", 0, "", "Internal: Bad assertCtlGet query"); + VL_UNREACHABLE; + } // LCOV_EXCL_STOP } void VerilatedContext::calcUnusedSigs(bool flag) VL_MT_SAFE { const VerilatedLockGuard lock{m_mutex}; diff --git a/include/verilated.h b/include/verilated.h index f8075567e..a4535f2b4 100644 --- a/include/verilated.h +++ b/include/verilated.h @@ -175,6 +175,15 @@ enum class VerilatedAssertDirectiveType : uint8_t { DIRECTIVE_TYPE_COVER = (1 << 1), DIRECTIVE_TYPE_ASSUME = (1 << 2), }; + +/// Runtime query selector for assertion-control state +enum class VerilatedAssertCtlQuery : uint8_t { + ASSERT_CTL_ON, + ASSERT_CTL_KILL, + ASSERT_CTL_PASS_ON_VACUOUS, + ASSERT_CTL_PASS_ON_NONVACUOUS, + ASSERT_CTL_FAIL_ON, +}; using VerilatedAssertType_t = std::underlying_type::type; using VerilatedAssertDirectiveType_t = std::underlying_type::type; @@ -356,9 +365,10 @@ private: static constexpr size_t ASSERT_ON_WIDTH = ASSERT_DIRECTIVE_TYPE_MASK_WIDTH * std::numeric_limits::digits + 1; - // Build the m_assertOn/m_assertLock bit mask for the given assertion x directive types. + // Build the assertion-control bit mask for the given assertion x directive types. static uint32_t assertOnMask(VerilatedAssertType_t types, VerilatedAssertDirectiveType_t directives) VL_PURE; + static constexpr size_t ASSERT_CONTROL_SLOT_COUNT = ASSERT_ON_WIDTH - 1; protected: // TYPES @@ -381,6 +391,13 @@ protected: std::atomic m_assertLock{0}; // Locked assertion bits (IEEE 1800-2023 20.11 // Lock/Unlock); same layout as m_assertOn. While // a bit is locked, On/Off/Kill leave it unchanged. + std::atomic m_assertPassOnVacuous{ + std::numeric_limits::max()}; // Enabled vacuous pass actions + std::atomic m_assertPassOnNonvacuous{ + std::numeric_limits::max()}; // Enabled nonvacuous pass actions + std::atomic m_assertFailOn{ + std::numeric_limits::max()}; // Enabled fail actions + std::array, ASSERT_CONTROL_SLOT_COUNT> m_assertKill{}; bool m_calcUnusedSigs = false; // Waves file on, need all signals calculated bool m_fatalOnError = true; // Fatal on $stop/non-fatal error bool m_fatalOnVpiError = true; // Fatal on vpi error/unsupported @@ -490,11 +507,13 @@ public: /// Clear enabled status for given assertion types void assertOnClear(VerilatedAssertType_t types, VerilatedAssertDirectiveType_t directives) VL_MT_SAFE; - /// Apply a $assertcontrol control_type (IEEE 1800-2023 Table 20-5) to the given - /// assertion and directive types: 1=Lock, 2=Unlock, 3=On, 4=Off, 5=Kill. Locked - /// bits are left unchanged by On/Off/Kill. Other control_type values are ignored. + /// Apply assertion control for given control, assertion, and directive types void assertCtl(uint32_t controlType, VerilatedAssertType_t types, VerilatedAssertDirectiveType_t directives) VL_MT_SAFE; + /// Get assertion-control runtime state. Boolean queries return 0/1, Kill returns + /// the generation count. + uint32_t assertCtlGet(VerilatedAssertCtlQuery query, VerilatedAssertType_t type, + VerilatedAssertDirectiveType_t directive) const VL_MT_SAFE; /// Return if calculating of unused signals (for traces) bool calcUnusedSigs() const VL_MT_SAFE { return m_s.m_calcUnusedSigs; } /// Enable calculation of unused signals (for traces) diff --git a/src/V3Assert.cpp b/src/V3Assert.cpp index 18df21153..8d4bf5275 100644 --- a/src/V3Assert.cpp +++ b/src/V3Assert.cpp @@ -226,12 +226,23 @@ class AssertVisitor final : public VNVisitor { bool m_inRestrict = false; // True inside restrict assertion AstNode* m_passsp = nullptr; // Current pass statement AstNode* m_failsp = nullptr; // Current fail statement + AstNodeCoverOrAssert* m_assertp = nullptr; // Current assertion AstFinal* m_finalp = nullptr; // Current final block // Map from (expression, senTree) to AstAlways that computes delayed values of the expression std::unordered_map, std::unordered_map, AstAlways*>> m_modExpr2Sen2DelayedAlwaysp; // METHODS + static string assertCtlGetCall(const char* query, VAssertType type, + VAssertDirectiveType directiveType) { + return "vlSymsp->_vm_contextp__->assertCtlGet(VerilatedAssertCtlQuery::"s + query + ", "s + + std::to_string(type) + ", "s + std::to_string(directiveType) + ")"s; + } + static const char* assertPassOnQuery(bool vacuous) { + static constexpr const char* queries[2] + = {"ASSERT_CTL_PASS_ON_NONVACUOUS", "ASSERT_CTL_PASS_ON_VACUOUS"}; + return queries[vacuous]; + } static AstNodeExpr* assertOnCond(FileLine* fl, VAssertType type, VAssertDirectiveType directiveType) { // cppcheck-suppress missingReturn @@ -251,9 +262,7 @@ class AssertVisitor final : public VNVisitor { case VAssertDirectiveType::ASSUME: { if (v3Global.opt.assertOn()) { return new AstCExpr{fl, AstCExpr::Pure{}, - "vlSymsp->_vm_contextp__->assertOnGet("s + std::to_string(type) - + ", "s + std::to_string(directiveType) + ")"s, - 1}; + assertCtlGetCall("ASSERT_CTL_ON", type, directiveType), 1}; } return new AstConst{fl, AstConst::BitFalse{}}; } @@ -269,6 +278,31 @@ class AssertVisitor final : public VNVisitor { } VL_UNREACHABLE; } + static string assertActionControlPrefix(VAssertDirectiveType directiveType) { + const int controlled = !!(static_cast(directiveType) + & (static_cast(VAssertDirectiveType::ASSERT) + | static_cast(VAssertDirectiveType::COVER) + | static_cast(VAssertDirectiveType::ASSUME))); + const int checkRuntime = controlled & static_cast(v3Global.opt.assertOn()); + return "("s + std::to_string(controlled ^ 1) + " || ("s + std::to_string(checkRuntime) + + " && "s; + } + static AstNodeExpr* assertPassOnCond(FileLine* fl, VAssertType type, + VAssertDirectiveType directiveType, bool vacuous) { + return new AstCExpr{fl, AstCExpr::Pure{}, + assertActionControlPrefix(directiveType) + + assertCtlGetCall(assertPassOnQuery(vacuous), type, directiveType) + + "))"s, + 1}; + } + static AstNodeExpr* assertFailOnCond(FileLine* fl, VAssertType type, + VAssertDirectiveType directiveType) { + return new AstCExpr{fl, AstCExpr::Pure{}, + assertActionControlPrefix(directiveType) + + assertCtlGetCall("ASSERT_CTL_FAIL_ON", type, directiveType) + + "))"s, + 1}; + } string assertDisplayMessage(const AstNode* nodep, const string& prefix, const string& message, VDisplayType severity) { if (severity == VDisplayType::DT_ERROR || severity == VDisplayType::DT_FATAL) { @@ -280,12 +314,6 @@ class AssertVisitor final : public VNVisitor { + cvtToStr(nodep->fileline()->lineno()) + ": %m" + ((message != "") ? ": " : "") + message + "\n"); } - // Default assertion_type and directive_type when the argument is omitted - // (IEEE 1800-2023 20.11): assertion_type defaults to all types, directive_type - // to Assert|Cover|Assume. - static constexpr uint8_t DEFAULT_DIRECTIVE_TYPES = VAssertDirectiveType::ASSERT - | VAssertDirectiveType::COVER - | VAssertDirectiveType::ASSUME; void replaceDisplay(AstDisplay* nodep, const string& prefix) { nodep->fmtp()->text( assertDisplayMessage(nodep, prefix, nodep->fmtp()->text(), nodep->displayType())); @@ -327,8 +355,8 @@ class AssertVisitor final : public VNVisitor { } static AstIf* newIfAssertOn(AstNode* bodyp, VAssertDirectiveType directiveType, VAssertType type = VAssertType::INTERNAL) { - // 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. + // Add an internal if to check assertions are on. + // Don't make this an AND term, as it's unlikely to need to test this. FileLine* const fl = bodyp->fileline(); AstNodeExpr* const condp = assertOnCond(fl, type, directiveType); @@ -337,6 +365,28 @@ class AssertVisitor final : public VNVisitor { newp->user2(true); // Mark as an assertOn() check return newp; } + static AstNodeStmt* newIfAssertPassOn(AstNode* bodyp, VAssertDirectiveType directiveType, + VAssertType type, bool vacuous) { + // Add an internal if to check assertion passOn is enabled. + // Don't make this an AND term, as it's unlikely to need to test this. + FileLine* const fl = bodyp->fileline(); + AstNodeExpr* const condp = assertPassOnCond(fl, type, directiveType, vacuous); + AstNodeIf* const newp = new AstIf{fl, condp, bodyp}; + newp->isBoundsCheck(true); // To avoid LATCH warning + newp->user1(true); // Don't assert/cover this if + return newp; + } + static AstNodeStmt* newIfAssertFailOn(AstNode* bodyp, VAssertDirectiveType directiveType, + VAssertType type) { + // Add an internal if to check assertion failOn is enabled. + // Don't make this an AND term, as it's unlikely to need to test this. + FileLine* const fl = bodyp->fileline(); + AstNodeExpr* const condp = assertFailOnCond(fl, type, directiveType); + AstNodeIf* const newp = new AstIf{fl, condp, bodyp}; + newp->isBoundsCheck(true); // To avoid LATCH warning + newp->user1(true); // Don't assert/cover this if + return newp; + } static AstIf* assertCond(const AstNodeCoverOrAssert* nodep, AstNodeExpr* propp, AstNode* passsp, AstNode* failsp) { @@ -493,6 +543,7 @@ class AssertVisitor final : public VNVisitor { if (failsp) failsp->unlinkFrBackWithNext(); bool selfDestruct = false; + bool passspGated = false; if (const AstCover* const snodep = VN_CAST(nodep, Cover)) { ++m_statCover; if (!v3Global.opt.coverageUser()) { @@ -504,6 +555,9 @@ class AssertVisitor final : public VNVisitor { covincp->unlinkFrBackWithNext(); // next() might have AstAssign for trace if (message != "") covincp->declp()->comment(message); if (passsp) { + passsp = newIfAssertPassOn(passsp, nodep->directive(), nodep->userType(), + /*vacuous=*/false); + passspGated = true; passsp = AstNode::addNext(covincp, passsp); } else { passsp = covincp; @@ -524,8 +578,10 @@ class AssertVisitor final : public VNVisitor { VL_RESTORER(m_passsp); VL_RESTORER(m_failsp); + VL_RESTORER(m_assertp); m_passsp = passsp; m_failsp = failsp; + m_assertp = nodep; iterate(nodep->propp()); AstNode* propExprp; @@ -537,6 +593,15 @@ class AssertVisitor final : public VNVisitor { propExprp = nodep->propp()->unlinkFrBack(); } FileLine* const flp = nodep->fileline(); + bool passspAlreadyGated = false; + if (passsp && VN_IS(passsp, If)) passspAlreadyGated = VN_AS(passsp, If)->user1(); + if (passsp && !passspGated && !passspAlreadyGated && !VN_IS(propExprp, PExpr)) { + passsp = newIfAssertPassOn(passsp, nodep->directive(), nodep->userType(), + /*vacuous=*/false); + } + if (failsp && !VN_IS(propExprp, PExpr)) { + failsp = newIfAssertFailOn(failsp, nodep->directive(), nodep->userType()); + } AstNode* bodysp = assertBody(nodep, propExprp, passsp, failsp); if (disablep) bodysp = new AstIf{flp, new AstLogNot{flp, disablep}, bodysp}; // Add assertOn check last, for better combining @@ -870,8 +935,11 @@ class AssertVisitor final : public VNVisitor { if (nodep->pass() && m_passsp) { // Cover adds COVERINC by AstNode::addNext, thus need to clone next too. stmtsp = m_passsp->cloneTree(true); + stmtsp = newIfAssertPassOn(stmtsp, m_assertp->directive(), m_assertp->userType(), + nodep->vacuous()); } else if (!nodep->pass() && m_failsp) { stmtsp = m_failsp->cloneTree(true); + stmtsp = newIfAssertFailOn(stmtsp, m_assertp->directive(), m_assertp->userType()); } if (stmtsp) { stmtsp->foreachAndNext([](AstNodeVarRef* const refp) { @@ -978,66 +1046,69 @@ class AssertVisitor final : public VNVisitor { } void visit(AstAssertCtl* nodep) override { iterateChildren(nodep); + + bool assertTypeConst = true; + if (!nodep->assertTypesp()) { + nodep->ctlAssertTypes(VAssertType{ALL_ASSERT_TYPES}); + } else if (const AstConst* const assertTypesp = VN_CAST(nodep->assertTypesp(), Const)) { + nodep->ctlAssertTypes(VAssertType{assertTypesp->toSInt()}); + } else { + assertTypeConst = false; + } + + bool controlTypeConst = false; + if (const AstConst* const constp = VN_CAST(nodep->controlTypep(), Const)) { + nodep->ctlType(constp->toSInt()); + controlTypeConst = true; + } + if (controlTypeConst + && (nodep->ctlType() < VAssertCtlType::LOCK + || nodep->ctlType() > VAssertCtlType::VACUOUS_OFF)) { + nodep->unlinkFrBack(); + nodep->v3error("Bad $assertcontrol control_type '" + << cvtToStr(static_cast(nodep->ctlType())) + << "' (IEEE 1800-2023 Table 20-5)"); + VL_DO_DANGLING(pushDeletep(nodep), nodep); + return; + } + if (assertTypeConst && nodep->ctlAssertTypes() != ALL_ASSERT_TYPES + && nodep->ctlAssertTypes().containsAny(VAssertType::UNIQUE | VAssertType::UNIQUE0 + | VAssertType::PRIORITY)) { + nodep->v3warn(E_UNSUPPORTED, "Unsupported: assert control assertion_type"); + VL_DO_DANGLING(pushDeletep(nodep->unlinkFrBack()), nodep); + return; + } + + bool directiveTypeConst = true; + if (!nodep->directiveTypesp()) { + nodep->ctlDirectiveTypes(VAssertDirectiveType::ASSERT | VAssertDirectiveType::ASSUME + | VAssertDirectiveType::COVER); + } else if (const AstConst* const directiveTypesp + = VN_CAST(nodep->directiveTypesp(), Const)) { + nodep->ctlDirectiveTypes(VAssertDirectiveType{directiveTypesp->toSInt()}); + } else { + directiveTypeConst = false; + } + if (!directiveTypeConst) { + nodep->v3warn(E_UNSUPPORTED, + "Unsupported: non-const assert directive type expression"); + VL_DO_DANGLING(pushDeletep(nodep->unlinkFrBack()), nodep); + return; + } + FileLine* const fl = nodep->fileline(); - - // control_type, assertion_type and directive_type are integer expressions - // (IEEE 1800-2023 20.11) and may be non-constant; they are evaluated at runtime - // by VerilatedContext::assertCtl. The levels and scope/assertion-list arguments - // are not modeled -- control applies to the whole context. - // When control_type is a compile-time constant, reject the not-yet-modeled - // action-control codes (Table 20-5 values 6..11) and out-of-range values with a - // clear error rather than emitting a runtime no-op. - if (const AstConst* const controlp = VN_CAST(nodep->controlTypep(), Const)) { - const int32_t control = controlp->toSInt(); - if (control < VAssertCtlType::LOCK || control > VAssertCtlType::VACUOUS_OFF) { - nodep->unlinkFrBack(); - nodep->v3warn(EC_ERROR, "Bad $assertcontrol control_type '" - << control << "' (IEEE 1800-2023 Table 20-5)"); - VL_DO_DANGLING(pushDeletep(nodep), nodep); - return; - } - if (control >= VAssertCtlType::PASS_ON) { - nodep->unlinkFrBack(); - nodep->v3warn(E_UNSUPPORTED, - "Unsupported: $assertcontrol control_type '" << control << "'"); - VL_DO_DANGLING(pushDeletep(nodep), nodep); - return; - } - } - - // When assertion_type is a compile-time constant, reject values that cannot be - // filtered at runtime because unique/priority violations use bare assertOn() rather - // than a per-type assertOnGet() call (IEEE 1800-2023 Table 20-6). + UINFO(9, "Generating assertctl for a module: " << m_modp); + AstCStmt* const newp = new AstCStmt{fl}; + newp->add("vlSymsp->_vm_contextp__->assertCtl("); + newp->add(nodep->controlTypep()->unlinkFrBack()); + newp->add(", "); if (nodep->assertTypesp()) { - if (const AstConst* const typecp = VN_CAST(nodep->assertTypesp(), Const)) { - if (typecp->toUInt() - & (VAssertType::EXPECT | VAssertType::UNIQUE | VAssertType::UNIQUE0 - | VAssertType::PRIORITY)) { - nodep->unlinkFrBack(); - nodep->v3warn(E_UNSUPPORTED, "Unsupported: assert control assertion_type"); - VL_DO_DANGLING(pushDeletep(nodep), nodep); - return; - } - } - } - - UINFO(9, "Generating assertctl in module: " << m_modp); - AstCStmt* const callp = new AstCStmt{fl, "vlSymsp->_vm_contextp__->assertCtl("}; - callp->add(nodep->controlTypep()->unlinkFrBack()); - callp->add(", "); - if (AstNodeExpr* const typesp = nodep->assertTypesp()) { - callp->add(typesp->unlinkFrBack()); + newp->add(nodep->assertTypesp()->unlinkFrBack()); } else { - callp->add(std::to_string(ALL_ASSERT_TYPES)); + newp->add(std::to_string(ALL_ASSERT_TYPES)); } - callp->add(", "); - if (AstNodeExpr* const directivesp = nodep->directiveTypesp()) { - callp->add(directivesp->unlinkFrBack()); - } else { - callp->add(std::to_string(DEFAULT_DIRECTIVE_TYPES)); - } - callp->add(");\n"); - nodep->replaceWith(callp); + newp->add(", " + std::to_string(nodep->ctlDirectiveTypes()) + ");\n"); + nodep->replaceWith(newp); VL_DO_DANGLING(pushDeletep(nodep), nodep); } void visit(AstAssertIntrinsic* nodep) override { // diff --git a/src/V3AssertNfa.cpp b/src/V3AssertNfa.cpp index 222d88128..b6ec6964f 100644 --- a/src/V3AssertNfa.cpp +++ b/src/V3AssertNfa.cpp @@ -198,6 +198,78 @@ static AstNodeExpr* sampled(AstNodeExpr* exprp) { return sp; } +static string assertCtlGetCall(const char* query, VAssertType type, + VAssertDirectiveType directiveType) { + return "vlSymsp->_vm_contextp__->assertCtlGet(VerilatedAssertCtlQuery::"s + query + ", "s + + std::to_string(type) + ", "s + std::to_string(directiveType) + ")"s; +} + +static const char* assertPassOnQuery(bool vacuous) { + static constexpr const char* queries[2] + = {"ASSERT_CTL_PASS_ON_NONVACUOUS", "ASSERT_CTL_PASS_ON_VACUOUS"}; + return queries[vacuous]; +} + +static AstNodeExpr* assertOnCond(FileLine* flp, VAssertType type, + VAssertDirectiveType directiveType) { + if (!v3Global.opt.assertOn()) { return new AstConst{flp, AstConst::BitFalse{}}; } + return new AstCExpr{flp, AstCExpr::Pure{}, + assertCtlGetCall("ASSERT_CTL_ON", type, directiveType), 1}; +} + +static AstNodeExpr* assertKillGet(FileLine* flp, VAssertType type, + VAssertDirectiveType directiveType) { + return new AstCExpr{flp, AstCExpr::Pure{}, + assertCtlGetCall("ASSERT_CTL_KILL", type, directiveType), 32}; +} + +static string assertActionControlPrefix(VAssertDirectiveType directiveType) { + const int controlled = !!(static_cast(directiveType) + & (static_cast(VAssertDirectiveType::ASSERT) + | static_cast(VAssertDirectiveType::COVER) + | static_cast(VAssertDirectiveType::ASSUME))); + const int checkRuntime = controlled & static_cast(v3Global.opt.assertOn()); + return "("s + std::to_string(controlled ^ 1) + " || ("s + std::to_string(checkRuntime) + + " && "s; +} + +static AstNodeExpr* assertPassOnCond(FileLine* flp, VAssertType type, + VAssertDirectiveType directiveType, bool vacuous) { + return new AstCExpr{flp, AstCExpr::Pure{}, + assertActionControlPrefix(directiveType) + + assertCtlGetCall(assertPassOnQuery(vacuous), type, directiveType) + + "))"s, + 1}; +} + +static AstNodeExpr* assertFailOnCond(FileLine* flp, VAssertType type, + VAssertDirectiveType directiveType) { + return new AstCExpr{flp, AstCExpr::Pure{}, + assertActionControlPrefix(directiveType) + + assertCtlGetCall("ASSERT_CTL_FAIL_ON", type, directiveType) + "))"s, + 1}; +} + +static AstIf* newPassOnIf(FileLine* flp, AstNodeExpr* firep, AstNode* bodyp, VAssertType type, + VAssertDirectiveType directiveType, bool vacuous) { + AstNodeExpr* const condp + = new AstLogAnd{flp, firep, assertPassOnCond(flp, type, directiveType, vacuous)}; + AstIf* const ifp = new AstIf{flp, condp, bodyp}; + ifp->isBoundsCheck(true); + ifp->user1(true); + return ifp; +} + +static AstNodeStmt* newIfAssertFailOn(AstNode* bodyp, VAssertDirectiveType directiveType, + VAssertType type) { + FileLine* const flp = bodyp->fileline(); + AstNodeExpr* const condp = assertFailOnCond(flp, type, directiveType); + AstIf* const ifp = new AstIf{flp, condp, bodyp}; + ifp->isBoundsCheck(true); + ifp->user1(true); + return ifp; +} + //###################################################################### // NFA Builder @@ -1280,6 +1352,9 @@ class SvaNfaLowering final { AstNodeExpr* matchCondp; // Final boolean match condition (may be nullptr) AstVar* disableCntVarp; // disable counter var (may be nullptr) AstVar* snapshotVarp; // disable snapshot var (may be nullptr) + VAssertType assertType; // Assertion type for control tasks + VAssertDirectiveType directiveType; // Directive type for control tasks + AstVar* killVarp; // Last observed kill generation SvaGraph& graph; // NFA graph }; @@ -1298,6 +1373,15 @@ class SvaNfaLowering final { if (!ap) return bp; return new AstLogOr{flp, ap, bp}; } + static AstNodeExpr* killActive(LowerCtx& c) { + return new AstNeq{c.flp, new AstVarRef{c.flp, c.killVarp, VAccess::READ}, + assertKillGet(c.flp, c.assertType, c.directiveType)}; + } + static AstNodeExpr* notKillActive(LowerCtx& c) { return new AstLogNot{c.flp, killActive(c)}; } + static AstNodeExpr* gateNotKill(LowerCtx& c, AstNodeExpr* exprp) { + if (!exprp) return nullptr; + return new AstLogAnd{c.flp, exprp, notKillActive(c)}; + } // Phase 3 output signals struct SignalSet final { @@ -1337,6 +1421,7 @@ class SvaNfaLowering final { UASSERT_OBJ(nextStatep, c.vtx[i], "Registered vertex has no clocked incoming contribution"); + nextStatep = gateNotKill(c, nextStatep); AstAssignDly* const assignp = new AstAssignDly{ c.flp, new AstVarRef{c.flp, c.vtx[i]->datap()->stateVarp, VAccess::WRITE}, @@ -1407,7 +1492,8 @@ class SvaNfaLowering final { = new AstEq{c.flp, new AstVarRef{c.flp, cntp, VAccess::READ}, new AstConst{c.flp, AstConst::WidthedValue{}, 32, counterMax}}; - AstNodeExpr* const donep = new AstLogOr{c.flp, matchedNowp, counterAtEndp}; + AstNodeExpr* const donep = new AstLogOr{ + c.flp, killActive(c), new AstLogOr{c.flp, matchedNowp, counterAtEndp}}; AstAssignDly* const clearActivep = new AstAssignDly{c.flp, new AstVarRef{c.flp, activep, VAccess::WRITE}, @@ -1427,7 +1513,8 @@ class SvaNfaLowering final { = new AstAssignDly{c.flp, new AstVarRef{c.flp, cntp, VAccess::WRITE}, new AstConst{c.flp, AstConst::WidthedValue{}, 32, 0u}}; setActivep->addNext(resetCountp); - AstIf* const startIfp = new AstIf{c.flp, incomingp, setActivep, nullptr}; + AstIf* const startIfp + = new AstIf{c.flp, gateNotKill(c, incomingp), setActivep, nullptr}; AstIf* const topIfp = new AstIf{c.flp, new AstVarRef{c.flp, activep, VAccess::READ}, doneIfp, startIfp}; @@ -1486,13 +1573,22 @@ class SvaNfaLowering final { AstIf* const setRIfp = new AstIf{c.flp, gateRp, setRp, nullptr}; setLIfp->addNext(setRIfp); - AstIf* const topp = new AstIf{ - c.flp, c.vtx[ai]->datap()->stateSigp->cloneTreePure(false), clearLp, setLIfp}; + AstNodeExpr* const clearCondp = new AstLogOr{ + c.flp, killActive(c), c.vtx[ai]->datap()->stateSigp->cloneTreePure(false)}; + AstIf* const topp = new AstIf{c.flp, clearCondp, clearLp, setLIfp}; m_modp->addStmtsp( new AstAlways{c.flp, VAlwaysKwd::ALWAYS, c.senTreep->cloneTree(false), topp}); } } + void emitKillAckNba(LowerCtx& c) { + AstAssignDly* const ackp + = new AstAssignDly{c.flp, new AstVarRef{c.flp, c.killVarp, VAccess::WRITE}, + assertKillGet(c.flp, c.assertType, c.directiveType)}; + m_modp->addStmtsp(new AstAlways{c.flp, VAlwaysKwd::ALWAYS, c.senTreep->cloneTree(false), + new AstIf{c.flp, killActive(c), ackp, nullptr}}); + } + // Phase 3/3a/3b: Compute terminal match/reject signals, required-step reject, // throughout-drop reject; clean up intermediate state signals. // Phase 3: terminalActive and rejectBase from Links to matchVertex. @@ -1610,7 +1706,7 @@ class SvaNfaLowering final { condp = tep->m_condp->cloneTreePure(false); } AstNodeExpr* const notCondp = new AstLogNot{c.flp, condp}; - AstNodeExpr* const failp = new AstLogAnd{c.flp, srcSigp, notCondp}; + AstNodeExpr* const failp = gateNotKill(c, new AstLogAnd{c.flp, srcSigp, notCondp}); if (outRequiredStepSrcsp) { outRequiredStepSrcsp->push_back(failp->cloneTreePure(false)); } @@ -1618,6 +1714,9 @@ class SvaNfaLowering final { } computeThroughoutReject(c, sigs); + sigs.terminalActivep = gateNotKill(c, sigs.terminalActivep); + sigs.rejectBasep = gateNotKill(c, sigs.rejectBasep); + sigs.throughoutRejectp = gateNotKill(c, sigs.throughoutRejectp); // Clean up intermediate state signals. These are orphan subtrees // (never linked into the enclosing AST); deleteTree() is immediate @@ -1826,7 +1925,9 @@ public: AstNodeExpr** outMatchpp = nullptr, AstVar* disableCntVarp = nullptr, AstVar* snapshotVarp = nullptr, std::vector* outRequiredStepSrcsp = nullptr, - std::vector* outPerMidSrcsp = nullptr) { + std::vector* outPerMidSrcsp = nullptr, + VAssertType assertType = VAssertType::INTERNAL, + VAssertDirectiveType directiveType = VAssertDirectiveType::INTERNAL) { const std::string baseName = m_names.get(""); // Number vertices with sequential colors for array indexing. @@ -1859,6 +1960,10 @@ public: } AstNodeDType* const u32DTypep = m_modp->findBasicDType(VBasicDTypeKwd::UINT32); + AstVar* const killVarp + = new AstVar{flp, VVarType::MODULETEMP, baseName + "__kill", u32DTypep}; + killVarp->lifetime(VLifetime::STATIC_EXPLICIT); + m_modp->addStmtsp(killVarp); for (int i = 0; i < N; ++i) { if (vtx[i]->m_isAndCombiner) { const std::string base = baseName + "__a" + std::to_string(i); @@ -1899,9 +2004,9 @@ public: } // Build lowering context for phase sub-functions. - LowerCtx c{flp, N, vtx, edges, startIdx, - matchIdx, senTreep, disableExprp, matchCondp, disableCntVarp, - snapshotVarp, graph}; + LowerCtx c{flp, N, vtx, edges, startIdx, + matchIdx, senTreep, disableExprp, matchCondp, disableCntVarp, + snapshotVarp, assertType, directiveType, killVarp, graph}; // Phase 1: Resolve combinational Links via fixed-point propagation. resolveLinks(c, triggerExprp); @@ -1910,6 +2015,7 @@ public: emitStateRegisterNba(c); emitCounterFsmNba(c); emitAndCombinerDoneLatchNba(c); + emitKillAckNba(c); // Phase 3/3a/3b: Compute terminal match/reject signals (cleans up stateSig). const SignalSet sigs = computeSignals(c, outRequiredStepSrcsp, outPerMidSrcsp); @@ -2176,6 +2282,38 @@ class AssertNfaVisitor final : public VNVisitor { return parts; } + static bool canSplitImplicationPassActions(const PropertyParts& parts) { + UASSERT(parts.hasImplication, + "Implication pass action split requested without implication"); + UASSERT(parts.triggerExprp, "Implication pass action split requested without trigger"); + // Direct vacuous/nonvacuous classification uses the antecedent value in the current + // assertion attempt. Leave delayed antecedents on the existing NFA pass path. + return !hasMultiCycleExpr(parts.triggerExprp); + } + + static void splitImplicationPassActions(AstAssert* assertp, const PropertyParts& parts, + AstNodeExpr* nonvacuousMatchp) { + FileLine* const flp = assertp->fileline(); + + AstNode* const passsp = assertp->passsp()->unlinkFrBackWithNext(); + AstNode* splitsp = nullptr; + + if (!parts.isFollowedBy) { + AstNodeExpr* const vacuousp + = new AstLogNot{flp, sampled(parts.triggerExprp->cloneTreePure(false))}; + AstNode* const vacuousBodyp = passsp->cloneTree(false); + splitsp = newPassOnIf(flp, vacuousp, vacuousBodyp, assertp->userType(), + assertp->directive(), /*vacuous=*/true); + } + + AstIf* const nonvacuousp + = newPassOnIf(flp, nonvacuousMatchp, passsp, assertp->userType(), assertp->directive(), + /*vacuous=*/false); + splitsp = splitsp ? AstNode::addNext(splitsp, nonvacuousp) + : static_cast(nonvacuousp); + assertp->addPasssp(splitsp); + } + // Allocate disable-iff counter + snapshot vars and unlink the original // disable expression from the PropSpec. Returns {cntp, snapp} or // {nullptr, nullptr} if no counter is needed. @@ -2311,7 +2449,11 @@ class AssertNfaVisitor final : public VNVisitor { cumulativeOrp->cloneTreePure(false)}; m_modp->addStmtsp( new AstAlways{flp, VAlwaysKwd::ALWAYS, perSrcSenTreep->cloneTree(false), - new AstIf{flp, condp, failsp->cloneTree(true), nullptr}}); + new AstIf{flp, condp, + newIfAssertFailOn(failsp->cloneTree(true), + assertWithFailp->directive(), + assertWithFailp->userType()), + nullptr}}); cumulativeOrp = new AstLogOr{flp, cumulativeOrp, srcp->cloneTreePure(false)}; } VL_DO_DANGLING(pushDeletep(cumulativeOrp), cumulativeOrp); @@ -2510,8 +2652,11 @@ class AssertNfaVisitor final : public VNVisitor { const bool disableExprUnlinked = disableCntVarp && disableExprp; AstAssert* const assertAssertp = VN_CAST(assertp, Assert); - const bool needMatch - = !isCover && !parts.hasImplication && assertAssertp && assertAssertp->passsp(); + const bool splitImplicationPasssp = assertAssertp && assertAssertp->passsp() + && parts.hasImplication + && canSplitImplicationPassActions(parts); + const bool needMatch = assertAssertp && assertAssertp->passsp() + && (!parts.hasImplication || splitImplicationPasssp); AstNodeExpr* matchExprp = nullptr; AstAssert* const assertWithFailp = VN_CAST(assertp, Assert); @@ -2525,12 +2670,14 @@ class AssertNfaVisitor final : public VNVisitor { // coverp / isCoverSeq are computed earlier (passed to SvaNfaBuilder). std::vector perMidSrcs; - AstNodeExpr* const alwaysTriggerp = new AstConst{flp, AstConst::BitTrue{}}; + AstNodeExpr* const alwaysTriggerp + = assertOnCond(flp, assertp->userType(), assertp->directive()); AstNodeExpr* const outputExprp = m_loweringp->lower( flp, graph, alwaysTriggerp, senTreep, result.finalCondp, isCover, disableExprp ? disableExprp->cloneTreePure(false) : nullptr, negated, needMatch ? &matchExprp : nullptr, disableCntVarp, snapshotVarp, - needPerSrcFail ? &requiredStepSrcs : nullptr, isCoverSeq ? &perMidSrcs : nullptr); + needPerSrcFail ? &requiredStepSrcs : nullptr, isCoverSeq ? &perMidSrcs : nullptr, + assertp->userType(), assertp->directive()); AstSenTree* const perSrcSenTreep = (requiredStepSrcs.size() >= 2) ? senTreep->cloneTree(false) : nullptr; @@ -2540,8 +2687,15 @@ class AssertNfaVisitor final : public VNVisitor { if (disableExprUnlinked) VL_DO_DANGLING(pushDeletep(disableExprp), disableExprp); if (result.finalCondp && !result.finalCondp->backp()) pushDeletep(result.finalCondp); - attachMatchHandlers(flp, assertAssertp, assertWithFailp, needMatch ? matchExprp : nullptr, - perSrcSenTreep, requiredStepSrcs); + if (splitImplicationPasssp) { + splitImplicationPassActions(assertAssertp, parts, matchExprp); + matchExprp = nullptr; + } else { + attachMatchHandlers(flp, assertAssertp, assertWithFailp, + needMatch ? matchExprp : nullptr, perSrcSenTreep, + requiredStepSrcs); + matchExprp = nullptr; + } if (isCoverSeq && perMidSrcs.size() > 1) { // Clone AstCover (N-1) times, each gated by its own per-mid signal. diff --git a/src/V3AstNodeStmt.h b/src/V3AstNodeStmt.h index 46c49b515..25de3ad08 100644 --- a/src/V3AstNodeStmt.h +++ b/src/V3AstNodeStmt.h @@ -942,13 +942,16 @@ public: class AstPExprClause final : public AstNodeStmt { const bool m_pass; // True if will be replaced by passing assertion clause, false for // assertion failure clause + const bool m_vacuous; // True if pass is vacuous public: ASTGEN_MEMBERS_AstPExprClause; - explicit AstPExprClause(FileLine* fl, bool pass = true) + explicit AstPExprClause(FileLine* fl, bool pass = true, bool vacuous = false) : ASTGEN_SUPER_PExprClause(fl) - , m_pass{pass} {} + , m_pass{pass} + , m_vacuous{vacuous} {} bool pass() const { return m_pass; } + bool vacuous() const { return m_vacuous; } }; class AstPrintTimeScale final : public AstNodeStmt { // Parents: stmtlist diff --git a/src/V3EmitCHeaders.cpp b/src/V3EmitCHeaders.cpp index 524a39222..2a3197112 100644 --- a/src/V3EmitCHeaders.cpp +++ b/src/V3EmitCHeaders.cpp @@ -419,20 +419,14 @@ class EmitCHeader final : public EmitCConstInit { puts("return !(*this == rhs);\n}\n"); putns(sdtypep, "\nbool operator<(const " + EmitCUtil::prefixNameProtect(sdtypep) + "& rhs) const {\n"); - puts("return "); - puts("std::tie("); for (const AstMemberDType* itemp = sdtypep->membersp(); itemp; itemp = VN_AS(itemp->nextp(), MemberDType)) { - if (itemp != sdtypep->membersp()) puts(", "); - putns(itemp, itemp->nameProtect()); + putns(itemp, "if (" + itemp->nameProtect() + " < rhs." + itemp->nameProtect() + + ") return true;\n"); + putns(itemp, "if (rhs." + itemp->nameProtect() + " < " + itemp->nameProtect() + + ") return false;\n"); } - puts(")\n < std::tie("); - for (const AstMemberDType* itemp = sdtypep->membersp(); itemp; - itemp = VN_AS(itemp->nextp(), MemberDType)) { - if (itemp != sdtypep->membersp()) puts(", "); - putns(itemp, "rhs." + itemp->nameProtect()); - } - puts(");\n"); + puts("return false;\n"); puts("}\n"); puts("};\n"); puts("template <>\n"); diff --git a/test_regress/t/t_assert_basic.v b/test_regress/t/t_assert_basic.v index 7d96ac19c..55360519d 100644 --- a/test_regress/t/t_assert_basic.v +++ b/test_regress/t/t_assert_basic.v @@ -13,6 +13,24 @@ module t ( integer cyc; initial cyc = 1; wire [7:0] cyc_copy = cyc[7:0]; + typedef enum logic { CAST_ONE = 1'b1 } cast_e; + cast_e cast_dst; + integer action_hits = 0; + + assert property (@(posedge clk) 1'b1) + if (cyc >= 0) action_hits++; + + assert property (@(posedge clk) 1'b1) + action_hits++; + else + action_hits--; + + cover property (@(posedge clk) 1'b1) + action_hits++; + + initial begin + $cast(cast_dst, 1); + end always @(negedge clk) begin AssertionFalse1 : assert (cyc < 100); @@ -26,6 +44,12 @@ module t ( if (cyc != 0) begin cyc <= cyc + 1; toggle <= !cyc[0]; + assert (cyc >= 0) + if (cyc >= 0) action_hits++; + assert (cyc >= 0) + action_hits++; + else + action_hits--; if (cyc == 7) assert (cyc[0] == cyc[1]); // bug743 if (cyc == 9) begin `ifdef FAILING_ASSERTIONS diff --git a/test_regress/t/t_assert_ctl_arg.cpp b/test_regress/t/t_assert_ctl_arg.cpp index 7e386b5b0..684db6436 100644 --- a/test_regress/t/t_assert_ctl_arg.cpp +++ b/test_regress/t/t_assert_ctl_arg.cpp @@ -82,6 +82,61 @@ void verilatedTest() { contextp->assertOn(false); // Now everything is disabled TEST_CHECK_Z(contextp->assertOn()); + + // Unified runtime query getter + using Query = VerilatedAssertCtlQuery; + constexpr uint32_t LOCK = 1; + constexpr uint32_t UNLOCK = 2; + constexpr uint32_t ON = 3; + constexpr uint32_t OFF = 4; + constexpr uint32_t KILL = 5; + constexpr uint32_t PASS_ON = 6; + constexpr uint32_t PASS_OFF = 7; + constexpr uint32_t FAIL_ON = 8; + constexpr uint32_t FAIL_OFF = 9; + constexpr uint32_t NONVACUOUS_ON = 10; + constexpr uint32_t VACUOUS_OFF = 11; + constexpr uint32_t TYPE = 1; + constexpr uint32_t DIRECTIVE = 1; + + TEST_CHECK_Z(contextp->assertCtlGet(Query::ASSERT_CTL_ON, TYPE, DIRECTIVE)); + TEST_CHECK_Z(contextp->assertCtlGet(Query::ASSERT_CTL_ON, 0, DIRECTIVE)); + + contextp->assertCtl(LOCK, TYPE, DIRECTIVE); + contextp->assertCtl(ON, TYPE, DIRECTIVE); + TEST_CHECK_Z(contextp->assertCtlGet(Query::ASSERT_CTL_ON, TYPE, DIRECTIVE)); + contextp->assertCtl(UNLOCK, TYPE, DIRECTIVE); + contextp->assertCtl(ON, TYPE, DIRECTIVE); + TEST_CHECK_NZ(contextp->assertCtlGet(Query::ASSERT_CTL_ON, TYPE, DIRECTIVE)); + contextp->assertCtl(OFF, TYPE, DIRECTIVE); + TEST_CHECK_Z(contextp->assertCtlGet(Query::ASSERT_CTL_ON, TYPE, DIRECTIVE)); + + const uint32_t killBefore = contextp->assertCtlGet(Query::ASSERT_CTL_KILL, TYPE, DIRECTIVE); + contextp->assertCtl(KILL, TYPE, DIRECTIVE); + TEST_CHECK_EQ(contextp->assertCtlGet(Query::ASSERT_CTL_KILL, TYPE, DIRECTIVE), killBefore + 1); + TEST_CHECK_Z(contextp->assertCtlGet(Query::ASSERT_CTL_ON, TYPE, DIRECTIVE)); + + TEST_CHECK_NZ(contextp->assertCtlGet(Query::ASSERT_CTL_PASS_ON_NONVACUOUS, TYPE, DIRECTIVE)); + TEST_CHECK_NZ(contextp->assertCtlGet(Query::ASSERT_CTL_PASS_ON_VACUOUS, TYPE, DIRECTIVE)); + contextp->assertCtl(PASS_OFF, TYPE, DIRECTIVE); + TEST_CHECK_Z(contextp->assertCtlGet(Query::ASSERT_CTL_PASS_ON_NONVACUOUS, TYPE, DIRECTIVE)); + TEST_CHECK_Z(contextp->assertCtlGet(Query::ASSERT_CTL_PASS_ON_VACUOUS, TYPE, DIRECTIVE)); + + contextp->assertCtl(NONVACUOUS_ON, TYPE, DIRECTIVE); + TEST_CHECK_NZ(contextp->assertCtlGet(Query::ASSERT_CTL_PASS_ON_NONVACUOUS, TYPE, DIRECTIVE)); + TEST_CHECK_Z(contextp->assertCtlGet(Query::ASSERT_CTL_PASS_ON_VACUOUS, TYPE, DIRECTIVE)); + contextp->assertCtl(PASS_ON, TYPE, DIRECTIVE); + TEST_CHECK_NZ(contextp->assertCtlGet(Query::ASSERT_CTL_PASS_ON_NONVACUOUS, TYPE, DIRECTIVE)); + TEST_CHECK_NZ(contextp->assertCtlGet(Query::ASSERT_CTL_PASS_ON_VACUOUS, TYPE, DIRECTIVE)); + contextp->assertCtl(VACUOUS_OFF, TYPE, DIRECTIVE); + TEST_CHECK_NZ(contextp->assertCtlGet(Query::ASSERT_CTL_PASS_ON_NONVACUOUS, TYPE, DIRECTIVE)); + TEST_CHECK_Z(contextp->assertCtlGet(Query::ASSERT_CTL_PASS_ON_VACUOUS, TYPE, DIRECTIVE)); + + TEST_CHECK_NZ(contextp->assertCtlGet(Query::ASSERT_CTL_FAIL_ON, TYPE, DIRECTIVE)); + contextp->assertCtl(FAIL_OFF, TYPE, DIRECTIVE); + TEST_CHECK_Z(contextp->assertCtlGet(Query::ASSERT_CTL_FAIL_ON, TYPE, DIRECTIVE)); + contextp->assertCtl(FAIL_ON, TYPE, DIRECTIVE); + TEST_CHECK_NZ(contextp->assertCtlGet(Query::ASSERT_CTL_FAIL_ON, TYPE, DIRECTIVE)); } int main(int argc, char** argv) { verilatedTest(); diff --git a/test_regress/t/t_assert_ctl_arg_unsup.out b/test_regress/t/t_assert_ctl_arg_unsup.out index da5e1145d..8325ccdf1 100644 --- a/test_regress/t/t_assert_ctl_arg_unsup.out +++ b/test_regress/t/t_assert_ctl_arg_unsup.out @@ -1,14 +1,18 @@ %Error-UNSUPPORTED: t/t_assert_ctl_arg_unsup.v:15:5: Unsupported: assert control assertion_type - 15 | $assertcontrol(OFF, EXPECT); + : ... note: In instance 't' + 15 | $assertcontrol(OFF, UNIQUE); | ^~~~~~~~~~~~~~ ... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest %Error-UNSUPPORTED: t/t_assert_ctl_arg_unsup.v:16:5: Unsupported: assert control assertion_type - 16 | $assertcontrol(OFF, UNIQUE); + : ... note: In instance 't' + 16 | $assertcontrol(OFF, UNIQUE0); | ^~~~~~~~~~~~~~ %Error-UNSUPPORTED: t/t_assert_ctl_arg_unsup.v:17:5: Unsupported: assert control assertion_type - 17 | $assertcontrol(OFF, UNIQUE0); + : ... note: In instance 't' + 17 | $assertcontrol(OFF, PRIORITY); | ^~~~~~~~~~~~~~ -%Error-UNSUPPORTED: t/t_assert_ctl_arg_unsup.v:18:5: Unsupported: assert control assertion_type - 18 | $assertcontrol(OFF, PRIORITY); +%Error-UNSUPPORTED: t/t_assert_ctl_arg_unsup.v:18:5: Unsupported: non-const assert directive type expression + : ... note: In instance 't' + 18 | $assertcontrol(OFF, 1, directive_type); | ^~~~~~~~~~~~~~ %Error: Exiting due to diff --git a/test_regress/t/t_assert_ctl_arg_unsup.v b/test_regress/t/t_assert_ctl_arg_unsup.v index b041652f2..c82410860 100644 --- a/test_regress/t/t_assert_ctl_arg_unsup.v +++ b/test_regress/t/t_assert_ctl_arg_unsup.v @@ -6,15 +6,15 @@ module t; let OFF = 4; - let EXPECT = 16; let UNIQUE = 32; let UNIQUE0 = 64; let PRIORITY = 128; + logic directive_type = 1'b1; initial begin - $assertcontrol(OFF, EXPECT); $assertcontrol(OFF, UNIQUE); $assertcontrol(OFF, UNIQUE0); $assertcontrol(OFF, PRIORITY); + $assertcontrol(OFF, 1, directive_type); end endmodule diff --git a/test_regress/t/t_assert_ctl_concurrent.v b/test_regress/t/t_assert_ctl_concurrent.v index 3cdda2bc1..c7d62648a 100644 --- a/test_regress/t/t_assert_ctl_concurrent.v +++ b/test_regress/t/t_assert_ctl_concurrent.v @@ -7,32 +7,49 @@ module t; bit clock = 1'b0; - bit reset = 1'b0; + bit start = 1'b0; + bit done = 1'b0; + int concurrent_fails = 0; initial begin + $asserton; + + @(negedge clock); + start = 1'b1; + done = 1'b0; + + @(negedge clock); + start = 1'b0; $assertkill; + $asserton; - #10 reset = 1'b1; - $display("%t: deassert reset %d", $time, reset); + @(posedge clock); + #1; + if (concurrent_fails != 0) $stop; - #40 $asserton; + @(negedge clock); + start = 1'b1; + done = 1'b0; - reset = 1'b0; - $display("%t: deassert reset %d", $time, reset); + @(negedge clock); + start = 1'b0; - #200 $display("%t: finish", $time); + @(posedge clock); + #1; + if (concurrent_fails != 1) $stop; + + $assertcontrol(5, 1, 1); + $asserton; + + $display("%t: finish", $time); $write("*-* All Finished *-*\n"); $finish; - end - always #10 clock = ~clock; - reg r = 1'b0; - - always @(posedge clock) if (reset) r <= 1'b1; + always #5 clock = ~clock; assert_test : - assert property (@(posedge clock) (reset | r)) - else $error("%t: assertion triggered", $time); + assert property (@(posedge clock) start |-> ##1 done) + else concurrent_fails++; endmodule diff --git a/test_regress/t/t_assert_ctl_unsup.py b/test_regress/t/t_assert_ctl_pass_actions.py similarity index 70% rename from test_regress/t/t_assert_ctl_unsup.py rename to test_regress/t/t_assert_ctl_pass_actions.py index da00b062f..fdd1c0d4d 100755 --- a/test_regress/t/t_assert_ctl_unsup.py +++ b/test_regress/t/t_assert_ctl_pass_actions.py @@ -4,13 +4,15 @@ # This program is free software; you can redistribute it and/or modify it # under the terms of either the GNU Lesser General Public License Version 3 # or the Perl Artistic License Version 2.0. -# SPDX-FileCopyrightText: 2024 Wilson Snyder +# SPDX-FileCopyrightText: 2026 Wilson Snyder # SPDX-License-Identifier: LGPL-3.0-only OR Artistic-2.0 import vltest_bootstrap -test.scenarios('linter') +test.scenarios('vlt') -test.lint(verilator_flags2=['--assert'], fails=True, expect_filename=test.golden_filename) +test.compile(verilator_flags2=["--binary --assert"]) + +test.execute() test.passes() diff --git a/test_regress/t/t_assert_ctl_pass_actions.v b/test_regress/t/t_assert_ctl_pass_actions.v new file mode 100644 index 000000000..3768f4bd1 --- /dev/null +++ b/test_regress/t/t_assert_ctl_pass_actions.v @@ -0,0 +1,214 @@ +// DESCRIPTION: Verilator: Verilog Test module +// +// This file ONLY is placed under the Creative Commons Public Domain. +// SPDX-FileCopyrightText: 2026 Antmicro +// SPDX-License-Identifier: CC0-1.0 + +// verilog_format: off +`define stop $stop +`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) +// verilog_format: on + +`ifdef VERILATOR +// The '$c(1)' is there to prevent inlining of the signal by V3Gate. +`define IMPURE_ONE ($c(1)) +`else +// Use standard $random. The chance of getting 2 consecutive zeroes is negligible. +`define IMPURE_ONE (|($random | $random)) +`endif + +interface AssertCtlIface; + bit run_initial = 0; + bit initial_done = 0; + int fails = 0; + + function void clear(); + fails = 0; + endfunction + function void assert_off(); + $assertcontrol(4, 2, 1); + endfunction + function void assert_on(); + $assertcontrol(3, 2, 1); + endfunction + function void fail_check(); + assert (0) `stop; else fails++; + endfunction + function void run_checks(); + assert_off(); + fail_check(); + assert_on(); + fail_check(); + endfunction + + initial begin + wait (run_initial); + run_checks(); + initial_done = 1; + end +endinterface + +module t; + bit clk = 0; + int imm_passes = 0; + int imm_fails = 0; + int vacuous_passes = 0; + int nonvacuous_passes = 0; + int concurrent_fails = 0; + int class_fails = 0; + + class AssertCtlClass; + function void assert_off(); + $assertcontrol(4, 2, 1); + endfunction + function void assert_on(); + $assertcontrol(3, 2, 1); + endfunction + function void fail_check(); + assert (0) `stop; else class_fails++; + endfunction + endclass + + AssertCtlClass assert_ctl_class; + AssertCtlIface assert_ctl_iface(); + virtual AssertCtlIface v_assert_ctl_iface = assert_ctl_iface; + + always #5 clk = !clk; + + default clocking @(posedge clk); + endclocking + + assert property (@(posedge clk) 1'b0 |-> ##1 1'b1) begin + vacuous_passes++; + end else + `stop; + + assert property (@(posedge clk) 1'b1 |-> ##1 1'b1) begin + nonvacuous_passes++; + end else + `stop; + + assert property (@(posedge clk) 1'b1 |-> ##1 1'b0) begin + end else + concurrent_fails++; + + task automatic tick_and_check(input int exp_vacuous, input int exp_nonvacuous, + input int exp_concurrent_fails); + @(posedge clk); + #2; + `checkd(vacuous_passes, exp_vacuous); + `checkd(nonvacuous_passes, exp_nonvacuous); + `checkd(concurrent_fails, exp_concurrent_fails); + endtask + + initial begin + assert_ctl_class = new; + + $assertcontrol(4, 16, 1); + $assertcontrol(5, 16, 1); + $assertcontrol(3*`IMPURE_ONE, 2*`IMPURE_ONE); + + $assertcontrol(3, 255, 7); + $assertcontrol(6, 255, 7); + $assertcontrol(8, 255, 7); + + assert (1) imm_passes++; else `stop; + `checkd(imm_passes, 1); + + $assertcontrol(1, 2, 1); + $assertcontrol(4, 2, 1); + assert (1) imm_passes++; else `stop; + `checkd(imm_passes, 2); + + $assertcontrol(2, 2, 1); + $assertcontrol(4, 2, 1); + assert (1) imm_passes++; else `stop; + `checkd(imm_passes, 2); + + $assertcontrol(3, 2, 1); + + $assertcontrol(1, 2, 1); + $assertcontrol(7, 2, 1); + assert (1) imm_passes++; else `stop; + `checkd(imm_passes, 3); + + $assertcontrol(2, 2, 1); + $assertcontrol(7, 2, 1); + assert (1) imm_passes++; else `stop; + `checkd(imm_passes, 3); + + $assertcontrol(10, 2, 1); + assert (1) imm_passes++; else `stop; + `checkd(imm_passes, 4); + + $assertcontrol(11, 2, 1); + assert (1) imm_passes++; else `stop; + `checkd(imm_passes, 5); + + $assertcontrol(6, 2, 1); + + assert (0) `stop; else imm_fails++; + `checkd(imm_fails, 1); + + $assertcontrol(1, 2, 1); + $assertcontrol(9, 2, 1); + assert (0) `stop; else imm_fails++; + `checkd(imm_fails, 2); + + $assertcontrol(2, 2, 1); + $assertcontrol(9, 2, 1); + assert (0) `stop; else imm_fails++; + `checkd(imm_fails, 2); + + $assertcontrol(8, 2, 1); + assert (0) `stop; else imm_fails++; + `checkd(imm_fails, 3); + + assert_ctl_class.assert_off(); + assert_ctl_class.fail_check(); + `checkd(class_fails, 0); + + assert_ctl_class.assert_on(); + assert_ctl_class.fail_check(); + `checkd(class_fails, 1); + + assert_ctl_iface.run_initial = 1; + wait (assert_ctl_iface.initial_done); + `checkd(assert_ctl_iface.fails, 1); + + assert_ctl_iface.clear(); + assert_ctl_iface.run_checks(); + `checkd(assert_ctl_iface.fails, 1); + + assert_ctl_iface.clear(); + v_assert_ctl_iface.run_checks(); + `checkd(assert_ctl_iface.fails, 1); + + $assertcontrol(9, 1, 1); + + tick_and_check(1, 0, 0); + tick_and_check(2, 1, 0); + + $assertcontrol(11, 1, 1); + tick_and_check(2, 2, 0); + + $assertcontrol(7, 1, 1); + tick_and_check(2, 2, 0); + + $assertcontrol(10, 1, 1); + tick_and_check(2, 3, 0); + + $assertcontrol(6, 1, 1); + tick_and_check(3, 4, 0); + + $assertcontrol(8, 1, 1); + tick_and_check(4, 5, 1); + + $write("*-* All Finished *-*\n"); + $finish; + end +endmodule diff --git a/test_regress/t/t_assert_ctl_type_runtime_bad.out b/test_regress/t/t_assert_ctl_type_runtime_bad.out new file mode 100644 index 000000000..aaa9ff404 --- /dev/null +++ b/test_regress/t/t_assert_ctl_type_runtime_bad.out @@ -0,0 +1 @@ +%Warning: Bad $assertcontrol control_type '100' (IEEE 1800-2023 Table 20-5) diff --git a/test_regress/t/t_assert_ctl_type_runtime_bad.py b/test_regress/t/t_assert_ctl_type_runtime_bad.py new file mode 100755 index 000000000..84d6702d8 --- /dev/null +++ b/test_regress/t/t_assert_ctl_type_runtime_bad.py @@ -0,0 +1,18 @@ +#!/usr/bin/env python3 +# DESCRIPTION: Verilator: Verilog Test driver/expect definition +# +# This program is free software; you can redistribute it and/or modify it +# under the terms of either the GNU Lesser General Public License Version 3 +# or the Perl Artistic License Version 2.0. +# SPDX-FileCopyrightText: 2026 Wilson Snyder +# SPDX-License-Identifier: LGPL-3.0-only OR Artistic-2.0 + +import vltest_bootstrap + +test.scenarios('simulator') + +test.compile(verilator_flags2=['--binary', '--assert']) + +test.execute(expect_filename=test.golden_filename) + +test.passes() diff --git a/test_regress/t/t_assert_ctl_type_runtime_bad.v b/test_regress/t/t_assert_ctl_type_runtime_bad.v new file mode 100644 index 000000000..d35421daf --- /dev/null +++ b/test_regress/t/t_assert_ctl_type_runtime_bad.v @@ -0,0 +1,20 @@ +// DESCRIPTION: Verilator: Verilog Test module +// +// This file ONLY is placed under the Creative Commons Public Domain. +// SPDX-FileCopyrightText: 2026 Antmicro +// SPDX-License-Identifier: CC0-1.0 + +`ifdef VERILATOR +// The '$c1(1)' is there to prevent inlining of the signal by V3Gate +`define IMPURE_ONE ($c(1)) +`else +// Use standard $random (chaces of getting 2 consecutive zeroes is zero). +`define IMPURE_ONE (|($random | $random)) +`endif + +module t; + initial begin + $assertcontrol(100*`IMPURE_ONE); + $finish; + end +endmodule diff --git a/test_regress/t/t_assert_disabled.py b/test_regress/t/t_assert_disabled.py index 3a4d31c50..390d36ef3 100755 --- a/test_regress/t/t_assert_disabled.py +++ b/test_regress/t/t_assert_disabled.py @@ -10,9 +10,9 @@ import vltest_bootstrap test.scenarios('simulator') -test.top_filename = "t/t_assert_on.v" +test.top_filename = "t/t_assert_disabled.v" -test.compile(verilator_flags2=['--no-assert']) +test.compile(verilator_flags2=['--no-assert', '--timing']) test.execute() diff --git a/test_regress/t/t_assert_disabled.v b/test_regress/t/t_assert_disabled.v new file mode 100644 index 000000000..447253c68 --- /dev/null +++ b/test_regress/t/t_assert_disabled.v @@ -0,0 +1,34 @@ +// DESCRIPTION: Verilator: Verilog Test module +// +// This file ONLY is placed under the Creative Commons Public Domain. +// SPDX-FileCopyrightText: 2026 Antmicro +// SPDX-License-Identifier: CC0-1.0 + +// verilog_format: off +`define stop $stop +`define checkd(gotv,expv) do if ((gotv) !== (expv)) begin $write("%%Error: %s:%0d: got=%0d exp=%0d\n", `__FILE__,`__LINE__, (gotv), (expv)); `stop; end while(0); +// verilog_format: on + +module t ( + input clk +); + + integer action_hits = 0; + integer cyc = 0; + + assert property (@(posedge clk) ##1 1'b1) + action_hits++; + else + action_hits--; + + always @(posedge clk) begin + cyc++; + assert (0); + if (cyc == 4) begin + `checkd(action_hits, 0); + $write("*-* All Finished *-*\n"); + $finish; + end + end + +endmodule diff --git a/test_regress/t/t_assert_opt_check.py b/test_regress/t/t_assert_opt_check.py index 884e2876c..62b5a95d0 100755 --- a/test_regress/t/t_assert_opt_check.py +++ b/test_regress/t/t_assert_opt_check.py @@ -16,6 +16,6 @@ test.compile(verilator_flags2=['--binary', '--stats']) test.execute(check_finished=True) test.file_grep(test.stats, r'Assertions, assertOn checks combined\s+(\d+)', 3) -test.file_grep(test.stats, r'Assertions, assertOn checks hoisted\s+(\d+)', 15) +test.file_grep(test.stats, r'Assertions, assertOn checks hoisted\s+(\d+)', 16) test.passes() diff --git a/test_regress/t/t_assertcontrol.py b/test_regress/t/t_assertcontrol.py new file mode 100755 index 000000000..fdd1c0d4d --- /dev/null +++ b/test_regress/t/t_assertcontrol.py @@ -0,0 +1,18 @@ +#!/usr/bin/env python3 +# DESCRIPTION: Verilator: Verilog Test driver/expect definition +# +# This program is free software; you can redistribute it and/or modify it +# under the terms of either the GNU Lesser General Public License Version 3 +# or the Perl Artistic License Version 2.0. +# SPDX-FileCopyrightText: 2026 Wilson Snyder +# SPDX-License-Identifier: LGPL-3.0-only OR Artistic-2.0 + +import vltest_bootstrap + +test.scenarios('vlt') + +test.compile(verilator_flags2=["--binary --assert"]) + +test.execute() + +test.passes() diff --git a/test_regress/t/t_assertcontrol.v b/test_regress/t/t_assertcontrol.v new file mode 100644 index 000000000..26f9d360b --- /dev/null +++ b/test_regress/t/t_assertcontrol.v @@ -0,0 +1,113 @@ +// DESCRIPTION: Verilator: Verilog Test module +// +// This file ONLY is placed under the Creative Commons Public Domain. +// SPDX-FileCopyrightText: 2026 Antmicro +// SPDX-License-Identifier: CC0-1.0 + +// verilog_format: off +`define stop $stop +`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) +// verilog_format: on + +module t; + let LOCK = 1; + let UNLOCK = 2; + let ON = 3; + let OFF = 4; + let PASS_ON = 6; + let PASS_OFF = 7; + let FAIL_ON = 8; + let FAIL_OFF = 9; + + let SIMPLE_IMMEDIATE = 2; + let ASSERT = 1; + + int pass_count = 0; + int fail_count = 0; + int ctl_type = 0; + + task automatic run_pass(); + assert (1) begin + pass_count++; + end else + `stop; + endtask + + task automatic run_fail(); + assert (0) + `stop; + else begin + fail_count++; + end + endtask + + initial begin + $assertcontrol(ON, 255, 7); + $assertcontrol(PASS_ON, 255, 7); + $assertcontrol(FAIL_ON, 255, 7); + + run_pass(); + `checkd(pass_count, 1); + + // Lock preserves the enabled checking state against OFF. + $assertcontrol(LOCK, SIMPLE_IMMEDIATE, ASSERT); + ctl_type = OFF; + $assertcontrol(ctl_type, SIMPLE_IMMEDIATE, ASSERT); + run_pass(); + `checkd(pass_count, 2); + + $assertcontrol(UNLOCK, SIMPLE_IMMEDIATE, ASSERT); + $assertcontrol(OFF, SIMPLE_IMMEDIATE, ASSERT); + run_pass(); + `checkd(pass_count, 2); + + // Lock preserves the disabled checking state against ON. + $assertcontrol(LOCK, SIMPLE_IMMEDIATE, ASSERT); + $assertcontrol(ON, SIMPLE_IMMEDIATE, ASSERT); + run_pass(); + `checkd(pass_count, 2); + + $assertcontrol(UNLOCK, SIMPLE_IMMEDIATE, ASSERT); + $assertcontrol(ON, SIMPLE_IMMEDIATE, ASSERT); + run_pass(); + `checkd(pass_count, 3); + + // Lock also preserves pass-action state. + $assertcontrol(LOCK, SIMPLE_IMMEDIATE, ASSERT); + $assertcontrol(PASS_OFF, SIMPLE_IMMEDIATE, ASSERT); + run_pass(); + `checkd(pass_count, 4); + + $assertcontrol(UNLOCK, SIMPLE_IMMEDIATE, ASSERT); + $assertcontrol(PASS_OFF, SIMPLE_IMMEDIATE, ASSERT); + run_pass(); + `checkd(pass_count, 4); + + $assertcontrol(PASS_ON, SIMPLE_IMMEDIATE, ASSERT); + + run_fail(); + `checkd(fail_count, 1); + + // Lock also preserves fail-action state. + $assertcontrol(LOCK, SIMPLE_IMMEDIATE, ASSERT); + $assertcontrol(FAIL_OFF, SIMPLE_IMMEDIATE, ASSERT); + run_fail(); + `checkd(fail_count, 2); + + $assertcontrol(UNLOCK, SIMPLE_IMMEDIATE, ASSERT); + $assertcontrol(FAIL_OFF, SIMPLE_IMMEDIATE, ASSERT); + run_fail(); + `checkd(fail_count, 2); + + $assertcontrol(FAIL_ON, SIMPLE_IMMEDIATE, ASSERT); + run_fail(); + `checkd(fail_count, 3); + + $write("*-* All Finished *-*\n"); + $finish; + end +endmodule diff --git a/test_regress/t/t_assertcontrol_noinl.py b/test_regress/t/t_assertcontrol_noinl.py new file mode 100755 index 000000000..cbc5575bf --- /dev/null +++ b/test_regress/t/t_assertcontrol_noinl.py @@ -0,0 +1,19 @@ +#!/usr/bin/env python3 +# DESCRIPTION: Verilator: Verilog Test driver/expect definition +# +# This program is free software; you can redistribute it and/or modify it +# under the terms of either the GNU Lesser General Public License Version 3 +# or the Perl Artistic License Version 2.0. +# SPDX-FileCopyrightText: 2026 Wilson Snyder +# SPDX-License-Identifier: LGPL-3.0-only OR Artistic-2.0 + +import vltest_bootstrap + +test.scenarios('vlt') +test.top_filename = "t_assertcontrol.v" + +test.compile(verilator_flags2=["--binary --assert --fno-inline"]) + +test.execute() + +test.passes() diff --git a/test_regress/t/t_prop_followed_by.v b/test_regress/t/t_prop_followed_by.v index 0fea33f5b..c1e5778a6 100644 --- a/test_regress/t/t_prop_followed_by.v +++ b/test_regress/t/t_prop_followed_by.v @@ -25,9 +25,12 @@ module t ( integer impl_f = 0; integer nimp_f = 0; integer wide_f = 0; + integer action_hits = 0; // Smoke: trivially-true forms must compile and never fail. assert property (@(posedge clk) 1'b1 #-# 1'b1); + assert property (@(posedge clk) 1'b1 #-# 1'b1) + action_hits++; assert property (@(posedge clk) 0 |-> (0 #-# 0)); assert property (@(posedge clk) 0 |-> (0 #=# 0)); diff --git a/test_regress/t/t_property_sexpr_cov.v b/test_regress/t/t_property_sexpr_cov.v index 59fa3ddc9..ef58a1fd8 100644 --- a/test_regress/t/t_property_sexpr_cov.v +++ b/test_regress/t/t_property_sexpr_cov.v @@ -52,4 +52,12 @@ module t ( /*AUTOARG*/ cover property (@(posedge clk) ##3 val[0] && val[1]) $display("[%0t] concurrent cover, fileline:%0d", $time, `__LINE__); + + integer action_hits = 0; + + assert property (@(posedge clk) ##1 1'b1) + action_hits++; + + assert property (@(posedge clk) (val[0] ##1 val[1]) |-> 1'b1) + action_hits++; endmodule diff --git a/test_regress/t/t_sequence_within.v b/test_regress/t/t_sequence_within.v index a8ec28b25..093b7afcb 100644 --- a/test_regress/t/t_sequence_within.v +++ b/test_regress/t/t_sequence_within.v @@ -91,6 +91,8 @@ module t ( (a ##3 b) intersect ((c ##1 d) within (a ##3 b))) count_p10 <= count_p10 + 1; + initial $assertvacuousoff; + always_ff @(posedge clk) begin cyc <= cyc + 1; crc <= {crc[62:0], crc[63] ^ crc[2] ^ crc[0]}; @@ -103,11 +105,11 @@ module t ( // p1/p2/p5 use |->; the NFA currently fires the pass action on // vacuous passes too, so counts are inflated vs. Questa. Pre-existing // engine-wide behavior, not within-specific. - `checkd(count_p1, 89); // Questa: 23 - `checkd(count_p2, 89); // Questa: 44 + `checkd(count_p1, 23); // Questa: 23 + `checkd(count_p2, 44); // Questa: 44 `checkd(count_p3, 26); // Questa: 20 `checkd(count_p4, 24); // Questa: 22 - `checkd(count_p5, 89); // Questa: 26 + `checkd(count_p5, 26); // Questa: 26 `checkd(count_p6, 21); // Questa: 16 `checkd(count_p7, 15); // Questa: 9 `checkd(count_p8, 15); // Questa: 4