Fully support global $assertcontrol

Signed-off-by: Artur Bieniek <abieniek@antmicro.com>

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.
+    return assertCtlGet(VerilatedAssertCtlQuery::ASSERT_CTL_ON, type, directive);
-    // 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));
 }
 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 &= ~lockedMask;
-        m_s.m_assertOn &= ~(mask & ~m_s.m_assertLock);
         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<int>(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};

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<VerilatedAssertType>::type;
 using VerilatedAssertDirectiveType_t = std::underlying_type<VerilatedAssertDirectiveType>::type;
 
@@ -356,9 +365,10 @@ private:
     static constexpr size_t ASSERT_ON_WIDTH
         = ASSERT_DIRECTIVE_TYPE_MASK_WIDTH * std::numeric_limits<VerilatedAssertType_t>::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<uint32_t> 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<uint32_t> m_assertPassOnVacuous{
+            std::numeric_limits<uint32_t>::max()};  // Enabled vacuous pass actions
+        std::atomic<uint32_t> m_assertPassOnNonvacuous{
+            std::numeric_limits<uint32_t>::max()};  // Enabled nonvacuous pass actions
+        std::atomic<uint32_t> m_assertFailOn{
+            std::numeric_limits<uint32_t>::max()};  // Enabled fail actions
+        std::array<std::atomic<uint32_t>, 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
+    /// Apply assertion control for given control, assertion, and directive types
-    /// 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.
     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)

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<VNRef<AstNodeExpr>, std::unordered_map<VNRef<AstSenTree>, 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)
+                                    assertCtlGetCall("ASSERT_CTL_ON", type, directiveType), 1};
-                                        + ", "s + std::to_string(directiveType) + ")"s,
-                                    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<int>(directiveType)
+                                  & (static_cast<int>(VAssertDirectiveType::ASSERT)
+                                     | static_cast<int>(VAssertDirectiveType::COVER)
+                                     | static_cast<int>(VAssertDirectiveType::ASSUME)));
+        const int checkRuntime = controlled & static_cast<int>(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.
+        // Add an internal if to check assertions are on.
-        // Don't make this a AND term, as it's unlikely to need to test this.
+        // 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<AstNode, AstNode>(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<int>(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();
-
+        UINFO(9, "Generating assertctl for a module: " << m_modp);
-        // control_type, assertion_type and directive_type are integer expressions
+        AstCStmt* const newp = new AstCStmt{fl};
-        // (IEEE 1800-2023 20.11) and may be non-constant; they are evaluated at runtime
+        newp->add("vlSymsp->_vm_contextp__->assertCtl(");
-        // by VerilatedContext::assertCtl. The levels and scope/assertion-list arguments
+        newp->add(nodep->controlTypep()->unlinkFrBack());
-        // are not modeled -- control applies to the whole context.
+        newp->add(", ");
-        // 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).
         if (nodep->assertTypesp()) {
-            if (const AstConst* const typecp = VN_CAST(nodep->assertTypesp(), Const)) {
+            newp->add(nodep->assertTypesp()->unlinkFrBack());
-                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());
         } else {
-            callp->add(std::to_string(ALL_ASSERT_TYPES));
+            newp->add(std::to_string(ALL_ASSERT_TYPES));
         }
-        callp->add(", ");
+        newp->add(", " + std::to_string(nodep->ctlDirectiveTypes()) + ");\n");
-        if (AstNodeExpr* const directivesp = nodep->directiveTypesp()) {
+        nodep->replaceWith(newp);
-            callp->add(directivesp->unlinkFrBack());
-        } else {
-            callp->add(std::to_string(DEFAULT_DIRECTIVE_TYPES));
-        }
-        callp->add(");\n");
-        nodep->replaceWith(callp);
         VL_DO_DANGLING(pushDeletep(nodep), nodep);
     }
     void visit(AstAssertIntrinsic* nodep) override {  //

src/V3AssertNfa.cpp

@@ -194,6 +194,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<int>(directiveType)
+                              & (static_cast<int>(VAssertDirectiveType::ASSERT)
+                                 | static_cast<int>(VAssertDirectiveType::COVER)
+                                 | static_cast<int>(VAssertDirectiveType::ASSUME)));
+    const int checkRuntime = controlled & static_cast<int>(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
 
@@ -1247,6 +1319,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
     };
 
@@ -1265,6 +1340,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 {
@@ -1304,6 +1388,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},
@@ -1374,7 +1459,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},
@@ -1394,7 +1480,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};
 
