luke
/
verilator
mirror of https://github.com/verilator/verilator.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Support 'until' property (partial #7290) (#7399)

This commit is contained in:
Ryszard Rozak 2026-04-10 14:17:54 +02:00 committed by GitHub
parent cf9a52cb92
commit 4da31b0418
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
13 changed files with 269 additions and 140 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

42
src/V3AssertPre.cpp
View File

@ -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<AstVarXRef*> m_xrefsp; // list of xrefs that need name fixup
bool m_inPExpr = false; // True if in AstPExpr
std::vector<AstSequence*> 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;

18
src/V3AstNodeExpr.h
View File

@ -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]

9
src/V3Width.cpp
View File

@ -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()) {

2
src/verilog.y
View File

@ -6759,7 +6759,7 @@ pexpr<nodeExprp>: // 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

121
test_regress/t/t_property_pexpr_unsup.out
View File

@ -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

4
test_regress/t/t_property_pexpr_unsup.v
View File

@ -27,10 +27,6 @@ module t (
weak(a);
endproperty
property p_until;
a until b;
endproperty
property p_suntil;
a s_until b;
endproperty

16
test_regress/t/t_property_sexpr_parse_unsup.out
View File

@ -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.

12
test_regress/t/t_property_sexpr_unsup.out
View File

@ -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

6
test_regress/t/t_property_sexpr_unsup.v
View File

@ -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

100
test_regress/t/t_property_unsup.out
View File

@ -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

4
test_regress/t/t_property_unsup.v
View File

@ -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 :

18
test_regress/t/t_property_until.py Executable file
View File

@ -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()

57
test_regress/t/t_property_until.v Normal file
View File

@ -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