diff --git a/src/V3Assert.cpp b/src/V3Assert.cpp index 3b482c427..0ccf162fa 100644 --- a/src/V3Assert.cpp +++ b/src/V3Assert.cpp @@ -253,8 +253,7 @@ class AssertVisitor final : public VNVisitor { } } AstSampled* newSampledExpr(AstNodeExpr* nodep) { - AstSampled* const sampledp = new AstSampled{nodep->fileline(), nodep}; - sampledp->dtypeFrom(nodep); + AstSampled* const sampledp = new AstSampled{nodep->fileline(), nodep, nodep->dtypep()}; return sampledp; } AstVarRef* newMonitorNumVarRefp(const AstNode* nodep, VAccess access) { diff --git a/src/V3AssertNfa.cpp b/src/V3AssertNfa.cpp index 3bfe7dfda..bf50e97a1 100644 --- a/src/V3AssertNfa.cpp +++ b/src/V3AssertNfa.cpp @@ -182,8 +182,7 @@ struct BuildResult final { }; static AstNodeExpr* sampled(AstNodeExpr* exprp) { - AstSampled* const sp = new AstSampled{exprp->fileline(), exprp}; - sp->dtypeFrom(exprp); + AstSampled* const sp = new AstSampled{exprp->fileline(), exprp, exprp->dtypep()}; return sp; } @@ -838,13 +837,14 @@ class SvaNfaBuilder final { BuildResult buildUntil(AstUntil* nodep, SvaStateVertex* entryVtxp, bool isTopLevelStep) { FileLine* const flp = nodep->fileline(); if (!isTopLevelStep) { - nodep->v3warn(E_UNSUPPORTED, "Unsupported: 'until' in complex property expression"); + nodep->v3warn(E_UNSUPPORTED, "Unsupported: '" << nodep->verilogKwd() + << "' in complex property expression"); return BuildResult::failWithError(); } if (nodep->isStrong()) { nodep->v3warn(E_UNSUPPORTED, "Unsupported: s_until" << (nodep->isOverlapping() ? "_with" : "") - << " (in property expresion)"); + << " (in property expression)"); return BuildResult::failWithError(); } AstNodeExpr* const lhsp = nodep->lhsp(); @@ -853,7 +853,8 @@ class SvaNfaBuilder final { return ep->exists([](const AstNodeExpr* np) { return np->isMultiCycleSva(); }); }; if (hasSeq(lhsp) || hasSeq(rhsp)) { - nodep->v3warn(E_UNSUPPORTED, "Unsupported: 'until' in complex property expression"); + nodep->v3warn(E_UNSUPPORTED, "Unsupported: '" << nodep->verilogKwd() + << "' in complex property expression"); return BuildResult::failWithError(); } @@ -1926,16 +1927,16 @@ class AssertNfaVisitor final : public VNVisitor { // Bare `assert property (p until q)` with boolean operands stays on // V3AssertPre's AstLoop lowering, which preserves per-attempt action-block - // firings that this NFA's single-bit aggregated state cannot. NFA still - // owns strong forms, sequence operands, and any embedding inside a - // multi-cycle context (implication consequent, or/and operands, etc.). + // firings that this NFA's single-bit aggregated state cannot. Strong bare + // forms are also lowered there. NFA still owns sequence operands and any + // embedding inside a multi-cycle context (implication consequent, or/and + // operands, etc.). static bool isBareTopLevelUntil(AstNode* propp) { AstNode* p = propp; if (AstPropSpec* const specp = VN_CAST(p, PropSpec)) p = specp->propp(); while (AstLogNot* const notp = VN_CAST(p, LogNot)) p = notp->lhsp(); AstUntil* const untilp = VN_CAST(p, Until); if (!untilp) return false; - if (untilp->isStrong()) return false; const auto hasSeq = [](const AstNodeExpr* ep) { return ep->exists([](const AstNodeExpr* np) { return np->isMultiCycleSva(); }); }; diff --git a/src/V3AssertPre.cpp b/src/V3AssertPre.cpp index 349f2df67..c61299a66 100644 --- a/src/V3AssertPre.cpp +++ b/src/V3AssertPre.cpp @@ -366,8 +366,8 @@ private: if (skewp->num().is1Step()) { // #1step means the value that is sampled is always the signal's last value // before the clock edge (IEEE 1800-2023 14.4) - AstSampled* const sampledp = new AstSampled{flp, exprp->cloneTreePure(false)}; - sampledp->dtypeFrom(exprp); + AstSampled* const sampledp + = new AstSampled{flp, exprp->cloneTreePure(false), exprp->dtypep()}; AstAssign* const assignp = new AstAssign{flp, refp, sampledp}; m_clockingp->addNextHere(new AstAlways{ flp, VAlwaysKwd::ALWAYS, @@ -413,7 +413,7 @@ private: } } void visit(AstDelay* nodep) override { - m_hasCycleDelay = true; + m_hasCycleDelay |= nodep->isCycleDelay(); // Only cycle delays are relevant in this stage; also only process once if (!nodep->isCycleDelay()) { if (m_inSynchDrive) { @@ -844,7 +844,7 @@ private: // Assertion condition check AstLoop* const loopp = new AstLoop{flp}; - AstNodeExpr* const condp = new AstSampled{flp, nodep->exprp()->unlinkFrBack()}; + AstNodeExpr* const condp = new AstSampled{flp, nodep->exprp()->unlinkFrBack(), nullptr}; loopp->addStmtsp(new AstLoopTest{flp, loopp, new AstLogNot{flp, condp}}); loopp->addStmtsp(new AstEventControl{flp, sentreep, nullptr}); @@ -1298,17 +1298,121 @@ private: } void visit(AstUntil* nodep) override { FileLine* const flp = nodep->fileline(); - if (m_pexprp) { - nodep->v3warn(E_UNSUPPORTED, "Unsupported: 'until' in complex property expression"); - nodep->replaceWith(new AstConst{flp, AstConst::BitFalse{}}); - VL_DO_DANGLING(pushDeletep(nodep), nodep); - return; - } + UASSERT_OBJ( + !m_pexprp, nodep, + "'" << nodep->verilogKwd() + << "' in complex property expression should have been rejected by V3AssertNfa"); if (nodep->isStrong()) { - nodep->v3warn(E_UNSUPPORTED, "Unsupported: s_until" - << (nodep->isOverlapping() ? "_with" : "") - << " (in property expresion)"); - nodep->replaceWith(new AstConst{flp, AstConst::BitFalse{}}); + // p s_until q / p s_until_with q: q must eventually be true. Until then, p must + // be true on every sampled tick. For s_until, check q first: when q is true on + // this tick, p is not required. For s_until_with, p must be true on the q tick too. + AstNodeExpr* const rawLhsp = nodep->lhsp()->unlinkFrBack(); + AstNodeExpr* const rawRhsp = nodep->rhsp()->unlinkFrBack(); + AstSampled* const lhsp = new AstSampled{flp, rawLhsp, rawLhsp->dtypep()}; + AstSampled* const rhsp = new AstSampled{flp, rawRhsp, rawRhsp->dtypep()}; + AstNodeExpr* finalCondp = rhsp->cloneTreePure(false); + if (nodep->isOverlapping()) { + finalCondp = new AstLogAnd{flp, lhsp->cloneTreePure(false), finalCondp}; + } + + // Track active assertion attempts. Only the count is needed to emit final failures. + AstVar* const activep = new AstVar{flp, VVarType::MODULETEMP, m_activeNames.get(""), + nodep->findBasicDType(VBasicDTypeKwd::UINT32)}; + activep->lifetime(VLifetime::STATIC_EXPLICIT); + m_modp->addStmtsp(activep); + + AstVar* const donep + = new AstVar{flp, VVarType::BLOCKTEMP, "__VassertDone", nodep->findBitDType()}; + donep->lifetime(VLifetime::AUTOMATIC_EXPLICIT); + auto setDone = [&]() { + return new AstAssign{flp, new AstVarRef{flp, donep, VAccess::WRITE}, + new AstConst{flp, AstConst::BitTrue{}}}; + }; + + AstLoop* const loopp = new AstLoop{flp}; + AstAssign* const decrementVar = new AstAssign{ + flp, new AstVarRef{flp, activep, VAccess::WRITE}, + new AstSub{flp, new AstVarRef{flp, activep, VAccess::READ}, new AstConst{flp, 1}}}; + loopp->addStmtsp(new AstLoopTest{ + flp, loopp, new AstLogNot{flp, new AstVarRef{flp, donep, VAccess::READ}}}); + { + AstBegin* const passp = new AstBegin{flp, "", nullptr, true}; + passp->addStmtsp(new AstPExprClause{flp}); + passp->addStmtsp(decrementVar); + passp->addStmtsp(setDone()); + AstNodeExpr* passCondp = rhsp; + if (nodep->isOverlapping()) { + passCondp = new AstLogAnd{flp, lhsp->cloneTreePure(false), passCondp}; + } + loopp->addStmtsp(new AstIf{flp, passCondp, passp}); + } + { + AstBegin* const failp = new AstBegin{flp, "", nullptr, true}; + failp->addStmtsp(new AstPExprClause{flp, false}); + failp->addStmtsp(decrementVar->cloneTree(false)); + failp->addStmtsp(setDone()); + loopp->addStmtsp(new AstIf{ + flp, + new AstLogAnd{flp, + new AstLogNot{flp, new AstVarRef{flp, donep, VAccess::READ}}, + new AstLogNot{flp, lhsp}}, + failp}); + } + AstDelay* const delayp = new AstDelay{flp, new AstConst{flp, 1}, false}; + delayp->timeunit(m_modp->timeunit()); + loopp->addStmtsp(new AstIf{ + flp, new AstLogNot{flp, new AstVarRef{flp, donep, VAccess::READ}}, delayp}); + + // Main assertion block + AstBegin* const bodyp = new AstBegin{flp, "", nullptr, true}; + bodyp->addStmtsp(donep); + bodyp->addStmtsp(new AstAssign{flp, new AstVarRef{flp, donep, VAccess::WRITE}, + new AstConst{flp, AstConst::BitFalse{}}}); + FileLine* const flp = activep->fileline(); + bodyp->addStmtsp( + new AstAssign{flp, new AstVarRef{flp, activep, VAccess::WRITE}, + new AstAdd{flp, new AstVarRef{flp, activep, VAccess::READ}, + new AstConst{flp, 1}}}); + bodyp->addStmtsp(loopp); + + // Validate assertion condition for each active assert + AstVar* const activeCountp = new AstVar{flp, VVarType::BLOCKTEMP, "__VassertCount", + nodep->findBasicDType(VBasicDTypeKwd::UINT32)}; + activeCountp->lifetime(VLifetime::AUTOMATIC_EXPLICIT); + + AstAssign* const initActiveCountp + = new AstAssign{flp, new AstVarRef{flp, activeCountp, VAccess::WRITE}, + new AstVarRef{flp, activep, VAccess::READ}}; + AstLoop* const finalLoopp = new AstLoop{flp}; + finalLoopp->addStmtsp( + new AstLoopTest{flp, finalLoopp, + new AstNeq{flp, new AstVarRef{flp, activeCountp, VAccess::READ}, + new AstConst{flp, 0}}}); + finalLoopp->addStmtsp(new AstIf{flp, finalCondp, new AstPExprClause{flp}, + new AstPExprClause{flp, false}}); + finalLoopp->addStmtsp( + new AstAssign{flp, new AstVarRef{flp, activeCountp, VAccess::WRITE}, + new AstSub{flp, new AstVarRef{flp, activeCountp, VAccess::READ}, + new AstConst{flp, 1}}}); + + // Final assertion block + AstBegin* const finalp = new AstBegin{flp, "", nullptr, true}; + finalp->addStmtsp(activeCountp); + finalp->addStmtsp(initActiveCountp); + finalp->addStmtsp(finalLoopp); + + AstPExpr* const pexprp = new AstPExpr{flp, bodyp, finalp, nodep->dtypep()}; + VL_RESTORER(m_pexprp); + VL_RESTORER(m_hasCycleDelay); + m_pexprp = pexprp; + m_hasCycleDelay = false; + iterate(bodyp); + iterate(finalp); + + UASSERT_OBJ(!m_hasCycleDelay, nodep, + "s_until cycle delay should have been handled by V3AssertNfa"); + + nodep->replaceWith(pexprp); VL_DO_DANGLING(pushDeletep(nodep), nodep); return; } @@ -1367,8 +1471,8 @@ private: iterateNull(nodep->disablep()); if (!VN_AS(nodep->backp(), NodeCoverOrAssert)->immediate()) { const AstNodeDType* const propDtp = nodep->propp()->dtypep(); - nodep->propp(new AstSampled{nodep->fileline(), nodep->propp()->unlinkFrBack()}); - nodep->propp()->dtypeFrom(propDtp); + nodep->propp(new AstSampled{nodep->fileline(), nodep->propp()->unlinkFrBack(), + propDtp->dtypep()}); } iterate(nodep->propp()); } diff --git a/src/V3AstNodeExpr.h b/src/V3AstNodeExpr.h index 06cda4604..41d980697 100644 --- a/src/V3AstNodeExpr.h +++ b/src/V3AstNodeExpr.h @@ -2519,9 +2519,10 @@ class AstSampled final : public AstNodeExpr { // Verilog $sampled // @astgen op1 := exprp : AstNode public: - AstSampled(FileLine* fl, AstNode* exprp) + AstSampled(FileLine* fl, AstNode* exprp, AstNodeDType* dtypep) : ASTGEN_SUPER_Sampled(fl) { this->exprp(exprp); + this->dtypep(dtypep); } ASTGEN_MEMBERS_AstSampled; string emitVerilog() override { return "$sampled(%l)"; } @@ -2906,6 +2907,9 @@ public: string emitVerilog() override { V3ERROR_NA_RETURN(""); } string emitC() override { V3ERROR_NA_RETURN(""); } string emitSimpleOperator() override { V3ERROR_NA_RETURN(""); } + string verilogKwd() const override { + return (isStrong() ? "s_" : string()) + "until" + (isOverlapping() ? "_with" : ""); + } bool cleanOut() const override { V3ERROR_NA_RETURN(""); } int instrCount() const override { return widthInstrs(); } bool sameNode(const AstNode* /*samep*/) const override { return true; } diff --git a/src/V3Slice.cpp b/src/V3Slice.cpp index 875ce7624..4331e4015 100644 --- a/src/V3Slice.cpp +++ b/src/V3Slice.cpp @@ -210,7 +210,7 @@ class SliceVisitor final : public VNVisitor { UINFO(9, " cloneSliceSel(" << elements << "," << elemIdx << ") " << nodep); AstNodeExpr* const exprp = VN_AS(snodep->exprp(), NodeExpr); AstNodeExpr* const selp = cloneAndSel(exprp, elements, elemIdx, needPure); - return new AstSampled{nodep->fileline(), selp}; + return new AstSampled{nodep->fileline(), selp, nullptr}; } else if (AstExprStmt* const snodep = VN_CAST(nodep, ExprStmt)) { UINFO(9, " cloneExprStmt(" << elements << "," << elemIdx << ") " << nodep); AstNodeExpr* const resultSelp diff --git a/src/V3Width.cpp b/src/V3Width.cpp index ff3d8431b..5a24539b2 100644 --- a/src/V3Width.cpp +++ b/src/V3Width.cpp @@ -1714,6 +1714,13 @@ class WidthVisitor final : public VNVisitor { } void visit(AstUntil* nodep) override { + if (nodep->isStrong() + && (v3Global.opt.timing().isSetFalse() || !v3Global.opt.timing().isSetTrue())) { + nodep->v3warn(E_NOTIMING, nodep->verilogKwd() << " requires --timing"); + nodep->replaceWith(new AstConst{nodep->fileline(), AstConst::BitFalse{}}); + VL_DO_DANGLING(nodep->deleteTree(), nodep); + return; + } assertAtExpr(nodep); if (m_vup->prelim()) { iterateCheckBool(nodep, "LHS", nodep->lhsp(), BOTH); diff --git a/src/verilog.y b/src/verilog.y index 829f8c4a4..441d6f3de 100644 --- a/src/verilog.y +++ b/src/verilog.y @@ -4531,7 +4531,7 @@ system_f_or_t_expr_call: // IEEE: part of system_tf_call (can be tas | yD_ROSE '(' expr ',' expr ')' { $$ = new AstRose{$1, $3, GRAMMARP->createSenTreeChanged($1, $5)}; } | yD_ROSE_GCLK '(' expr ')' { $$ = new AstRose{$1, $3, GRAMMARP->createGlobalClockSenTree($1)}; } | yD_RTOI '(' expr ')' { $$ = new AstRToIS{$1, $3}; } - | yD_SAMPLED '(' expr ')' { $$ = new AstSampled{$1, $3}; } + | yD_SAMPLED '(' expr ')' { $$ = new AstSampled{$1, $3, $3->dtypep()}; } | yD_SFORMATF '(' exprDispList ')' { $$ = new AstSFormatF{$1, AstSFormatF::ExprFormat{}, $3, 'd', false}; } | yD_SHORTREALTOBITS '(' expr ')' { $$ = new AstRealToBits{$1, $3}; UNSUPREAL($1); } | yD_SIGNED '(' expr ')' { $$ = new AstSigned{$1, $3}; } diff --git a/test_regress/t/t_notiming.out b/test_regress/t/t_notiming.out index 7d6b42ef8..9b27de641 100644 --- a/test_regress/t/t_notiming.out +++ b/test_regress/t/t_notiming.out @@ -51,4 +51,12 @@ : ... note: In instance 't' 38 | assert property (@(e) s_eventually 1'h1); | ^~~~~~~~~~~~ +%Error-NOTIMING: t/t_notiming.v:39:31: s_until requires --timing + : ... note: In instance 't' + 39 | assert property (@(e) 1'h1 s_until 1'h1); + | ^~~~~~~ +%Error-NOTIMING: t/t_notiming.v:40:31: s_until_with requires --timing + : ... note: In instance 't' + 40 | assert property (@(e) 1'h1 s_until_with 1'h1); + | ^~~~~~~~~~~~ %Error: Exiting due to diff --git a/test_regress/t/t_notiming.v b/test_regress/t/t_notiming.v index f91dd2c27..667d9b1d3 100644 --- a/test_regress/t/t_notiming.v +++ b/test_regress/t/t_notiming.v @@ -36,6 +36,8 @@ module t; s.get(); end assert property (@(e) s_eventually 1'h1); + assert property (@(e) 1'h1 s_until 1'h1); + assert property (@(e) 1'h1 s_until_with 1'h1); endmodule `ifdef VERILATOR_TIMING diff --git a/test_regress/t/t_property_sexpr_parse_unsup.out b/test_regress/t/t_property_sexpr_parse_unsup.out index f84b96594..4c8e5bba1 100644 --- a/test_regress/t/t_property_sexpr_parse_unsup.out +++ b/test_regress/t/t_property_sexpr_parse_unsup.out @@ -1,16 +1,16 @@ -%Warning-WIDTHTRUNC: t/t_property_sexpr_unsup.v:72:14: Logical operator IMPLICATION expects 1 bit on the RHS, but RHS's CMETHODHARD 'at' generates 8 bits. +%Warning-WIDTHTRUNC: t/t_property_sexpr_unsup.v:80:14: Logical operator IMPLICATION expects 1 bit on the RHS, but RHS's CMETHODHARD 'at' generates 8 bits. : ... note: In instance 't.ieee' - 72 | $rose(a) |-> q[0]; + 80 | $rose(a) |-> q[0]; | ^~~ ... For warning description see https://verilator.org/warn/WIDTHTRUNC?v=latest ... Use "/* verilator lint_off WIDTHTRUNC */" and lint_on around source to disable this message. -%Warning-WIDTHTRUNC: t/t_property_sexpr_unsup.v:77:29: Logical operator SEXPR expects 1 bit on the exprp, but exprp's CMETHODHARD 'at' generates 8 bits. +%Warning-WIDTHTRUNC: t/t_property_sexpr_unsup.v:85:29: Logical operator SEXPR expects 1 bit on the exprp, but exprp's CMETHODHARD 'at' generates 8 bits. : ... note: In instance 't.ieee' - 77 | ($rose(a), l_b = b) |-> ##[3:10] q[l_b]; + 85 | ($rose(a), l_b = b) |-> ##[3:10] q[l_b]; | ^~ -%Warning-WIDTHTRUNC: t/t_property_sexpr_unsup.v:98:31: Logical operator SEXPR expects 1 bit on the exprp, but exprp's VARREF 'b' generates 32 bits. - : ... note: In instance 't.ieee' - 98 | assert property (@clk not a ##1 b); +%Warning-WIDTHTRUNC: t/t_property_sexpr_unsup.v:106:31: Logical operator SEXPR expects 1 bit on the exprp, but exprp's VARREF 'b' generates 32 bits. + : ... note: In instance 't.ieee' + 106 | assert property (@clk not a ##1 b); | ^~ %Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:47:39: Unsupported: 'until' in complex property expression : ... note: In instance 't' @@ -21,16 +21,32 @@ : ... note: In instance 't' 49 | assert property (@(posedge clk) val until (val ##1 val)) $display("[%0t] sequence in until, fileline:%d", $time, 49); | ^~~~~ -%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:51:39: Unsupported: s_until (in property expresion) +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:51:44: Unsupported: s_until (in property expression) : ... note: In instance 't' - 51 | assert property (@(posedge clk) val s_until !val) $display("[%0t] s_until, fileline:%d", $time, 51); + 51 | assert property (@(posedge clk) ##1 (val s_until val)) $display("[%0t] s_until in sequence, fileline:%d", $time, 51); + | ^~~~~~~ +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:53:39: Unsupported: s_until (in property expression) + : ... note: In instance 't' + 53 | assert property (@(posedge clk) val s_until val s_until val) $display("[%0t] nested s_until, fileline:%d", $time, 53); | ^~~~~~~ -%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:53:39: Unsupported: s_until_with (in property expresion) +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:55:39: Unsupported: s_until (in property expression) : ... note: In instance 't' - 53 | assert property (@(posedge clk) val s_until_with val) $display("[%0t] s_until_with, fileline:%d", $time, 53); + 55 | assert property (@(posedge clk) val s_until (val ##1 val)) $display("[%0t] sequence in until_with, fileline:%d", $time, 55); + | ^~~~~~~ +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:57:44: Unsupported: s_until_with (in property expression) + : ... note: In instance 't' + 57 | assert property (@(posedge clk) ##1 (val s_until_with val)) $display("[%0t] s_until_with in sequence, fileline:%d", $time, 57); + | ^~~~~~~~~~~~ +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:59:39: Unsupported: s_until_with (in property expression) + : ... note: In instance 't' + 59 | assert property (@(posedge clk) val s_until_with val s_until_with val) $display("[%0t] nested s_until_with, fileline:%d", $time, 59); | ^~~~~~~~~~~~ -%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:55:40: Unsupported: 'until' in complex property expression +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:61:39: Unsupported: s_until_with (in property expression) : ... note: In instance 't' - 55 | assert property (@(posedge clk) (val until val) or val) $display("[%0t] until inside or, fileline:%d", $time, 55); + 61 | assert property (@(posedge clk) val s_until_with (val ##1 val)) $display("[%0t] sequence in until_with, fileline:%d", $time, 61); + | ^~~~~~~~~~~~ +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:63:40: Unsupported: 'until' in complex property expression + : ... note: In instance 't' + 63 | assert property (@(posedge clk) (val until val) or val) $display("[%0t] until inside or, fileline:%d", $time, 63); | ^~~~~ %Error: Exiting due to diff --git a/test_regress/t/t_property_sexpr_unsup.out b/test_regress/t/t_property_sexpr_unsup.out index a13d0fd31..078d116e2 100644 --- a/test_regress/t/t_property_sexpr_unsup.out +++ b/test_regress/t/t_property_sexpr_unsup.out @@ -7,16 +7,32 @@ : ... note: In instance 't' 49 | assert property (@(posedge clk) val until (val ##1 val)) $display("[%0t] sequence in until, fileline:%d", $time, 49); | ^~~~~ -%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:51:39: Unsupported: s_until (in property expresion) +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:51:44: Unsupported: s_until (in property expression) : ... note: In instance 't' - 51 | assert property (@(posedge clk) val s_until !val) $display("[%0t] s_until, fileline:%d", $time, 51); + 51 | assert property (@(posedge clk) ##1 (val s_until val)) $display("[%0t] s_until in sequence, fileline:%d", $time, 51); + | ^~~~~~~ +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:53:39: Unsupported: s_until (in property expression) + : ... note: In instance 't' + 53 | assert property (@(posedge clk) val s_until val s_until val) $display("[%0t] nested s_until, fileline:%d", $time, 53); | ^~~~~~~ -%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:53:39: Unsupported: s_until_with (in property expresion) +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:55:39: Unsupported: s_until (in property expression) : ... note: In instance 't' - 53 | assert property (@(posedge clk) val s_until_with val) $display("[%0t] s_until_with, fileline:%d", $time, 53); + 55 | assert property (@(posedge clk) val s_until (val ##1 val)) $display("[%0t] sequence in until_with, fileline:%d", $time, 55); + | ^~~~~~~ +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:57:44: Unsupported: s_until_with (in property expression) + : ... note: In instance 't' + 57 | assert property (@(posedge clk) ##1 (val s_until_with val)) $display("[%0t] s_until_with in sequence, fileline:%d", $time, 57); + | ^~~~~~~~~~~~ +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:59:39: Unsupported: s_until_with (in property expression) + : ... note: In instance 't' + 59 | assert property (@(posedge clk) val s_until_with val s_until_with val) $display("[%0t] nested s_until_with, fileline:%d", $time, 59); | ^~~~~~~~~~~~ -%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:55:40: Unsupported: 'until' in complex property expression +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:61:39: Unsupported: s_until_with (in property expression) : ... note: In instance 't' - 55 | assert property (@(posedge clk) (val until val) or val) $display("[%0t] until inside or, fileline:%d", $time, 55); + 61 | assert property (@(posedge clk) val s_until_with (val ##1 val)) $display("[%0t] sequence in until_with, fileline:%d", $time, 61); + | ^~~~~~~~~~~~ +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:63:40: Unsupported: 'until' in complex property expression + : ... note: In instance 't' + 63 | assert property (@(posedge clk) (val until val) or val) $display("[%0t] until inside or, fileline:%d", $time, 63); | ^~~~~ %Error: Exiting due to diff --git a/test_regress/t/t_property_sexpr_unsup.v b/test_regress/t/t_property_sexpr_unsup.v index d6a5b4aca..9fedd15b8 100644 --- a/test_regress/t/t_property_sexpr_unsup.v +++ b/test_regress/t/t_property_sexpr_unsup.v @@ -48,9 +48,17 @@ module t ( /*AUTOARG*/ assert property (@(posedge clk) val until (val ##1 val)) $display("[%0t] sequence in until, fileline:%d", $time, `__LINE__); - assert property (@(posedge clk) val s_until !val) $display("[%0t] s_until, fileline:%d", $time, `__LINE__); + assert property (@(posedge clk) ##1 (val s_until val)) $display("[%0t] s_until in sequence, fileline:%d", $time, `__LINE__); - assert property (@(posedge clk) val s_until_with val) $display("[%0t] s_until_with, fileline:%d", $time, `__LINE__); + assert property (@(posedge clk) val s_until val s_until val) $display("[%0t] nested s_until, fileline:%d", $time, `__LINE__); + + assert property (@(posedge clk) val s_until (val ##1 val)) $display("[%0t] sequence in until_with, fileline:%d", $time, `__LINE__); + + assert property (@(posedge clk) ##1 (val s_until_with val)) $display("[%0t] s_until_with in sequence, fileline:%d", $time, `__LINE__); + + assert property (@(posedge clk) val s_until_with val s_until_with val) $display("[%0t] nested s_until_with, fileline:%d", $time, `__LINE__); + + assert property (@(posedge clk) val s_until_with (val ##1 val)) $display("[%0t] sequence in until_with, fileline:%d", $time, `__LINE__); assert property (@(posedge clk) (val until val) or val) $display("[%0t] until inside or, fileline:%d", $time, `__LINE__); diff --git a/test_regress/t/t_property_until.v b/test_regress/t/t_property_until.v index 137c9417c..1223cb37c 100644 --- a/test_regress/t/t_property_until.v +++ b/test_regress/t/t_property_until.v @@ -46,6 +46,40 @@ module t ( /*AUTOARG*/ results[5].passs++; else results[5].fails++; + assert property (@(posedge clk) 0 s_until 1) + results[6].passs++; + else results[6].fails++; + + assert property (@(posedge clk) cyc < 5 s_until cyc >= 5) + results[7].passs++; + else results[7].fails++; + + assert property (@(posedge clk) cyc % 3 == 0 s_until cyc % 5 == 0) + results[8].passs++; + else results[8].fails++; + + // Check that s_until accepts immediately when RHS is true, even if LHS is false. + assert property (@(posedge clk) cyc % 2 == 0 s_until 1) + results[9].passs++; + else results[9].fails++; + + // Check that s_until_with requires LHS when RHS is true on the same tick. + assert property (@(posedge clk) 0 s_until_with 1) + results[10].passs++; + else results[10].fails++; + + assert property (@(posedge clk) 1 s_until_with cyc >= 5) + results[11].passs++; + else results[11].fails++; + + assert property (@(posedge clk) cyc <= 5 s_until_with cyc >= 5) + results[12].passs++; + else results[12].fails++; + + assert property (@(posedge clk) cyc < 5 s_until_with cyc >= 5) + results[13].passs++; + else results[13].fails++; + always @(edge clk) begin ++cyc; if (cyc == MAX) begin @@ -54,6 +88,14 @@ module t ( /*AUTOARG*/ expected[3] = '{0, 7}; expected[4] = '{5, 2}; expected[5] = '{2, 5}; + expected[6] = '{0, 7}; + expected[7] = '{0, 7}; + expected[8] = '{5, 2}; + expected[9] = '{0, 7}; + expected[10] = '{7, 0}; + expected[11] = '{0, 7}; + expected[12] = '{4, 3}; + expected[13] = '{7, 0}; `checkh(results, expected); $write("*-* All Finished *-*\n"); $finish; diff --git a/test_regress/t/t_timing_unset1.out b/test_regress/t/t_timing_unset1.out index 79ef98aee..cb0cc5420 100644 --- a/test_regress/t/t_timing_unset1.out +++ b/test_regress/t/t_timing_unset1.out @@ -52,4 +52,12 @@ 38 | assert property (@(e) s_eventually 1'h1); | ^~~~~~~~~~~~ ... For error description see https://verilator.org/warn/NOTIMING?v=latest +%Error-NOTIMING: t/t_notiming.v:39:31: s_until requires --timing + : ... note: In instance 't' + 39 | assert property (@(e) 1'h1 s_until 1'h1); + | ^~~~~~~ +%Error-NOTIMING: t/t_notiming.v:40:31: s_until_with requires --timing + : ... note: In instance 't' + 40 | assert property (@(e) 1'h1 s_until_with 1'h1); + | ^~~~~~~~~~~~ %Error: Exiting due to