@@ -1453,13 +1540,22 @@ class SvaNfaLowering final {
             AstIf* const setRIfp = new AstIf{c.flp, gateRp, setRp, nullptr};
             setLIfp->addNext(setRIfp);
 
-            AstIf* const topp = new AstIf{
+            AstNodeExpr* const clearCondp = new AstLogOr{
-                c.flp, c.vtx[ai]->datap()->stateSigp->cloneTreePure(false), clearLp, setLIfp};
+                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.
@@ -1577,7 +1673,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));
             }
@@ -1585,6 +1681,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
@@ -1793,7 +1892,9 @@ public:
                        AstNodeExpr** outMatchpp = nullptr, AstVar* disableCntVarp = nullptr,
                        AstVar* snapshotVarp = nullptr,
                        std::vector<AstNodeExpr*>* outRequiredStepSrcsp = nullptr,
-                       std::vector<AstNodeExpr*>* outPerMidSrcsp = nullptr) {
+                       std::vector<AstNodeExpr*>* 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.
@@ -1826,6 +1927,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);
@@ -1866,9 +1971,9 @@ public:
         }
 
         // Build lowering context for phase sub-functions.
-        LowerCtx c{flp,          N,        vtx,          edges,      startIdx,
+        LowerCtx c{flp,          N,          vtx,           edges,      startIdx,
-                   matchIdx,     senTreep, disableExprp, matchCondp, disableCntVarp,
+                   matchIdx,     senTreep,   disableExprp,  matchCondp, disableCntVarp,
-                   snapshotVarp, graph};
+                   snapshotVarp, assertType, directiveType, killVarp,   graph};
 
         // Phase 1: Resolve combinational Links via fixed-point propagation.
         resolveLinks(c, triggerExprp);
@@ -1877,6 +1982,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);
@@ -2116,6 +2222,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<AstNode, AstNode>(splitsp, nonvacuousp)
+                          : static_cast<AstNode*>(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.
@@ -2251,7 +2389,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);
@@ -2450,8 +2592,11 @@ class AssertNfaVisitor final : public VNVisitor {
         const bool disableExprUnlinked = disableCntVarp && disableExprp;
 
         AstAssert* const assertAssertp = VN_CAST(assertp, Assert);
-        const bool needMatch
+        const bool splitImplicationPasssp = assertAssertp && assertAssertp->passsp()
-            = !isCover && !parts.hasImplication && 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);
@@ -2465,12 +2610,14 @@ class AssertNfaVisitor final : public VNVisitor {
         // coverp / isCoverSeq are computed earlier (passed to SvaNfaBuilder).
         std::vector<AstNodeExpr*> 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;
@@ -2480,8 +2627,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,
+        if (splitImplicationPasssp) {
-                            perSrcSenTreep, requiredStepSrcs);
+            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.

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

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, "if (" + itemp->nameProtect() + " < rhs." + itemp->nameProtect()
-            putns(itemp, itemp->nameProtect());
+                             + ") return true;\n");
+            putns(itemp, "if (rhs." + itemp->nameProtect() + " < " + itemp->nameProtect()
+                             + ") return false;\n");
         }
-        puts(")\n    <  std::tie(");
+        puts("return false;\n");
-        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("}\n");
         puts("};\n");
         puts("template <>\n");

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

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();

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
+%Error-UNSUPPORTED: t/t_assert_ctl_arg_unsup.v:18:5: Unsupported: non-const assert directive type expression
-   18 |     $assertcontrol(OFF, PRIORITY);
+                                                   : ... note: In instance 't'
+   18 |     $assertcontrol(OFF, 1, directive_type);
       |     ^~~~~~~~~~~~~~
 %Error: Exiting due to

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

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;
+    @(posedge clock);
-    $display("%t: deassert reset %d", $time, reset);
+    #1;
+    if (concurrent_fails != 0) $stop;
 
-    #40 $asserton;
+    @(negedge clock);
+    start = 1'b1;
+    done = 1'b0;
 
-    reset = 1'b0;
+    @(negedge clock);
-    $display("%t: deassert reset %d", $time, reset);
+    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;
+  always #5 clock = ~clock;
-  reg r = 1'b0;
-
-  always @(posedge clock) if (reset) r <= 1'b1;
 
   assert_test :
-  assert property (@(posedge clock) (reset | r))
+  assert property (@(posedge clock) start |-> ##1 done)
-  else $error("%t: assertion triggered", $time);
+  else concurrent_fails++;
 
 endmodule

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()

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

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)

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()

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

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()
 

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

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()

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()

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

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()

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));
 

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

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_p1, 23);  // Questa: 23
-      `checkd(count_p2, 89);  // Questa: 44
+      `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