diff --git a/src/V3Assert.cpp b/src/V3Assert.cpp index 02e06592e..fc29de08c 100644 --- a/src/V3Assert.cpp +++ b/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}; } diff --git a/src/V3AssertPre.cpp b/src/V3AssertPre.cpp index 92a4b46aa..49ca80995 100644 --- a/src/V3AssertPre.cpp +++ b/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 = 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}; - } - } + m_disablep = nodep->disablep(); // Unlink and just keep a pointer to it, convert to sentree as needed m_senip = nodep->sensesp(); - nodep->replaceWith(blockp); - VL_DO_DANGLING(pushDeletep(nodep), nodep); + iterateNull(nodep->disablep()); + 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); diff --git a/test_regress/t/t_assert_disable_iff.v b/test_regress/t/t_assert_disable_iff.v index 23ec387bc..764a406bc 100644 --- a/test_regress/t/t_assert_disable_iff.v +++ b/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); diff --git a/test_regress/t/t_assert_implication.v b/test_regress/t/t_assert_implication.v index 4a93b6d08..1ff747a6b 100644 --- a/test_regress/t/t_assert_implication.v +++ b/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 );