From 4da31b0418d248bc8f2f9ce3de8adb877dd7a4a0 Mon Sep 17 00:00:00 2001 From: Ryszard Rozak Date: Fri, 10 Apr 2026 14:17:54 +0200 Subject: [PATCH] Support 'until' property (partial #7290) (#7399) --- src/V3AssertPre.cpp | 42 +++++- src/V3AstNodeExpr.h | 18 +++ src/V3Width.cpp | 9 ++ src/verilog.y | 2 +- test_regress/t/t_property_pexpr_unsup.out | 121 +++++++++--------- test_regress/t/t_property_pexpr_unsup.v | 4 - .../t/t_property_sexpr_parse_unsup.out | 16 +-- test_regress/t/t_property_sexpr_unsup.out | 12 ++ test_regress/t/t_property_sexpr_unsup.v | 6 + test_regress/t/t_property_unsup.out | 100 +++++++-------- test_regress/t/t_property_unsup.v | 4 - test_regress/t/t_property_until.py | 18 +++ test_regress/t/t_property_until.v | 57 +++++++++ 13 files changed, 269 insertions(+), 140 deletions(-) create mode 100755 test_regress/t/t_property_until.py create mode 100644 test_regress/t/t_property_until.v diff --git a/src/V3AssertPre.cpp b/src/V3AssertPre.cpp index fe1b58a79..765e4ec9b 100644 --- a/src/V3AssertPre.cpp +++ b/src/V3AssertPre.cpp @@ -41,6 +41,7 @@ class AssertPreVisitor final : public VNVisitor { private: // NODE STATE // AstClockingItem::user1p() // AstVar*. varp() of ClockingItem after unlink + // AstPExpr::user1() // bool. Created from AstUntil const VNUser1InUse m_inuser1; // STATE // Current context: @@ -58,6 +59,7 @@ private: // Reset each assertion: AstNodeExpr* m_disablep = nullptr; // Last disable AstIf* m_disableSeqIfp = nullptr; // Used for handling disable iff in sequences + AstPExpr* m_pexprp = nullptr; // Last AstPExpr // Other: V3UniqueNames m_cycleDlyNames{"__VcycleDly"}; // Cycle delay counter name generator V3UniqueNames m_consRepNames{"__VconsRep"}; // Consecutive repetition counter name generator @@ -69,7 +71,6 @@ private: bool m_inAssignDlyLhs = false; // True if in AssignDly's LHS bool m_inSynchDrive = false; // True if in synchronous drive std::vector m_xrefsp; // list of xrefs that need name fixup - bool m_inPExpr = false; // True if in AstPExpr std::vector m_seqsToCleanup; // Sequences to clean up after traversal // METHODS @@ -430,7 +431,7 @@ private: VL_DO_DANGLING(pushDeletep(nodep->unlinkFrBack()), nodep); return; } - if (m_inPExpr) { + if (m_pexprp) { // ##0 in sequence context = zero delay = same clock tick VL_DO_DANGLING(pushDeletep(nodep->unlinkFrBack()), nodep); return; @@ -461,7 +462,7 @@ private: } AstSenItem* sensesp = nullptr; if (!m_defaultClockingp) { - if (!m_inPExpr) { + if (!m_pexprp) { nodep->v3error("Usage of cycle delays requires default clocking" " (IEEE 1800-2023 14.11)"); VL_DO_DANGLING(nodep->unlinkFrBack()->deleteTree(), nodep); @@ -1139,6 +1140,30 @@ private: } VL_DO_DANGLING(pushDeletep(nodep), nodep); } + 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; + } + AstLoop* const loopp = new AstLoop{flp}; + AstNodeExpr* const rhsp = nodep->rhsp()->unlinkFrBack(); + AstLogAnd* const condp + = new AstLogAnd{flp, nodep->lhsp()->unlinkFrBack(), new AstLogNot{flp, rhsp}}; + loopp->addStmtsp(new AstLoopTest{flp, loopp, condp}); + loopp->addStmtsp(new AstEventControl{flp, newSenTree(nodep), nullptr}); + + AstBegin* const beginp = new AstBegin{flp, "", loopp, true}; + beginp->addStmtsp(new AstIf{flp, rhsp->cloneTreePure(false), new AstPExprClause{flp}, + new AstPExprClause{flp, false}}); + + AstPExpr* const pexprp = new AstPExpr{flp, beginp, nodep->dtypep()}; + pexprp->user1(1); + nodep->replaceWith(pexprp); + VL_DO_DANGLING(pushDeletep(nodep), nodep); + } void visit(AstDefaultDisable* nodep) override { // Done with these @@ -1175,6 +1200,13 @@ private: iterate(nodep->propp()); } void visit(AstPExpr* nodep) override { + if (m_pexprp && m_pexprp->user1()) { + nodep->v3warn(E_UNSUPPORTED, + "Unsupported: Complex property expression inside 'until''"); + nodep->replaceWith(new AstConst{nodep->fileline(), AstConst::BitFalse{}}); + VL_DO_DANGLING(pushDeletep(nodep), nodep); + return; + } if (AstLogNot* const notp = VN_CAST(nodep->backp(), LogNot)) { notp->replaceWith(nodep->unlinkFrBack()); VL_DO_DANGLING(pushDeletep(notp), notp); @@ -1191,9 +1223,9 @@ private: return; } } - VL_RESTORER(m_inPExpr); + VL_RESTORER(m_pexprp); VL_RESTORER(m_disableSeqIfp); - m_inPExpr = true; + m_pexprp = nodep; if (m_disablep) { const AstSampled* sampledp; diff --git a/src/V3AstNodeExpr.h b/src/V3AstNodeExpr.h index 058291d74..886fa4d7a 100644 --- a/src/V3AstNodeExpr.h +++ b/src/V3AstNodeExpr.h @@ -2733,6 +2733,24 @@ public: string emitC() override { V3ERROR_NA_RETURN(""); } bool cleanOut() const override { V3ERROR_NA_RETURN(true); } }; +class AstUntil final : public AstNodeExpr { + // The until property expression + // @astgen op1 := lhsp : AstNodeExpr + // @astgen op2 := rhsp : AstNodeExpr +public: + AstUntil(FileLine* fl, AstNodeExpr* lhsp, AstNodeExpr* rhsp) + : ASTGEN_SUPER_Until(fl) { + this->lhsp(lhsp); + this->rhsp(rhsp); + } + ASTGEN_MEMBERS_AstUntil; + string emitVerilog() override { V3ERROR_NA_RETURN(""); } + string emitC() override { V3ERROR_NA_RETURN(""); } + string emitSimpleOperator() override { V3ERROR_NA_RETURN(""); } + bool cleanOut() const override { V3ERROR_NA_RETURN(""); } + int instrCount() const override { return widthInstrs(); } + bool sameNode(const AstNode* /*samep*/) const override { return true; } +}; class AstValuePlusArgs final : public AstNodeExpr { // Search expression. If nullptr then this is a $test$plusargs instead of $value$plusargs. // @astgen op1 := searchp : Optional[AstNodeExpr] diff --git a/src/V3Width.cpp b/src/V3Width.cpp index 234df1d28..b9b0eb0c6 100644 --- a/src/V3Width.cpp +++ b/src/V3Width.cpp @@ -1647,6 +1647,15 @@ class WidthVisitor final : public VNVisitor { } } + void visit(AstUntil* nodep) override { + assertAtExpr(nodep); + if (m_vup->prelim()) { + iterateCheckBool(nodep, "LHS", nodep->lhsp(), BOTH); + iterateCheckBool(nodep, "RHS", nodep->rhsp(), BOTH); + nodep->dtypeSetBit(); + } + } + void visit(AstRand* nodep) override { assertAtExpr(nodep); if (m_vup->prelim()) { diff --git a/src/verilog.y b/src/verilog.y index ab951ebd5..437921dbe 100644 --- a/src/verilog.y +++ b/src/verilog.y @@ -6759,7 +6759,7 @@ pexpr: // IEEE: property_expr (The name pexpr is important as regex | yEVENTUALLY anyrange pexpr %prec yS_EVENTUALLY { $$ = $3; BBUNSUP($1, "Unsupported: eventually[] (in property expression)"); DEL($2); } | ~o~pexpr yUNTIL pexpr - { $$ = $1; BBUNSUP($2, "Unsupported: until (in property expression)"); DEL($3); } + { $$ = new AstUntil{$2, $1, $3}; } | ~o~pexpr yS_UNTIL pexpr { $$ = $1; BBUNSUP($2, "Unsupported: s_until (in property expression)"); DEL($3); } | ~o~pexpr yUNTIL_WITH pexpr diff --git a/test_regress/t/t_property_pexpr_unsup.out b/test_regress/t/t_property_pexpr_unsup.out index 72bf6e6d1..2e6a3696a 100644 --- a/test_regress/t/t_property_pexpr_unsup.out +++ b/test_regress/t/t_property_pexpr_unsup.out @@ -5,41 +5,44 @@ %Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:27:9: Unsupported: weak (in property expression) 27 | weak(a); | ^ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:31:7: Unsupported: until (in property expression) - 31 | a until b; - | ^~~~~ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:35:7: Unsupported: s_until (in property expression) - 35 | a s_until b; +%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:31:7: Unsupported: s_until (in property expression) + 31 | a s_until b; | ^~~~~~~ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:39:7: Unsupported: until_with (in property expression) - 39 | a until_with b; +%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:35:7: Unsupported: until_with (in property expression) + 35 | a until_with b; | ^~~~~~~~~~ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:43:7: Unsupported: s_until_with (in property expression) - 43 | a s_until_with b; +%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:39:7: Unsupported: s_until_with (in property expression) + 39 | a s_until_with b; | ^~~~~~~~~~~~ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:47:7: Unsupported: #-# (in property expression) - 47 | a #-# b; +%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:43:7: Unsupported: #-# (in property expression) + 43 | a #-# b; | ^~~ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:51:7: Unsupported: #=# (in property expression) - 51 | a #=# b; +%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:47:7: Unsupported: #=# (in property expression) + 47 | a #=# b; | ^~~ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:55:5: Unsupported: nexttime (in property expression) - 55 | nexttime a; +%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:51:5: Unsupported: nexttime (in property expression) + 51 | nexttime a; | ^~~~~~~~ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:59:5: Unsupported: nexttime[] (in property expression) - 59 | nexttime [2] a; +%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:55:5: Unsupported: nexttime[] (in property expression) + 55 | nexttime [2] a; | ^~~~~~~~ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:63:5: Unsupported: s_nexttime (in property expression) - 63 | s_nexttime a; +%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:59:5: Unsupported: s_nexttime (in property expression) + 59 | s_nexttime a; | ^~~~~~~~~~ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:67:5: Unsupported: s_nexttime[] (in property expression) - 67 | s_nexttime [2] a; +%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:63:5: Unsupported: s_nexttime[] (in property expression) + 63 | s_nexttime [2] a; | ^~~~~~~~~~ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:71:14: Unsupported: always (in property expression) - 71 | nexttime always a; +%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:67:14: Unsupported: always (in property expression) + 67 | nexttime always a; | ^~~~~~ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:71:5: Unsupported: nexttime (in property expression) - 71 | nexttime always a; +%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:67:5: Unsupported: nexttime (in property expression) + 67 | nexttime always a; + | ^~~~~~~~ +%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:71:18: Unsupported: always (in property expression) + 71 | nexttime [2] always a; + | ^~~~~~ +%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:71:5: Unsupported: nexttime[] (in property expression) + 71 | nexttime [2] always a; | ^~~~~~~~ %Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:75:18: Unsupported: always (in property expression) 75 | nexttime [2] always a; @@ -47,55 +50,49 @@ %Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:75:5: Unsupported: nexttime[] (in property expression) 75 | nexttime [2] always a; | ^~~~~~~~ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:79:18: Unsupported: always (in property expression) - 79 | nexttime [2] always a; - | ^~~~~~ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:79:5: Unsupported: nexttime[] (in property expression) - 79 | nexttime [2] always a; +%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:79:14: Unsupported: s_eventually (in property expression) + 79 | nexttime s_eventually a; + | ^~~~~~~~~~~~ +%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:79:5: Unsupported: nexttime (in property expression) + 79 | nexttime s_eventually a; | ^~~~~~~~ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:83:14: Unsupported: s_eventually (in property expression) - 83 | nexttime s_eventually a; +%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:83:33: Unsupported: always (in property expression) + 83 | nexttime s_eventually [2:$] always a; + | ^~~~~~ +%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:83:14: Unsupported: s_eventually[] (in property expression) + 83 | nexttime s_eventually [2:$] always a; | ^~~~~~~~~~~~ %Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:83:5: Unsupported: nexttime (in property expression) - 83 | nexttime s_eventually a; + 83 | nexttime s_eventually [2:$] always a; | ^~~~~~~~ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:87:33: Unsupported: always (in property expression) - 87 | nexttime s_eventually [2:$] always a; - | ^~~~~~ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:87:14: Unsupported: s_eventually[] (in property expression) - 87 | nexttime s_eventually [2:$] always a; - | ^~~~~~~~~~~~ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:87:5: Unsupported: nexttime (in property expression) - 87 | nexttime s_eventually [2:$] always a; - | ^~~~~~~~ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:91:15: Unsupported: accept_on (in property expression) - 91 | accept_on (a) b; +%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:87:15: Unsupported: accept_on (in property expression) + 87 | accept_on (a) b; | ^ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:95:20: Unsupported: sync_accept_on (in property expression) - 95 | sync_accept_on (a) b; +%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:91:20: Unsupported: sync_accept_on (in property expression) + 91 | sync_accept_on (a) b; | ^ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:99:15: Unsupported: reject_on (in property expression) - 99 | reject_on (a) b; +%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:95:15: Unsupported: reject_on (in property expression) + 95 | reject_on (a) b; | ^ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:103:20: Unsupported: sync_reject_on (in property expression) - 103 | sync_reject_on (a) b; +%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:99:20: Unsupported: sync_reject_on (in property expression) + 99 | sync_reject_on (a) b; | ^ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:106:26: Unsupported: property argument data type - 106 | property p_arg_propery(property inprop); +%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:102:26: Unsupported: property argument data type + 102 | property p_arg_propery(property inprop); | ^~~~~~~~ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:109:26: Unsupported: sequence argument data type - 109 | property p_arg_seqence(sequence inseq); +%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:105:26: Unsupported: sequence argument data type + 105 | property p_arg_seqence(sequence inseq); | ^~~~~~~~ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:114:5: Unsupported: property case expression - 114 | case (a) endcase +%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:110:5: Unsupported: property case expression + 110 | case (a) endcase | ^~~~ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:117:5: Unsupported: property case expression - 117 | case (a) default: b; endcase +%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:113:5: Unsupported: property case expression + 113 | case (a) default: b; endcase | ^~~~ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:120:5: Unsupported: property case expression - 120 | if (a) b +%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:116:5: Unsupported: property case expression + 116 | if (a) b | ^~ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:123:5: Unsupported: property case expression - 123 | if (a) b else c +%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:119:5: Unsupported: property case expression + 119 | if (a) b else c | ^~ %Error: Exiting due to diff --git a/test_regress/t/t_property_pexpr_unsup.v b/test_regress/t/t_property_pexpr_unsup.v index 2acbb3b40..5f7ff5e79 100644 --- a/test_regress/t/t_property_pexpr_unsup.v +++ b/test_regress/t/t_property_pexpr_unsup.v @@ -27,10 +27,6 @@ module t ( weak(a); endproperty - property p_until; - a until b; - endproperty - property p_suntil; a s_until b; endproperty diff --git a/test_regress/t/t_property_sexpr_parse_unsup.out b/test_regress/t/t_property_sexpr_parse_unsup.out index 3aeefadd4..aeec3a4f3 100644 --- a/test_regress/t/t_property_sexpr_parse_unsup.out +++ b/test_regress/t/t_property_sexpr_parse_unsup.out @@ -1,19 +1,19 @@ -%Warning-WIDTHTRUNC: t/t_property_sexpr_unsup.v:60: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:66:14: Logical operator IMPLICATION expects 1 bit on the RHS, but RHS's CMETHODHARD 'at' generates 8 bits. : ... note: In instance 't.ieee' - 60 | $rose(a) |-> q[0]; + 66 | $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:65: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:71:29: Logical operator SEXPR expects 1 bit on the exprp, but exprp's CMETHODHARD 'at' generates 8 bits. : ... note: In instance 't.ieee' - 65 | ($rose(a), l_b = b) |-> ##[3:10] q[l_b]; + 71 | ($rose(a), l_b = b) |-> ##[3:10] q[l_b]; | ^~ -%Warning-WIDTHTRUNC: t/t_property_sexpr_unsup.v:86:31: Logical operator SEXPR expects 1 bit on the exprp, but exprp's VARREF 'b' generates 32 bits. +%Warning-WIDTHTRUNC: t/t_property_sexpr_unsup.v:92:31: Logical operator SEXPR expects 1 bit on the exprp, but exprp's VARREF 'b' generates 32 bits. : ... note: In instance 't.ieee' - 86 | assert property (@clk not a ##1 b); + 92 | assert property (@clk not a ##1 b); | ^~ -%Error: Internal Error: t/t_property_sexpr_unsup.v:65:29: ../V3AssertProp.cpp:#: Range delay SExpr without clocking event +%Error: Internal Error: t/t_property_sexpr_unsup.v:71:29: ../V3AssertProp.cpp:#: Range delay SExpr without clocking event : ... note: In instance 't.ieee' - 65 | ($rose(a), l_b = b) |-> ##[3:10] q[l_b]; + 71 | ($rose(a), l_b = b) |-> ##[3:10] q[l_b]; | ^~ ... See the manual at https://verilator.org/verilator_doc.html?v=latest for more assistance. diff --git a/test_regress/t/t_property_sexpr_unsup.out b/test_regress/t/t_property_sexpr_unsup.out index d442825fa..ea5a9e088 100644 --- a/test_regress/t/t_property_sexpr_unsup.out +++ b/test_regress/t/t_property_sexpr_unsup.out @@ -23,4 +23,16 @@ : ... note: In instance 't' 43 | assert property (@(posedge clk) (##1 val) |-> (##1 val)) $display("[%0t] two delays implication stmt, fileline:%d", $time, 43); | ^~~ +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:45:44: Unsupported: 'until' in complex property expression + : ... note: In instance 't' + 45 | assert property (@(posedge clk) ##1 (val until val)) $display("[%0t] until in sequence, fileline:%d", $time, 45); + | ^~~~~ +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:47:49: Unsupported: 'until' in complex property expression + : ... note: In instance 't' + 47 | assert property (@(posedge clk) val until val until val) $display("[%0t] nested until, fileline:%d", $time, 47); + | ^~~~~ +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:49:50: Unsupported: Complex property expression inside 'until'' + : ... note: In instance 't' + 49 | assert property (@(posedge clk) val until (val ##1 val)) $display("[%0t] sequence in until, fileline:%d", $time, 49); + | ^~ %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 a424d576d..cbbe9748f 100644 --- a/test_regress/t/t_property_sexpr_unsup.v +++ b/test_regress/t/t_property_sexpr_unsup.v @@ -42,6 +42,12 @@ module t ( /*AUTOARG*/ assert property (@(posedge clk) (##1 val) |-> (##1 val)) $display("[%0t] two delays implication stmt, fileline:%d", $time, `__LINE__); + assert property (@(posedge clk) ##1 (val until val)) $display("[%0t] until in sequence, fileline:%d", $time, `__LINE__); + + assert property (@(posedge clk) val until val until val) $display("[%0t] nested until, fileline:%d", $time, `__LINE__); + + assert property (@(posedge clk) val until (val ##1 val)) $display("[%0t] sequence in until, fileline:%d", $time, `__LINE__); + property prop_implication; ##1 cyc == 4 |-> 1; endproperty diff --git a/test_regress/t/t_property_unsup.out b/test_regress/t/t_property_unsup.out index 0be572e64..809ec67ee 100644 --- a/test_regress/t/t_property_unsup.out +++ b/test_regress/t/t_property_unsup.out @@ -29,82 +29,70 @@ %Error-UNSUPPORTED: t/t_property_unsup.v:96:46: Unsupported: s_eventually (in property expression) 96 | assert property ((s_eventually a) implies (s_eventually a)); | ^~~~~~~~~~~~ -%Error-UNSUPPORTED: t/t_property_unsup.v:98:23: Unsupported: until (in property expression) - 98 | assert property ((a until b) implies (a until b)); - | ^~~~~ -%Error-UNSUPPORTED: t/t_property_unsup.v:98:43: Unsupported: until (in property expression) - 98 | assert property ((a until b) implies (a until b)); - | ^~~~~ -%Error-UNSUPPORTED: t/t_property_unsup.v:100:23: Unsupported: s_until (in property expression) - 100 | assert property ((a s_until b) implies (a s_until b)); +%Error-UNSUPPORTED: t/t_property_unsup.v:98:23: Unsupported: s_until (in property expression) + 98 | assert property ((a s_until b) implies (a s_until b)); | ^~~~~~~ -%Error-UNSUPPORTED: t/t_property_unsup.v:100:45: Unsupported: s_until (in property expression) - 100 | assert property ((a s_until b) implies (a s_until b)); +%Error-UNSUPPORTED: t/t_property_unsup.v:98:45: Unsupported: s_until (in property expression) + 98 | assert property ((a s_until b) implies (a s_until b)); | ^~~~~~~ -%Error-UNSUPPORTED: t/t_property_unsup.v:102:23: Unsupported: until_with (in property expression) - 102 | assert property ((a until_with b) implies (a until_with b)); +%Error-UNSUPPORTED: t/t_property_unsup.v:100:23: Unsupported: until_with (in property expression) + 100 | assert property ((a until_with b) implies (a until_with b)); | ^~~~~~~~~~ -%Error-UNSUPPORTED: t/t_property_unsup.v:102:48: Unsupported: until_with (in property expression) - 102 | assert property ((a until_with b) implies (a until_with b)); +%Error-UNSUPPORTED: t/t_property_unsup.v:100:48: Unsupported: until_with (in property expression) + 100 | assert property ((a until_with b) implies (a until_with b)); | ^~~~~~~~~~ -%Error-UNSUPPORTED: t/t_property_unsup.v:104:23: Unsupported: s_until_with (in property expression) - 104 | assert property ((a s_until_with b) implies (a s_until_with b)); +%Error-UNSUPPORTED: t/t_property_unsup.v:102:23: Unsupported: s_until_with (in property expression) + 102 | assert property ((a s_until_with b) implies (a s_until_with b)); | ^~~~~~~~~~~~ -%Error-UNSUPPORTED: t/t_property_unsup.v:104:50: Unsupported: s_until_with (in property expression) - 104 | assert property ((a s_until_with b) implies (a s_until_with b)); +%Error-UNSUPPORTED: t/t_property_unsup.v:102:50: Unsupported: s_until_with (in property expression) + 102 | assert property ((a s_until_with b) implies (a s_until_with b)); | ^~~~~~~~~~~~ -%Error-UNSUPPORTED: t/t_property_unsup.v:108:23: Unsupported: #-# (in property expression) - 108 | assert property ((a #-# b) implies (a #-# b)); +%Error-UNSUPPORTED: t/t_property_unsup.v:106:23: Unsupported: #-# (in property expression) + 106 | assert property ((a #-# b) implies (a #-# b)); | ^~~ -%Error-UNSUPPORTED: t/t_property_unsup.v:108:41: Unsupported: #-# (in property expression) - 108 | assert property ((a #-# b) implies (a #-# b)); +%Error-UNSUPPORTED: t/t_property_unsup.v:106:41: Unsupported: #-# (in property expression) + 106 | assert property ((a #-# b) implies (a #-# b)); | ^~~ -%Error-UNSUPPORTED: t/t_property_unsup.v:118:21: Unsupported: always (in property expression) - 118 | assert property ((always a) iff (always a)); +%Error-UNSUPPORTED: t/t_property_unsup.v:116:21: Unsupported: always (in property expression) + 116 | assert property ((always a) iff (always a)); | ^~~~~~ -%Error-UNSUPPORTED: t/t_property_unsup.v:118:36: Unsupported: always (in property expression) - 118 | assert property ((always a) iff (always a)); +%Error-UNSUPPORTED: t/t_property_unsup.v:116:36: Unsupported: always (in property expression) + 116 | assert property ((always a) iff (always a)); | ^~~~~~ -%Error-UNSUPPORTED: t/t_property_unsup.v:120:21: Unsupported: eventually[] (in property expression) - 120 | assert property ((eventually[0: 1] a) iff (eventually[0: 1] a)); +%Error-UNSUPPORTED: t/t_property_unsup.v:118:21: Unsupported: eventually[] (in property expression) + 118 | assert property ((eventually[0: 1] a) iff (eventually[0: 1] a)); | ^~~~~~~~~~ -%Error-UNSUPPORTED: t/t_property_unsup.v:120:46: Unsupported: eventually[] (in property expression) - 120 | assert property ((eventually[0: 1] a) iff (eventually[0: 1] a)); +%Error-UNSUPPORTED: t/t_property_unsup.v:118:46: Unsupported: eventually[] (in property expression) + 118 | assert property ((eventually[0: 1] a) iff (eventually[0: 1] a)); | ^~~~~~~~~~ -%Error-UNSUPPORTED: t/t_property_unsup.v:122:21: Unsupported: s_eventually (in property expression) - 122 | assert property ((s_eventually a) iff (s_eventually a)); +%Error-UNSUPPORTED: t/t_property_unsup.v:120:21: Unsupported: s_eventually (in property expression) + 120 | assert property ((s_eventually a) iff (s_eventually a)); | ^~~~~~~~~~~~ -%Error-UNSUPPORTED: t/t_property_unsup.v:122:42: Unsupported: s_eventually (in property expression) - 122 | assert property ((s_eventually a) iff (s_eventually a)); +%Error-UNSUPPORTED: t/t_property_unsup.v:120:42: Unsupported: s_eventually (in property expression) + 120 | assert property ((s_eventually a) iff (s_eventually a)); | ^~~~~~~~~~~~ -%Error-UNSUPPORTED: t/t_property_unsup.v:124:23: Unsupported: until (in property expression) - 124 | assert property ((a until b) iff (a until b)); - | ^~~~~ -%Error-UNSUPPORTED: t/t_property_unsup.v:124:39: Unsupported: until (in property expression) - 124 | assert property ((a until b) iff (a until b)); - | ^~~~~ -%Error-UNSUPPORTED: t/t_property_unsup.v:126:23: Unsupported: s_until (in property expression) - 126 | assert property ((a s_until b) iff (a s_until b)); +%Error-UNSUPPORTED: t/t_property_unsup.v:122:23: Unsupported: s_until (in property expression) + 122 | assert property ((a s_until b) iff (a s_until b)); | ^~~~~~~ -%Error-UNSUPPORTED: t/t_property_unsup.v:126:41: Unsupported: s_until (in property expression) - 126 | assert property ((a s_until b) iff (a s_until b)); +%Error-UNSUPPORTED: t/t_property_unsup.v:122:41: Unsupported: s_until (in property expression) + 122 | assert property ((a s_until b) iff (a s_until b)); | ^~~~~~~ -%Error-UNSUPPORTED: t/t_property_unsup.v:128:23: Unsupported: until_with (in property expression) - 128 | assert property ((a until_with b) iff (a until_with b)); +%Error-UNSUPPORTED: t/t_property_unsup.v:124:23: Unsupported: until_with (in property expression) + 124 | assert property ((a until_with b) iff (a until_with b)); | ^~~~~~~~~~ -%Error-UNSUPPORTED: t/t_property_unsup.v:128:44: Unsupported: until_with (in property expression) - 128 | assert property ((a until_with b) iff (a until_with b)); +%Error-UNSUPPORTED: t/t_property_unsup.v:124:44: Unsupported: until_with (in property expression) + 124 | assert property ((a until_with b) iff (a until_with b)); | ^~~~~~~~~~ -%Error-UNSUPPORTED: t/t_property_unsup.v:130:23: Unsupported: s_until_with (in property expression) - 130 | assert property ((a s_until_with b) iff (a s_until_with b)); +%Error-UNSUPPORTED: t/t_property_unsup.v:126:23: Unsupported: s_until_with (in property expression) + 126 | assert property ((a s_until_with b) iff (a s_until_with b)); | ^~~~~~~~~~~~ -%Error-UNSUPPORTED: t/t_property_unsup.v:130:46: Unsupported: s_until_with (in property expression) - 130 | assert property ((a s_until_with b) iff (a s_until_with b)); +%Error-UNSUPPORTED: t/t_property_unsup.v:126:46: Unsupported: s_until_with (in property expression) + 126 | assert property ((a s_until_with b) iff (a s_until_with b)); | ^~~~~~~~~~~~ -%Error-UNSUPPORTED: t/t_property_unsup.v:134:23: Unsupported: #-# (in property expression) - 134 | assert property ((a #-# b) iff (a #-# b)); +%Error-UNSUPPORTED: t/t_property_unsup.v:130:23: Unsupported: #-# (in property expression) + 130 | assert property ((a #-# b) iff (a #-# b)); | ^~~ -%Error-UNSUPPORTED: t/t_property_unsup.v:134:37: Unsupported: #-# (in property expression) - 134 | assert property ((a #-# b) iff (a #-# b)); +%Error-UNSUPPORTED: t/t_property_unsup.v:130:37: Unsupported: #-# (in property expression) + 130 | assert property ((a #-# b) iff (a #-# b)); | ^~~ %Error: Exiting due to diff --git a/test_regress/t/t_property_unsup.v b/test_regress/t/t_property_unsup.v index 49cfbedcd..e496b28c9 100644 --- a/test_regress/t/t_property_unsup.v +++ b/test_regress/t/t_property_unsup.v @@ -94,8 +94,6 @@ module sva_implies2 ( assert property ((eventually[0: 1] a) implies (eventually[0: 1] a)); p3 : assert property ((s_eventually a) implies (s_eventually a)); - p4 : - assert property ((a until b) implies (a until b)); p5 : assert property ((a s_until b) implies (a s_until b)); p6 : @@ -120,8 +118,6 @@ module sva_iff2 ( assert property ((eventually[0: 1] a) iff (eventually[0: 1] a)); p2 : assert property ((s_eventually a) iff (s_eventually a)); - p3 : - assert property ((a until b) iff (a until b)); p4 : assert property ((a s_until b) iff (a s_until b)); p5 : diff --git a/test_regress/t/t_property_until.py b/test_regress/t/t_property_until.py new file mode 100755 index 000000000..35e44000c --- /dev/null +++ b/test_regress/t/t_property_until.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(timing_loop=True, verilator_flags2=['--assert', '--timing']) + +test.execute() + +test.passes() diff --git a/test_regress/t/t_property_until.v b/test_regress/t/t_property_until.v new file mode 100644 index 000000000..b72706982 --- /dev/null +++ b/test_regress/t/t_property_until.v @@ -0,0 +1,57 @@ +// 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 + +`define stop $stop +`define checkh(gotv, + expv) do if ((gotv) !== (expv)) begin $write("%%Error: %s:%0d: got='h%p exp='h%p\n", `__FILE__,`__LINE__, (gotv), (expv)); `stop; end while(0) + +module t ( /*AUTOARG*/ + // Inputs + clk +); + + input clk; + + typedef struct { + int fails; + int passs; + } result_t; + + result_t results[int]; + result_t expected[int]; + + localparam MAX = 15; + integer cyc = 0; + + assert property (@(posedge clk) 0 until 1) + results[1].passs++; + else results[1].fails++; + + assert property (@(posedge clk) 1 until 0) + results[2].passs++; + else results[2].fails++; + + assert property (@(posedge clk) cyc < 5 until cyc >= 5) + results[3].passs++; + else results[3].fails++; + + assert property (@(posedge clk) cyc % 3 == 0 until cyc % 5 == 0) + results[4].passs++; + else results[4].fails++; + + always @(clk) begin + ++cyc; + if (cyc == MAX) begin + expected[1] = '{0, 7}; + // expected[2] shouldn't be initialized + expected[3] = '{0, 7}; + expected[4] = '{5, 2}; + `checkh(results, expected); + $write("*-* All Finished *-*\n"); + $finish; + end + end +endmodule