From ba508c00d2c8a5a667974638ef93ec75f9d233d2 Mon Sep 17 00:00:00 2001 From: Ryszard Rozak Date: Fri, 17 Apr 2026 12:33:36 +0200 Subject: [PATCH] Support `until_with` property (#7290 partial) (#7436) --- src/V3AssertPre.cpp | 22 +++++++++--- src/V3AstNodeExpr.h | 13 +++++-- src/V3AstNodes.cpp | 10 ++++++ src/verilog.y | 8 ++--- test_regress/t/t_property_pexpr_unsup.out | 9 ----- .../t/t_property_sexpr_parse_unsup.out | 16 ++++----- test_regress/t/t_property_sexpr_unsup.out | 8 +++++ test_regress/t/t_property_sexpr_unsup.v | 4 +++ test_regress/t/t_property_unsup.out | 36 ------------------- test_regress/t/t_property_until.v | 9 +++-- 10 files changed, 69 insertions(+), 66 deletions(-) diff --git a/src/V3AssertPre.cpp b/src/V3AssertPre.cpp index 765e4ec9b..789a73e3e 100644 --- a/src/V3AssertPre.cpp +++ b/src/V3AssertPre.cpp @@ -1148,16 +1148,28 @@ private: VL_DO_DANGLING(pushDeletep(nodep), nodep); return; } + if (nodep->isStrong()) { + nodep->v3warn(E_UNSUPPORTED, "Unsupported: s_until" + << (nodep->isOverlapping() ? "_with" : "") + << " (in property expresion)"); + 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}); + AstNodeExpr* const lhsp = nodep->lhsp()->unlinkFrBack(); + AstLogAnd* const loopCondp = new AstLogAnd{flp, lhsp, new AstLogNot{flp, rhsp}}; + loopp->addStmtsp(new AstLoopTest{flp, loopp, loopCondp}); loopp->addStmtsp(new AstEventControl{flp, newSenTree(nodep), nullptr}); + AstNodeExpr* const rhsCopyp = rhsp->cloneTreePure(false); + AstNodeExpr* const passCondp + = nodep->isOverlapping() ? new AstLogAnd{flp, lhsp->cloneTreePure(false), rhsCopyp} + : rhsCopyp; AstBegin* const beginp = new AstBegin{flp, "", loopp, true}; - beginp->addStmtsp(new AstIf{flp, rhsp->cloneTreePure(false), new AstPExprClause{flp}, - new AstPExprClause{flp, false}}); + beginp->addStmtsp( + new AstIf{flp, passCondp, new AstPExprClause{flp}, new AstPExprClause{flp, false}}); AstPExpr* const pexprp = new AstPExpr{flp, beginp, nodep->dtypep()}; pexprp->user1(1); diff --git a/src/V3AstNodeExpr.h b/src/V3AstNodeExpr.h index c821a179d..498744f72 100644 --- a/src/V3AstNodeExpr.h +++ b/src/V3AstNodeExpr.h @@ -2737,19 +2737,28 @@ class AstUntil final : public AstNodeExpr { // The until property expression // @astgen op1 := lhsp : AstNodeExpr // @astgen op2 := rhsp : AstNodeExpr + + const bool m_strong; // 's_' preffix + const bool m_overlapping; // '_with` suffix public: - AstUntil(FileLine* fl, AstNodeExpr* lhsp, AstNodeExpr* rhsp) - : ASTGEN_SUPER_Until(fl) { + AstUntil(FileLine* fl, AstNodeExpr* lhsp, AstNodeExpr* rhsp, bool strong, bool overlapping) + : ASTGEN_SUPER_Until(fl) + , m_strong{strong} + , m_overlapping{overlapping} { this->lhsp(lhsp); this->rhsp(rhsp); } ASTGEN_MEMBERS_AstUntil; + void dump(std::ostream& str) const override; + void dumpJson(std::ostream& str) const override; 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; } + bool isStrong() const { return m_strong; } + bool isOverlapping() const { return m_overlapping; } }; class AstValuePlusArgs final : public AstNodeExpr { // Search expression. If nullptr then this is a $test$plusargs instead of $value$plusargs. diff --git a/src/V3AstNodes.cpp b/src/V3AstNodes.cpp index 90fd147d3..acf4b10fa 100644 --- a/src/V3AstNodes.cpp +++ b/src/V3AstNodes.cpp @@ -2524,6 +2524,16 @@ bool AstUnionDType::sameNode(const AstNode* samep) const { const AstUnionDType* const asamep = VN_DBG_AS(samep, UnionDType); return m_isSoft == asamep->m_isSoft && m_isTagged == asamep->m_isTagged; } +void AstUntil::dump(std::ostream& str) const { + this->AstNodeExpr::dump(str); + if (isStrong()) str << " [strong]"; + if (isOverlapping()) str << " [overlapping]"; +} +void AstUntil::dumpJson(std::ostream& str) const { + this->AstNodeExpr::dumpJson(str); + dumpJsonBoolFuncIf(str, isStrong); + dumpJsonBoolFuncIf(str, isOverlapping); +} string AstNodeUOrStructDType::prettyDTypeName(bool full) const { string result = verilogKwd() + "{"; if (full) { // else shorten for errors diff --git a/src/verilog.y b/src/verilog.y index 437921dbe..b6c513ddb 100644 --- a/src/verilog.y +++ b/src/verilog.y @@ -6759,13 +6759,13 @@ 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 - { $$ = new AstUntil{$2, $1, $3}; } + { $$ = new AstUntil{$2, $1, $3, false, false}; } | ~o~pexpr yS_UNTIL pexpr - { $$ = $1; BBUNSUP($2, "Unsupported: s_until (in property expression)"); DEL($3); } + { $$ = new AstUntil{$2, $1, $3, true, false}; } | ~o~pexpr yUNTIL_WITH pexpr - { $$ = $1; BBUNSUP($2, "Unsupported: until_with (in property expression)"); DEL($3); } + { $$ = new AstUntil{$2, $1, $3, false, true}; } | ~o~pexpr yS_UNTIL_WITH pexpr - { $$ = $1; BBUNSUP($2, "Unsupported: s_until_with (in property expression)"); DEL($3); } + { $$ = new AstUntil{$2, $1, $3, true, true}; } | ~o~pexpr yIMPLIES pexpr { $$ = new AstLogOr{$2, new AstLogNot{$2, $1}, $3}; } // // yIFF also used by event_expression diff --git a/test_regress/t/t_property_pexpr_unsup.out b/test_regress/t/t_property_pexpr_unsup.out index 2e6a3696a..0a93880ae 100644 --- a/test_regress/t/t_property_pexpr_unsup.out +++ b/test_regress/t/t_property_pexpr_unsup.out @@ -5,15 +5,6 @@ %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: s_until (in property expression) - 31 | a s_until 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:39:7: Unsupported: s_until_with (in property expression) - 39 | a s_until_with b; - | ^~~~~~~~~~~~ %Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:43:7: Unsupported: #-# (in property expression) 43 | a #-# b; | ^~~ diff --git a/test_regress/t/t_property_sexpr_parse_unsup.out b/test_regress/t/t_property_sexpr_parse_unsup.out index aeec3a4f3..7a746e9dd 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:66: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:70:14: Logical operator IMPLICATION expects 1 bit on the RHS, but RHS's CMETHODHARD 'at' generates 8 bits. : ... note: In instance 't.ieee' - 66 | $rose(a) |-> q[0]; + 70 | $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:71: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:75:29: Logical operator SEXPR expects 1 bit on the exprp, but exprp's CMETHODHARD 'at' generates 8 bits. : ... note: In instance 't.ieee' - 71 | ($rose(a), l_b = b) |-> ##[3:10] q[l_b]; + 75 | ($rose(a), l_b = b) |-> ##[3:10] q[l_b]; | ^~ -%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. +%Warning-WIDTHTRUNC: t/t_property_sexpr_unsup.v:96:31: Logical operator SEXPR expects 1 bit on the exprp, but exprp's VARREF 'b' generates 32 bits. : ... note: In instance 't.ieee' - 92 | assert property (@clk not a ##1 b); + 96 | assert property (@clk not a ##1 b); | ^~ -%Error: Internal Error: t/t_property_sexpr_unsup.v:71:29: ../V3AssertProp.cpp:#: Range delay SExpr without clocking event +%Error: Internal Error: t/t_property_sexpr_unsup.v:75:29: ../V3AssertProp.cpp:#: Range delay SExpr without clocking event : ... note: In instance 't.ieee' - 71 | ($rose(a), l_b = b) |-> ##[3:10] q[l_b]; + 75 | ($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 ea5a9e088..54ba8d14e 100644 --- a/test_regress/t/t_property_sexpr_unsup.out +++ b/test_regress/t/t_property_sexpr_unsup.out @@ -35,4 +35,12 @@ : ... 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) + : ... note: In instance 't' + 51 | assert property (@(posedge clk) val s_until !val) $display("[%0t] s_until, fileline:%d", $time, 51); + | ^~~~~~~ +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:53:39: Unsupported: s_until_with (in property expresion) + : ... note: In instance 't' + 53 | assert property (@(posedge clk) val s_until_with val) $display("[%0t] s_until_with, fileline:%d", $time, 53); + | ^~~~~~~~~~~~ %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 cbbe9748f..c59b2b738 100644 --- a/test_regress/t/t_property_sexpr_unsup.v +++ b/test_regress/t/t_property_sexpr_unsup.v @@ -48,6 +48,10 @@ 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) val s_until_with val) $display("[%0t] s_until_with, 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 809ec67ee..ec5a79c63 100644 --- a/test_regress/t/t_property_unsup.out +++ b/test_regress/t/t_property_unsup.out @@ -29,24 +29,6 @@ %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: s_until (in property expression) - 98 | 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: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: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: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: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:106:23: Unsupported: #-# (in property expression) 106 | assert property ((a #-# b) implies (a #-# b)); | ^~~ @@ -71,24 +53,6 @@ %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: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: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: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: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: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: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:130:23: Unsupported: #-# (in property expression) 130 | assert property ((a #-# b) iff (a #-# b)); | ^~~ diff --git a/test_regress/t/t_property_until.v b/test_regress/t/t_property_until.v index b72706982..137c9417c 100644 --- a/test_regress/t/t_property_until.v +++ b/test_regress/t/t_property_until.v @@ -24,7 +24,7 @@ module t ( /*AUTOARG*/ result_t expected[int]; localparam MAX = 15; - integer cyc = 0; + integer cyc = 1; assert property (@(posedge clk) 0 until 1) results[1].passs++; @@ -42,13 +42,18 @@ module t ( /*AUTOARG*/ results[4].passs++; else results[4].fails++; - always @(clk) begin + assert property (@(posedge clk) cyc % 3 != 0 until_with cyc % 4 != 0) + results[5].passs++; + else results[5].fails++; + + always @(edge 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}; + expected[5] = '{2, 5}; `checkh(results, expected); $write("*-* All Finished *-*\n"); $finish;