Fix `disable iff` in simple properties (#6783)

src/V3Assert.cpp

@@ -452,7 +452,19 @@ class AssertVisitor final : public VNVisitor {
         m_underAssert = true;
         iterate(nodep->propp());
 
-        AstNode* bodysp = assertBody(nodep, nodep->propp()->unlinkFrBack(), passsp, failsp);
+        AstNode* propExprp;
+        AstNodeExpr* disablep = nullptr;
+        if (AstPropSpec* const specp = VN_CAST(nodep->propp(), PropSpec)) {
+            propExprp = specp->propp()->unlinkFrBack();
+            if (specp->disablep()) disablep = specp->disablep()->unlinkFrBack();
+        } else {
+            propExprp = nodep->propp()->unlinkFrBack();
+        }
+        AstNode* bodysp = assertBody(nodep, propExprp, passsp, failsp);
+        if (disablep) {
+            bodysp
+                = new AstIf{nodep->fileline(), new AstLogNot{nodep->fileline(), disablep}, bodysp};
+        }
         if (sentreep) {
             bodysp = new AstAlways{nodep->fileline(), VAlwaysKwd::ALWAYS, sentreep, bodysp};
         }

src/V3AssertPre.cpp

@@ -621,29 +621,17 @@ private:
 
     void visit(AstPropSpec* nodep) override {
         nodep = substitutePropertyCall(nodep);
-        // No need to iterate the body, once replace will get iterated
         iterateAndNextNull(nodep->sensesp());
-        if (m_senip)
+        if (m_senip && m_senip != nodep->sensesp())
             nodep->v3warn(E_UNSUPPORTED, "Unsupported: Only one PSL clock allowed per assertion");
-        // Block is the new expression to evaluate
-        AstNodeExpr* blockp = VN_AS(nodep->propp()->unlinkFrBack(), NodeExpr);
         if (!nodep->disablep() && m_defaultDisablep) {
             nodep->disablep(m_defaultDisablep->condp()->cloneTreePure(true));
         }
-        if (AstNodeExpr* const disablep = nodep->disablep()) {
+        m_disablep = nodep->disablep();
-            m_disablep = disablep;
-            if (VN_IS(nodep->backp(), Cover)) {
-                blockp = new AstAnd{disablep->fileline(),
-                                    new AstNot{disablep->fileline(), disablep->unlinkFrBack()},
-                                    blockp};
-            } else {
-                blockp = new AstOr{disablep->fileline(), disablep->unlinkFrBack(), blockp};
-            }
-        }
         // Unlink and just keep a pointer to it, convert to sentree as needed
         m_senip = nodep->sensesp();
-        nodep->replaceWith(blockp);
+        iterateNull(nodep->disablep());
-        VL_DO_DANGLING(pushDeletep(nodep), nodep);
+        iterate(nodep->propp());
     }
     void visit(AstPExpr* nodep) override {
         VL_RESTORER(m_inPExpr);
@@ -656,8 +644,6 @@ private:
         } else {
             iterateChildren(nodep);
         }
-
-        iterateChildren(nodep);
     }
     void visit(AstNodeModule* nodep) override {
         VL_RESTORER(m_defaultClockingp);

test_regress/t/t_assert_disable_iff.v

@@ -35,9 +35,11 @@ module Test (
    else $display("wrong disable");
 `endif
 
-   assert property (@(posedge clk) disable iff (1) 0);
+   assert property (@(posedge clk) disable iff (1) 0) $stop;
+   else $stop;
 
-   assert property (@(posedge clk) disable iff (1) 1);
+   assert property (@(posedge clk) disable iff (1) 1) $stop;
+   else $stop;
 
    assert property (@(posedge clk) disable iff (0) 1);
 

test_regress/t/t_assert_implication.v

@@ -111,13 +111,13 @@ module Test
 
    // Test correct handling of disable iff
    assert property (
-     @(posedge clk) disable iff (cyc < 3)
+     @(posedge clk) disable iff ($sampled(cyc) < 3)
      1 |=> cyc > 3
    );
 
    // Test correct handling of disable iff in current cycle
    assert property (
-     @(posedge clk) disable iff (cyc == 4)
+     @(posedge clk) disable iff ($sampled(cyc) == 4)
      (cyc == 4) |=> 0
    );