Fix parsing of `eventually[]` and pexpr memory leaks (#6530)
* Fix parsing of eventually[] * Fix parser memory leaks for pexpr Signed-off-by: Bartłomiej Chmiel <bchmiel@antmicro.com>
This commit is contained in:
Bartłomiej Chmiel
GitHub
parent
0280de11da
commit
9f5d22b21f
|
|
@ -6334,9 +6334,9 @@ property_port_itemDirE:
|
||||||
|
|
||||||
property_declarationBody<nodep>: // IEEE: part of property_declaration
|
property_declarationBody<nodep>: // IEEE: part of property_declaration
|
||||||
assertion_variable_declarationList property_spec
|
assertion_variable_declarationList property_spec
|
||||||
{ $$ = nullptr; BBUNSUP($1->fileline(), "Unsupported: property variable declaration"); DEL($1); }
|
{ $$ = nullptr; BBUNSUP($1->fileline(), "Unsupported: property variable declaration"); DEL($1, $2); }
|
||||||
| assertion_variable_declarationList property_spec ';'
|
| assertion_variable_declarationList property_spec ';'
|
||||||
{ $$ = nullptr; BBUNSUP($1->fileline(), "Unsupported: property variable declaration"); DEL($1); }
|
{ $$ = nullptr; BBUNSUP($1->fileline(), "Unsupported: property variable declaration"); DEL($1, $2); }
|
||||||
// // IEEE-2012: Incorrectly has yCOVER ySEQUENCE then property_spec here.
|
// // IEEE-2012: Incorrectly has yCOVER ySEQUENCE then property_spec here.
|
||||||
// // Fixed in IEEE 1800-2017
|
// // Fixed in IEEE 1800-2017
|
||||||
| property_spec { $$ = $1; }
|
| property_spec { $$ = $1; }
|
||||||
|
|
@ -6445,14 +6445,16 @@ property_spec<propSpecp>: // IEEE: property_spec
|
||||||
property_statementCaseIf<nodeExprp>: // IEEE: property_statement - minus pexpr
|
property_statementCaseIf<nodeExprp>: // IEEE: property_statement - minus pexpr
|
||||||
yCASE '(' expr/*expression_or_dist*/ ')' property_case_itemList yENDCASE
|
yCASE '(' expr/*expression_or_dist*/ ')' property_case_itemList yENDCASE
|
||||||
{ $$ = new AstConst{$1, AstConst::BitFalse{}};
|
{ $$ = new AstConst{$1, AstConst::BitFalse{}};
|
||||||
BBUNSUP($<fl>1, "Unsupported: property case expression"); }
|
BBUNSUP($<fl>1, "Unsupported: property case expression");
|
||||||
|
DEL($3, $5); }
|
||||||
| yCASE '(' expr/*expression_or_dist*/ ')' yENDCASE
|
| yCASE '(' expr/*expression_or_dist*/ ')' yENDCASE
|
||||||
{ $$ = new AstConst{$1, AstConst::BitFalse{}};
|
{ $$ = new AstConst{$1, AstConst::BitFalse{}};
|
||||||
BBUNSUP($<fl>1, "Unsupported: property case expression"); }
|
BBUNSUP($<fl>1, "Unsupported: property case expression");
|
||||||
|
DEL($3); }
|
||||||
| yIF '(' expr/*expression_or_dist*/ ')' pexpr %prec prLOWER_THAN_ELSE
|
| yIF '(' expr/*expression_or_dist*/ ')' pexpr %prec prLOWER_THAN_ELSE
|
||||||
{ $$ = $5; BBUNSUP($<fl>1, "Unsupported: property case expression"); }
|
{ $$ = $5; BBUNSUP($<fl>1, "Unsupported: property case expression"); DEL($3); }
|
||||||
| yIF '(' expr/*expression_or_dist*/ ')' pexpr yELSE pexpr
|
| yIF '(' expr/*expression_or_dist*/ ')' pexpr yELSE pexpr
|
||||||
{ $$ = $5; BBUNSUP($<fl>1, "Unsupported: property case expression"); }
|
{ $$ = $5; BBUNSUP($<fl>1, "Unsupported: property case expression"); DEL($3, $7); }
|
||||||
;
|
;
|
||||||
|
|
||||||
property_case_itemList<caseItemp>: // IEEE: {property_case_item}
|
property_case_itemList<caseItemp>: // IEEE: {property_case_item}
|
||||||
|
|
@ -6523,9 +6525,9 @@ pexpr<nodeExprp>: // IEEE: property_expr (The name pexpr is important as regex
|
||||||
| property_statementCaseIf { $$ = $1; }
|
| property_statementCaseIf { $$ = $1; }
|
||||||
//
|
//
|
||||||
| ~o~pexpr/*sexpr*/ yP_POUNDMINUSPD pexpr
|
| ~o~pexpr/*sexpr*/ yP_POUNDMINUSPD pexpr
|
||||||
{ $$ = $3; BBUNSUP($2, "Unsupported: #-# (in property expression)"); }
|
{ $$ = $1; BBUNSUP($2, "Unsupported: #-# (in property expression)"); DEL($3); }
|
||||||
| ~o~pexpr/*sexpr*/ yP_POUNDEQPD pexpr
|
| ~o~pexpr/*sexpr*/ yP_POUNDEQPD pexpr
|
||||||
{ $$ = $3; BBUNSUP($2, "Unsupported: #=# (in property expression)"); }
|
{ $$ = $1; BBUNSUP($2, "Unsupported: #=# (in property expression)"); DEL($3); }
|
||||||
| yNEXTTIME pexpr
|
| yNEXTTIME pexpr
|
||||||
{ $$ = $2; BBUNSUP($1, "Unsupported: nexttime (in property expression)"); }
|
{ $$ = $2; BBUNSUP($1, "Unsupported: nexttime (in property expression)"); }
|
||||||
| yS_NEXTTIME pexpr
|
| yS_NEXTTIME pexpr
|
||||||
|
|
@ -6540,22 +6542,20 @@ pexpr<nodeExprp>: // IEEE: property_expr (The name pexpr is important as regex
|
||||||
{ $$ = $3; BBUNSUP($1, "Unsupported: always[] (in property expression)"); DEL($2); }
|
{ $$ = $3; BBUNSUP($1, "Unsupported: always[] (in property expression)"); DEL($2); }
|
||||||
| yS_ALWAYS anyrange pexpr %prec yS_ALWAYS
|
| yS_ALWAYS anyrange pexpr %prec yS_ALWAYS
|
||||||
{ $$ = $3; BBUNSUP($1, "Unsupported: s_always (in property expression)"); DEL($2); }
|
{ $$ = $3; BBUNSUP($1, "Unsupported: s_always (in property expression)"); DEL($2); }
|
||||||
| yEVENTUALLY pexpr
|
|
||||||
{ $$ = $2; BBUNSUP($1, "Unsupported: eventually (in property expression)"); }
|
|
||||||
| yS_EVENTUALLY pexpr
|
| yS_EVENTUALLY pexpr
|
||||||
{ $$ = $2; BBUNSUP($1, "Unsupported: s_eventually (in property expression)"); }
|
{ $$ = $2; BBUNSUP($1, "Unsupported: s_eventually (in property expression)"); }
|
||||||
| yEVENTUALLY '[' constExpr ']' pexpr %prec yEVENTUALLY
|
|
||||||
{ $$ = $5; BBUNSUP($1, "Unsupported: eventually[] (in property expression)"); DEL($3); }
|
|
||||||
| yS_EVENTUALLY anyrange pexpr %prec yS_EVENTUALLY
|
| yS_EVENTUALLY anyrange pexpr %prec yS_EVENTUALLY
|
||||||
{ $$ = $3; BBUNSUP($1, "Unsupported: s_eventually[] (in property expression)"); DEL($2); }
|
{ $$ = $3; BBUNSUP($1, "Unsupported: s_eventually[] (in property expression)"); DEL($2); }
|
||||||
|
| yEVENTUALLY anyrange pexpr %prec yS_EVENTUALLY
|
||||||
|
{ $$ = $3; BBUNSUP($1, "Unsupported: eventually[] (in property expression)"); DEL($2); }
|
||||||
| ~o~pexpr yUNTIL pexpr
|
| ~o~pexpr yUNTIL pexpr
|
||||||
{ $$ = $1; BBUNSUP($2, "Unsupported: until (in property expression)"); }
|
{ $$ = $1; BBUNSUP($2, "Unsupported: until (in property expression)"); DEL($3); }
|
||||||
| ~o~pexpr yS_UNTIL pexpr
|
| ~o~pexpr yS_UNTIL pexpr
|
||||||
{ $$ = $1; BBUNSUP($2, "Unsupported: s_until (in property expression)"); }
|
{ $$ = $1; BBUNSUP($2, "Unsupported: s_until (in property expression)"); DEL($3); }
|
||||||
| ~o~pexpr yUNTIL_WITH pexpr
|
| ~o~pexpr yUNTIL_WITH pexpr
|
||||||
{ $$ = $1; BBUNSUP($2, "Unsupported: until_with (in property expression)"); }
|
{ $$ = $1; BBUNSUP($2, "Unsupported: until_with (in property expression)"); DEL($3); }
|
||||||
| ~o~pexpr yS_UNTIL_WITH pexpr
|
| ~o~pexpr yS_UNTIL_WITH pexpr
|
||||||
{ $$ = $1; BBUNSUP($2, "Unsupported: s_until_with (in property expression)"); }
|
{ $$ = $1; BBUNSUP($2, "Unsupported: s_until_with (in property expression)"); DEL($3); }
|
||||||
| ~o~pexpr yIMPLIES pexpr
|
| ~o~pexpr yIMPLIES pexpr
|
||||||
{ $$ = new AstLogOr{$2, new AstLogNot{$2, $1}, $3}; }
|
{ $$ = new AstLogOr{$2, new AstLogNot{$2, $1}, $3}; }
|
||||||
// // yIFF also used by event_expression
|
// // yIFF also used by event_expression
|
||||||
|
|
@ -6594,15 +6594,15 @@ sexpr<nodeExprp>: // ==IEEE: sequence_expr (The name sexpr is important as reg
|
||||||
// // IEEE: "sequence_expr cycle_delay_range sequence_expr { cycle_delay_range sequence_expr }"
|
// // IEEE: "sequence_expr cycle_delay_range sequence_expr { cycle_delay_range sequence_expr }"
|
||||||
// // Both rules basically mean we can repeat sequences, so make it simpler:
|
// // Both rules basically mean we can repeat sequences, so make it simpler:
|
||||||
cycle_delay_range ~p~sexpr %prec yP_POUNDPOUND
|
cycle_delay_range ~p~sexpr %prec yP_POUNDPOUND
|
||||||
{ $$ = $2; BBUNSUP($2->fileline(), "Unsupported: ## (in sequence expression)"); }
|
{ $$ = $2; BBUNSUP($2->fileline(), "Unsupported: ## (in sequence expression)"); DEL($1); }
|
||||||
| ~p~sexpr cycle_delay_range sexpr %prec prPOUNDPOUND_MULTI
|
| ~p~sexpr cycle_delay_range sexpr %prec prPOUNDPOUND_MULTI
|
||||||
{ $$ = $1; BBUNSUP($2->fileline(), "Unsupported: ## (in sequence expression)"); }
|
{ $$ = $1; BBUNSUP($2->fileline(), "Unsupported: ## (in sequence expression)"); DEL($2, $3); }
|
||||||
//
|
//
|
||||||
// // IEEE: expression_or_dist [ boolean_abbrev ]
|
// // IEEE: expression_or_dist [ boolean_abbrev ]
|
||||||
// // Note expression_or_dist includes "expr"!
|
// // Note expression_or_dist includes "expr"!
|
||||||
// // sexpr/*sexpression_or_dist*/ --- Hardcoded below
|
// // sexpr/*sexpression_or_dist*/ --- Hardcoded below
|
||||||
| ~p~sexpr/*sexpression_or_dist*/ boolean_abbrev
|
| ~p~sexpr/*sexpression_or_dist*/ boolean_abbrev
|
||||||
{ $$ = $1; BBUNSUP($2->fileline(), "Unsupported: boolean abbrev (in sequence expression)"); }
|
{ $$ = $1; BBUNSUP($2->fileline(), "Unsupported: boolean abbrev (in sequence expression)"); DEL($2); }
|
||||||
//
|
//
|
||||||
// // IEEE: "sequence_instance [ sequence_abbrev ]"
|
// // IEEE: "sequence_instance [ sequence_abbrev ]"
|
||||||
// // version without sequence_abbrev looks just like normal function call
|
// // version without sequence_abbrev looks just like normal function call
|
||||||
|
|
@ -6616,7 +6616,7 @@ sexpr<nodeExprp>: // ==IEEE: sequence_expr (The name sexpr is important as reg
|
||||||
// // "'(' sexpr ')' boolean_abbrev" matches "[sexpr:'(' expr ')'] boolean_abbrev" so we can drop it
|
// // "'(' sexpr ')' boolean_abbrev" matches "[sexpr:'(' expr ')'] boolean_abbrev" so we can drop it
|
||||||
| '(' ~p~sexpr ')' { $$ = $2; }
|
| '(' ~p~sexpr ')' { $$ = $2; }
|
||||||
| '(' ~p~sexpr ',' sequence_match_itemList ')'
|
| '(' ~p~sexpr ',' sequence_match_itemList ')'
|
||||||
{ $$ = $2; BBUNSUP($3, "Unsupported sequence match items"); }
|
{ $$ = $2; BBUNSUP($3, "Unsupported sequence match items"); DEL($4); }
|
||||||
//
|
//
|
||||||
// // AND/OR are between pexprs OR sexprs
|
// // AND/OR are between pexprs OR sexprs
|
||||||
| ~p~sexpr yAND ~p~sexpr
|
| ~p~sexpr yAND ~p~sexpr
|
||||||
|
|
@ -6627,18 +6627,18 @@ sexpr<nodeExprp>: // ==IEEE: sequence_expr (The name sexpr is important as reg
|
||||||
BBUNSUP($2, "Unsupported: or (in sequence expression)"); }
|
BBUNSUP($2, "Unsupported: or (in sequence expression)"); }
|
||||||
// // Intersect always has an sexpr rhs
|
// // Intersect always has an sexpr rhs
|
||||||
| ~p~sexpr yINTERSECT sexpr
|
| ~p~sexpr yINTERSECT sexpr
|
||||||
{ $$ = $1; BBUNSUP($2, "Unsupported: intersect (in sequence expression)"); }
|
{ $$ = $1; BBUNSUP($2, "Unsupported: intersect (in sequence expression)"); DEL($3); }
|
||||||
//
|
//
|
||||||
| yFIRST_MATCH '(' sexpr ')'
|
| yFIRST_MATCH '(' sexpr ')'
|
||||||
{ $$ = nullptr; BBUNSUP($1, "Unsupported: first_match (in sequence expression)"); DEL($3); }
|
{ $$ = $3; BBUNSUP($1, "Unsupported: first_match (in sequence expression)"); }
|
||||||
| yFIRST_MATCH '(' sexpr ',' sequence_match_itemList ')'
|
| yFIRST_MATCH '(' sexpr ',' sequence_match_itemList ')'
|
||||||
{ $$ = nullptr; BBUNSUP($1, "Unsupported: first_match (in sequence expression)"); DEL($3, $5); }
|
{ $$ = $3; BBUNSUP($1, "Unsupported: first_match (in sequence expression)"); DEL($5); }
|
||||||
| ~p~sexpr/*sexpression_or_dist*/ yTHROUGHOUT sexpr
|
| ~p~sexpr/*sexpression_or_dist*/ yTHROUGHOUT sexpr
|
||||||
{ $$ = $1; BBUNSUP($2, "Unsupported: throughout (in sequence expression)"); }
|
{ $$ = $1; BBUNSUP($2, "Unsupported: throughout (in sequence expression)"); DEL($3); }
|
||||||
// // Below pexpr's are really sequence_expr, but avoid conflict
|
// // Below pexpr's are really sequence_expr, but avoid conflict
|
||||||
// // IEEE: sexpr yWITHIN sexpr
|
// // IEEE: sexpr yWITHIN sexpr
|
||||||
| ~p~sexpr yWITHIN sexpr
|
| ~p~sexpr yWITHIN sexpr
|
||||||
{ $$ = $1; BBUNSUP($2, "Unsupported: within (in sequence expression)"); }
|
{ $$ = $1; BBUNSUP($2, "Unsupported: within (in sequence expression)"); DEL($3); }
|
||||||
// // Note concurrent_assertion had duplicate rule for below
|
// // Note concurrent_assertion had duplicate rule for below
|
||||||
//UNSUP clocking_event ~p~sexpr %prec prSEQ_CLOCKING { }
|
//UNSUP clocking_event ~p~sexpr %prec prSEQ_CLOCKING { }
|
||||||
//
|
//
|
||||||
|
|
@ -6664,7 +6664,7 @@ cycle_delay_range<nodep>: // IEEE: ==cycle_delay_range
|
||||||
// // the sv-ac committee has been asked to clarify (Mantis 1901)
|
// // the sv-ac committee has been asked to clarify (Mantis 1901)
|
||||||
| yP_POUNDPOUND anyrange
|
| yP_POUNDPOUND anyrange
|
||||||
{ $$ = new AstConst{$1, AstConst::BitFalse{}};
|
{ $$ = new AstConst{$1, AstConst::BitFalse{}};
|
||||||
BBUNSUP($<fl>1, "Unsupported: ## range cycle delay range expression"); }
|
BBUNSUP($<fl>1, "Unsupported: ## range cycle delay range expression"); DEL($2); }
|
||||||
| yP_POUNDPOUND yP_BRASTAR ']'
|
| yP_POUNDPOUND yP_BRASTAR ']'
|
||||||
{ $$ = new AstConst{$1, AstConst::BitFalse{}};
|
{ $$ = new AstConst{$1, AstConst::BitFalse{}};
|
||||||
BBUNSUP($<fl>1, "Unsupported: ## [*] cycle delay range expression"); }
|
BBUNSUP($<fl>1, "Unsupported: ## [*] cycle delay range expression"); }
|
||||||
|
|
@ -6691,7 +6691,7 @@ boolean_abbrev<nodeExprp>: // ==IEEE: boolean_abbrev
|
||||||
yP_BRASTAR constExpr ']'
|
yP_BRASTAR constExpr ']'
|
||||||
{ $$ = $2; BBUNSUP($<fl>1, "Unsupported: [*] boolean abbrev expression"); }
|
{ $$ = $2; BBUNSUP($<fl>1, "Unsupported: [*] boolean abbrev expression"); }
|
||||||
| yP_BRASTAR constExpr ':' constExpr ']'
|
| yP_BRASTAR constExpr ':' constExpr ']'
|
||||||
{ $$ = $2; BBUNSUP($<fl>1, "Unsupported: [*] boolean abbrev expression"); }
|
{ $$ = $2; BBUNSUP($<fl>1, "Unsupported: [*] boolean abbrev expression"); DEL($4); }
|
||||||
| yP_BRASTAR ']'
|
| yP_BRASTAR ']'
|
||||||
{ $$ = new AstConst{$1, AstConst::BitFalse{}};
|
{ $$ = new AstConst{$1, AstConst::BitFalse{}};
|
||||||
BBUNSUP($<fl>1, "Unsupported: [*] boolean abbrev expression"); }
|
BBUNSUP($<fl>1, "Unsupported: [*] boolean abbrev expression"); }
|
||||||
|
|
@ -6702,12 +6702,12 @@ boolean_abbrev<nodeExprp>: // ==IEEE: boolean_abbrev
|
||||||
| yP_BRAEQ constExpr ']'
|
| yP_BRAEQ constExpr ']'
|
||||||
{ $$ = $2; BBUNSUP($<fl>1, "Unsupported: [= boolean abbrev expression"); }
|
{ $$ = $2; BBUNSUP($<fl>1, "Unsupported: [= boolean abbrev expression"); }
|
||||||
| yP_BRAEQ constExpr ':' constExpr ']'
|
| yP_BRAEQ constExpr ':' constExpr ']'
|
||||||
{ $$ = $2; BBUNSUP($<fl>1, "Unsupported: [= boolean abbrev expression"); }
|
{ $$ = $2; BBUNSUP($<fl>1, "Unsupported: [= boolean abbrev expression"); DEL($4); }
|
||||||
// // IEEE: goto_repetition
|
// // IEEE: goto_repetition
|
||||||
| yP_BRAMINUSGT constExpr ']'
|
| yP_BRAMINUSGT constExpr ']'
|
||||||
{ $$ = $2; BBUNSUP($<fl>1, "Unsupported: [-> boolean abbrev expression"); }
|
{ $$ = $2; BBUNSUP($<fl>1, "Unsupported: [-> boolean abbrev expression"); }
|
||||||
| yP_BRAMINUSGT constExpr ':' constExpr ']'
|
| yP_BRAMINUSGT constExpr ':' constExpr ']'
|
||||||
{ $$ = $2; BBUNSUP($<fl>1, "Unsupported: [-> boolean abbrev expression"); }
|
{ $$ = $2; BBUNSUP($<fl>1, "Unsupported: [-> boolean abbrev expression"); DEL($4); }
|
||||||
;
|
;
|
||||||
|
|
||||||
//************************************************
|
//************************************************
|
||||||
|
|
|
||||||
|
|
@ -5,9 +5,22 @@
|
||||||
%Error-UNSUPPORTED: t/t_assert_always_unsup.v:25:7: Unsupported: s_always (in property expression)
|
%Error-UNSUPPORTED: t/t_assert_always_unsup.v:25:7: Unsupported: s_always (in property expression)
|
||||||
25 | s_always [2:5] a;
|
25 | s_always [2:5] a;
|
||||||
| ^~~~~~~~
|
| ^~~~~~~~
|
||||||
%Error: t/t_assert_always_unsup.v:29:20: syntax error, unexpected ':', expecting ']'
|
%Error-UNSUPPORTED: t/t_assert_always_unsup.v:29:7: Unsupported: eventually[] (in property expression)
|
||||||
29 | eventually [2:5] a;
|
29 | eventually [2:5] a;
|
||||||
| ^
|
| ^~~~~~~~~~
|
||||||
... See the manual at https://verilator.org/verilator_doc.html?v=latest for more assistance.
|
%Error-UNSUPPORTED: t/t_assert_always_unsup.v:33:7: Unsupported: s_eventually[] (in property expression)
|
||||||
%Error: Cannot continue
|
33 | s_eventually [2:5] a;
|
||||||
... This fatal error may be caused by the earlier error(s); resolve those first.
|
| ^~~~~~~~~~~~
|
||||||
|
%Error-UNSUPPORTED: t/t_assert_always_unsup.v:37:14: Unsupported: s_eventually[] (in property expression)
|
||||||
|
37 | always s_eventually [2:5] a;
|
||||||
|
| ^~~~~~~~~~~~
|
||||||
|
%Error-UNSUPPORTED: t/t_assert_always_unsup.v:37:7: Unsupported: always (in property expression)
|
||||||
|
37 | always s_eventually [2:5] a;
|
||||||
|
| ^~~~~~
|
||||||
|
%Error-UNSUPPORTED: t/t_assert_always_unsup.v:41:20: Unsupported: always[] (in property expression)
|
||||||
|
41 | s_eventually always [2:5] a;
|
||||||
|
| ^~~~~~
|
||||||
|
%Error-UNSUPPORTED: t/t_assert_always_unsup.v:41:7: Unsupported: s_eventually (in property expression)
|
||||||
|
41 | s_eventually always [2:5] a;
|
||||||
|
| ^~~~~~~~~~~~
|
||||||
|
%Error: Exiting due to
|
||||||
|
|
|
||||||
|
|
@ -1,7 +1,7 @@
|
||||||
// DESCRIPTION: Verilator: Verilog Test module
|
// DESCRIPTION: Verilator: Verilog Test module
|
||||||
//
|
//
|
||||||
// This file ONLY is placed under the Creative Commons Public Domain, for
|
// This file ONLY is placed under the Creative Commons Public Domain, for
|
||||||
// any use, without warranty, 2022 by Antmicro Ltd.
|
// any use, without warranty, 2022-2025 by Antmicro.
|
||||||
// SPDX-License-Identifier: CC0-1.0
|
// SPDX-License-Identifier: CC0-1.0
|
||||||
|
|
||||||
module t (/*AUTOARG*/
|
module t (/*AUTOARG*/
|
||||||
|
|
@ -29,10 +29,6 @@ module t (/*AUTOARG*/
|
||||||
eventually [2:5] a;
|
eventually [2:5] a;
|
||||||
endproperty
|
endproperty
|
||||||
|
|
||||||
property p_ev2;
|
|
||||||
eventually [2] a;
|
|
||||||
endproperty
|
|
||||||
|
|
||||||
property p_s_ev;
|
property p_s_ev;
|
||||||
s_eventually [2:5] a;
|
s_eventually [2:5] a;
|
||||||
endproperty
|
endproperty
|
||||||
|
|
|
||||||
|
|
@ -43,6 +43,7 @@ EXEMPT_FILES_LIST = """
|
||||||
test_regress/t/t_flag_f__3.v
|
test_regress/t/t_flag_f__3.v
|
||||||
test_regress/t/t_fuzz_eof_bad.v
|
test_regress/t/t_fuzz_eof_bad.v
|
||||||
test_regress/t/t_incr_void.v
|
test_regress/t/t_incr_void.v
|
||||||
|
test_regress/t/t_property_unsup.v
|
||||||
test_regress/t/tsub/t_flag_f_tsub.v
|
test_regress/t/tsub/t_flag_f_tsub.v
|
||||||
test_regress/t/tsub/t_flag_f_tsub_inc.v
|
test_regress/t/tsub/t_flag_f_tsub_inc.v
|
||||||
test_regress/t/uvm/dpi
|
test_regress/t/uvm/dpi
|
||||||
|
|
|
||||||
|
|
@ -47,61 +47,55 @@
|
||||||
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:77:7: Unsupported: nexttime[] (in property expression)
|
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:77:7: Unsupported: nexttime[] (in property expression)
|
||||||
77 | nexttime [2] always a;
|
77 | nexttime [2] always a;
|
||||||
| ^~~~~~~~
|
| ^~~~~~~~
|
||||||
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:81:16: Unsupported: eventually (in property expression)
|
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:81:20: Unsupported: always (in property expression)
|
||||||
81 | nexttime eventually a;
|
81 | nexttime [2] always a;
|
||||||
| ^~~~~~~~~~
|
|
||||||
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:81:7: Unsupported: nexttime (in property expression)
|
|
||||||
81 | nexttime eventually a;
|
|
||||||
| ^~~~~~~~
|
|
||||||
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:85:20: Unsupported: always (in property expression)
|
|
||||||
85 | nexttime [2] always a;
|
|
||||||
| ^~~~~~
|
| ^~~~~~
|
||||||
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:85:7: Unsupported: nexttime[] (in property expression)
|
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:81:7: Unsupported: nexttime[] (in property expression)
|
||||||
85 | nexttime [2] always a;
|
81 | nexttime [2] always a;
|
||||||
| ^~~~~~~~
|
| ^~~~~~~~
|
||||||
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:89:16: Unsupported: s_eventually (in property expression)
|
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:85:16: Unsupported: s_eventually (in property expression)
|
||||||
89 | nexttime s_eventually a;
|
85 | nexttime s_eventually a;
|
||||||
|
| ^~~~~~~~~~~~
|
||||||
|
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:85:7: Unsupported: nexttime (in property expression)
|
||||||
|
85 | nexttime s_eventually a;
|
||||||
|
| ^~~~~~~~
|
||||||
|
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:89:35: Unsupported: always (in property expression)
|
||||||
|
89 | nexttime s_eventually [2:$] always a;
|
||||||
|
| ^~~~~~
|
||||||
|
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:89:16: Unsupported: s_eventually[] (in property expression)
|
||||||
|
89 | nexttime s_eventually [2:$] always a;
|
||||||
| ^~~~~~~~~~~~
|
| ^~~~~~~~~~~~
|
||||||
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:89:7: Unsupported: nexttime (in property expression)
|
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:89:7: Unsupported: nexttime (in property expression)
|
||||||
89 | nexttime s_eventually a;
|
89 | nexttime s_eventually [2:$] always a;
|
||||||
| ^~~~~~~~
|
| ^~~~~~~~
|
||||||
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:93:35: Unsupported: always (in property expression)
|
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:93:17: Unsupported: accept_on (in property expression)
|
||||||
93 | nexttime s_eventually [2:$] always a;
|
93 | accept_on (a) b;
|
||||||
| ^~~~~~
|
| ^
|
||||||
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:93:16: Unsupported: s_eventually[] (in property expression)
|
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:97:22: Unsupported: sync_accept_on (in property expression)
|
||||||
93 | nexttime s_eventually [2:$] always a;
|
97 | sync_accept_on (a) b;
|
||||||
| ^~~~~~~~~~~~
|
| ^
|
||||||
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:93:7: Unsupported: nexttime (in property expression)
|
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:101:17: Unsupported: reject_on (in property expression)
|
||||||
93 | nexttime s_eventually [2:$] always a;
|
101 | reject_on (a) b;
|
||||||
|
| ^
|
||||||
|
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:105:22: Unsupported: sync_reject_on (in property expression)
|
||||||
|
105 | sync_reject_on (a) b;
|
||||||
|
| ^
|
||||||
|
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:108:27: Unsupported: property argument data type
|
||||||
|
108 | property p_arg_propery(property inprop);
|
||||||
| ^~~~~~~~
|
| ^~~~~~~~
|
||||||
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:97:17: Unsupported: accept_on (in property expression)
|
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:111:27: Unsupported: sequence argument data type
|
||||||
97 | accept_on (a) b;
|
111 | property p_arg_seqence(sequence inseq);
|
||||||
| ^
|
|
||||||
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:101:22: Unsupported: sync_accept_on (in property expression)
|
|
||||||
101 | sync_accept_on (a) b;
|
|
||||||
| ^
|
|
||||||
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:105:17: Unsupported: reject_on (in property expression)
|
|
||||||
105 | reject_on (a) b;
|
|
||||||
| ^
|
|
||||||
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:109:22: Unsupported: sync_reject_on (in property expression)
|
|
||||||
109 | sync_reject_on (a) b;
|
|
||||||
| ^
|
|
||||||
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:112:27: Unsupported: property argument data type
|
|
||||||
112 | property p_arg_propery(property inprop);
|
|
||||||
| ^~~~~~~~
|
| ^~~~~~~~
|
||||||
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:115:27: Unsupported: sequence argument data type
|
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:116:7: Unsupported: property case expression
|
||||||
115 | property p_arg_seqence(sequence inseq);
|
116 | case (a) endcase
|
||||||
| ^~~~~~~~
|
|
||||||
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:120:7: Unsupported: property case expression
|
|
||||||
120 | case (a) endcase
|
|
||||||
| ^~~~
|
| ^~~~
|
||||||
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:123:7: Unsupported: property case expression
|
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:119:7: Unsupported: property case expression
|
||||||
123 | case (a) default: b; endcase
|
119 | case (a) default: b; endcase
|
||||||
| ^~~~
|
| ^~~~
|
||||||
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:126:7: Unsupported: property case expression
|
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:122:7: Unsupported: property case expression
|
||||||
126 | if (a) b
|
122 | if (a) b
|
||||||
| ^~
|
| ^~
|
||||||
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:129:7: Unsupported: property case expression
|
%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:125:7: Unsupported: property case expression
|
||||||
129 | if (a) b else c
|
125 | if (a) b else c
|
||||||
| ^~
|
| ^~
|
||||||
%Error: Exiting due to
|
%Error: Exiting due to
|
||||||
|
|
|
||||||
|
|
@ -77,10 +77,6 @@ module t (/*AUTOARG*/
|
||||||
nexttime [2] always a;
|
nexttime [2] always a;
|
||||||
endproperty
|
endproperty
|
||||||
|
|
||||||
property p_nexttime_eventually;
|
|
||||||
nexttime eventually a;
|
|
||||||
endproperty
|
|
||||||
|
|
||||||
property p_nexttime_eventually2;
|
property p_nexttime_eventually2;
|
||||||
nexttime [2] always a;
|
nexttime [2] always a;
|
||||||
endproperty
|
endproperty
|
||||||
|
|
|
||||||
|
|
@ -0,0 +1,116 @@
|
||||||
|
%Error-UNSUPPORTED: t/t_property_unsup.v:62:41: Unsupported: eventually[] (in property expression)
|
||||||
|
62 | assert property (counter == 1 implies eventually[1: 2] counter == 3);
|
||||||
|
| ^~~~~~~~~~
|
||||||
|
... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest
|
||||||
|
%Error-UNSUPPORTED: t/t_property_unsup.v:77:20: Unsupported: eventually[] (in property expression)
|
||||||
|
77 | assert property (eventually[0: 2] counter == 3);
|
||||||
|
| ^~~~~~~~~~
|
||||||
|
%Error-UNSUPPORTED: t/t_property_unsup.v:87:21: Unsupported: always (in property expression)
|
||||||
|
87 | assert property ((always a) implies (always a));
|
||||||
|
| ^~~~~~
|
||||||
|
%Error-UNSUPPORTED: t/t_property_unsup.v:87:40: Unsupported: always (in property expression)
|
||||||
|
87 | assert property ((always a) implies (always a));
|
||||||
|
| ^~~~~~
|
||||||
|
%Error-UNSUPPORTED: t/t_property_unsup.v:89:26: Unsupported: always (in property expression)
|
||||||
|
89 | assert property ((a or(always b)) implies (a or(always b)));
|
||||||
|
| ^~~~~~
|
||||||
|
%Error-UNSUPPORTED: t/t_property_unsup.v:89:23: Unsupported: or (in sequence expression)
|
||||||
|
89 | assert property ((a or(always b)) implies (a or(always b)));
|
||||||
|
| ^~
|
||||||
|
%Error-UNSUPPORTED: t/t_property_unsup.v:89:51: Unsupported: always (in property expression)
|
||||||
|
89 | assert property ((a or(always b)) implies (a or(always b)));
|
||||||
|
| ^~~~~~
|
||||||
|
%Error-UNSUPPORTED: t/t_property_unsup.v:89:48: Unsupported: or (in sequence expression)
|
||||||
|
89 | assert property ((a or(always b)) implies (a or(always b)));
|
||||||
|
| ^~
|
||||||
|
%Error-UNSUPPORTED: t/t_property_unsup.v:91:21: Unsupported: eventually[] (in property expression)
|
||||||
|
91 | assert property ((eventually[0: 1] a) implies (eventually[0: 1] a));
|
||||||
|
| ^~~~~~~~~~
|
||||||
|
%Error-UNSUPPORTED: t/t_property_unsup.v:91:50: Unsupported: eventually[] (in property expression)
|
||||||
|
91 | assert property ((eventually[0: 1] a) implies (eventually[0: 1] a));
|
||||||
|
| ^~~~~~~~~~
|
||||||
|
%Error-UNSUPPORTED: t/t_property_unsup.v:93:21: Unsupported: s_eventually (in property expression)
|
||||||
|
93 | assert property ((s_eventually a) implies (s_eventually a));
|
||||||
|
| ^~~~~~~~~~~~
|
||||||
|
%Error-UNSUPPORTED: t/t_property_unsup.v:93:46: Unsupported: s_eventually (in property expression)
|
||||||
|
93 | assert property ((s_eventually a) implies (s_eventually a));
|
||||||
|
| ^~~~~~~~~~~~
|
||||||
|
%Error-UNSUPPORTED: t/t_property_unsup.v:95:23: Unsupported: until (in property expression)
|
||||||
|
95 | assert property ((a until b) implies (a until b));
|
||||||
|
| ^~~~~
|
||||||
|
%Error-UNSUPPORTED: t/t_property_unsup.v:95:43: Unsupported: until (in property expression)
|
||||||
|
95 | assert property ((a until b) implies (a until b));
|
||||||
|
| ^~~~~
|
||||||
|
%Error-UNSUPPORTED: t/t_property_unsup.v:97:23: Unsupported: s_until (in property expression)
|
||||||
|
97 | assert property ((a s_until b) implies (a s_until b));
|
||||||
|
| ^~~~~~~
|
||||||
|
%Error-UNSUPPORTED: t/t_property_unsup.v:97:45: Unsupported: s_until (in property expression)
|
||||||
|
97 | assert property ((a s_until b) implies (a s_until b));
|
||||||
|
| ^~~~~~~
|
||||||
|
%Error-UNSUPPORTED: t/t_property_unsup.v:99:23: Unsupported: until_with (in property expression)
|
||||||
|
99 | assert property ((a until_with b) implies (a until_with b));
|
||||||
|
| ^~~~~~~~~~
|
||||||
|
%Error-UNSUPPORTED: t/t_property_unsup.v:99:48: Unsupported: until_with (in property expression)
|
||||||
|
99 | assert property ((a until_with b) implies (a until_with b));
|
||||||
|
| ^~~~~~~~~~
|
||||||
|
%Error-UNSUPPORTED: t/t_property_unsup.v:101:23: Unsupported: s_until_with (in property expression)
|
||||||
|
101 | assert property ((a s_until_with b) implies (a s_until_with b));
|
||||||
|
| ^~~~~~~~~~~~
|
||||||
|
%Error-UNSUPPORTED: t/t_property_unsup.v:101:50: Unsupported: s_until_with (in property expression)
|
||||||
|
101 | assert property ((a s_until_with b) implies (a s_until_with b));
|
||||||
|
| ^~~~~~~~~~~~
|
||||||
|
%Error-UNSUPPORTED: t/t_property_unsup.v:105:23: Unsupported: #-# (in property expression)
|
||||||
|
105 | assert property ((a #-# b) implies (a #-# b));
|
||||||
|
| ^~~
|
||||||
|
%Error-UNSUPPORTED: t/t_property_unsup.v:105:41: Unsupported: #-# (in property expression)
|
||||||
|
105 | assert property ((a #-# b) implies (a #-# b));
|
||||||
|
| ^~~
|
||||||
|
%Error-UNSUPPORTED: t/t_property_unsup.v:115:21: Unsupported: always (in property expression)
|
||||||
|
115 | assert property ((always a) iff (always a));
|
||||||
|
| ^~~~~~
|
||||||
|
%Error-UNSUPPORTED: t/t_property_unsup.v:115:36: Unsupported: always (in property expression)
|
||||||
|
115 | assert property ((always a) iff (always a));
|
||||||
|
| ^~~~~~
|
||||||
|
%Error-UNSUPPORTED: t/t_property_unsup.v:117:21: Unsupported: eventually[] (in property expression)
|
||||||
|
117 | assert property ((eventually[0: 1] a) iff (eventually[0: 1] a));
|
||||||
|
| ^~~~~~~~~~
|
||||||
|
%Error-UNSUPPORTED: t/t_property_unsup.v:117:46: Unsupported: eventually[] (in property expression)
|
||||||
|
117 | assert property ((eventually[0: 1] a) iff (eventually[0: 1] a));
|
||||||
|
| ^~~~~~~~~~
|
||||||
|
%Error-UNSUPPORTED: t/t_property_unsup.v:119:21: Unsupported: s_eventually (in property expression)
|
||||||
|
119 | assert property ((s_eventually a) iff (s_eventually a));
|
||||||
|
| ^~~~~~~~~~~~
|
||||||
|
%Error-UNSUPPORTED: t/t_property_unsup.v:119:42: Unsupported: s_eventually (in property expression)
|
||||||
|
119 | assert property ((s_eventually a) iff (s_eventually a));
|
||||||
|
| ^~~~~~~~~~~~
|
||||||
|
%Error-UNSUPPORTED: t/t_property_unsup.v:121:23: Unsupported: until (in property expression)
|
||||||
|
121 | assert property ((a until b) iff (a until b));
|
||||||
|
| ^~~~~
|
||||||
|
%Error-UNSUPPORTED: t/t_property_unsup.v:121:39: Unsupported: until (in property expression)
|
||||||
|
121 | assert property ((a until b) iff (a until b));
|
||||||
|
| ^~~~~
|
||||||
|
%Error-UNSUPPORTED: t/t_property_unsup.v:123:23: Unsupported: s_until (in property expression)
|
||||||
|
123 | assert property ((a s_until b) iff (a s_until b));
|
||||||
|
| ^~~~~~~
|
||||||
|
%Error-UNSUPPORTED: t/t_property_unsup.v:123:41: Unsupported: s_until (in property expression)
|
||||||
|
123 | assert property ((a s_until b) iff (a s_until b));
|
||||||
|
| ^~~~~~~
|
||||||
|
%Error-UNSUPPORTED: t/t_property_unsup.v:125:23: Unsupported: until_with (in property expression)
|
||||||
|
125 | assert property ((a until_with b) iff (a until_with b));
|
||||||
|
| ^~~~~~~~~~
|
||||||
|
%Error-UNSUPPORTED: t/t_property_unsup.v:125:44: Unsupported: until_with (in property expression)
|
||||||
|
125 | assert property ((a until_with b) iff (a until_with b));
|
||||||
|
| ^~~~~~~~~~
|
||||||
|
%Error-UNSUPPORTED: t/t_property_unsup.v:127:23: Unsupported: s_until_with (in property expression)
|
||||||
|
127 | assert property ((a s_until_with b) iff (a s_until_with b));
|
||||||
|
| ^~~~~~~~~~~~
|
||||||
|
%Error-UNSUPPORTED: t/t_property_unsup.v:127:46: Unsupported: s_until_with (in property expression)
|
||||||
|
127 | assert property ((a s_until_with b) iff (a s_until_with b));
|
||||||
|
| ^~~~~~~~~~~~
|
||||||
|
%Error-UNSUPPORTED: t/t_property_unsup.v:131:23: Unsupported: #-# (in property expression)
|
||||||
|
131 | assert property ((a #-# b) iff (a #-# b));
|
||||||
|
| ^~~
|
||||||
|
%Error-UNSUPPORTED: t/t_property_unsup.v:131:37: Unsupported: #-# (in property expression)
|
||||||
|
131 | assert property ((a #-# b) iff (a #-# b));
|
||||||
|
| ^~~
|
||||||
|
%Error: Exiting due to
|
||||||
|
|
@ -0,0 +1,18 @@
|
||||||
|
#!/usr/bin/env python3
|
||||||
|
# DESCRIPTION: Verilator: Verilog Test driver/expect definition
|
||||||
|
#
|
||||||
|
# Copyright 2025 by Wilson Snyder. 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-License-Identifier: LGPL-3.0-only OR Artistic-2.0
|
||||||
|
|
||||||
|
import vltest_bootstrap
|
||||||
|
|
||||||
|
test.scenarios('simulator')
|
||||||
|
|
||||||
|
test.lint(expect_filename=test.golden_filename,
|
||||||
|
verilator_flags2=['--assert', '--timing', '--error-limit 1000'],
|
||||||
|
fails=True)
|
||||||
|
|
||||||
|
test.passes()
|
||||||
|
|
@ -0,0 +1,133 @@
|
||||||
|
// (C) 2001-2020, Daniel Kroening, Edmund Clarke,
|
||||||
|
// Computer Science Department, University of Oxford
|
||||||
|
// Computer Science Department, Carnegie Mellon University
|
||||||
|
//
|
||||||
|
// All rights reserved. Redistribution and use in source and binary forms, with
|
||||||
|
// or without modification, are permitted provided that the following
|
||||||
|
// conditions are met:
|
||||||
|
//
|
||||||
|
// 1. Redistributions of source code must retain the above copyright
|
||||||
|
// notice, this list of conditions and the following disclaimer.
|
||||||
|
//
|
||||||
|
// 2. Redistributions in binary form must reproduce the above copyright
|
||||||
|
// notice, this list of conditions and the following disclaimer in the
|
||||||
|
// documentation and/or other materials provided with the distribution.
|
||||||
|
//
|
||||||
|
// 3. Neither the name of the University nor the names of its contributors
|
||||||
|
// may be used to endorse or promote products derived from this software
|
||||||
|
// without specific prior written permission.
|
||||||
|
//
|
||||||
|
// THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
|
||||||
|
// AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
|
||||||
|
// IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
|
||||||
|
// ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE
|
||||||
|
// LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
|
||||||
|
// CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
|
||||||
|
// SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
|
||||||
|
// INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
|
||||||
|
// CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
|
||||||
|
// ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
|
||||||
|
// POSSIBILITY OF SUCH DAMAGE.
|
||||||
|
//
|
||||||
|
// You can contact the author at:
|
||||||
|
// - homepage : https://www.cprover.org/ebmc/
|
||||||
|
// - source repository : https://github.com/diffblue/hw-cbmc
|
||||||
|
|
||||||
|
module t ( /*AUTOARG*/
|
||||||
|
// Inputs
|
||||||
|
clk,
|
||||||
|
reset
|
||||||
|
);
|
||||||
|
input clk;
|
||||||
|
input reset;
|
||||||
|
eventually1 eventually1 (.*);
|
||||||
|
eventually2 eventually2 (.*);
|
||||||
|
sva_implies2 sva_implies2 (.*);
|
||||||
|
sva_iff2 sva_iff2 (.*);
|
||||||
|
endmodule
|
||||||
|
|
||||||
|
module eventually1 (
|
||||||
|
input clk,
|
||||||
|
input reset
|
||||||
|
);
|
||||||
|
|
||||||
|
// count up from 0 to 10
|
||||||
|
reg [7:0] counter;
|
||||||
|
initial counter = 0;
|
||||||
|
|
||||||
|
always @(posedge clk) if (counter != 10) counter = counter + 1;
|
||||||
|
|
||||||
|
// expected to pass
|
||||||
|
p0 :
|
||||||
|
assert property (counter == 1 implies eventually[1: 2] counter == 3);
|
||||||
|
|
||||||
|
endmodule
|
||||||
|
|
||||||
|
module eventually2 (
|
||||||
|
input clk,
|
||||||
|
input reset
|
||||||
|
);
|
||||||
|
|
||||||
|
reg [7:0] counter;
|
||||||
|
initial counter = 0;
|
||||||
|
always @(posedge clk) counter = 0;
|
||||||
|
|
||||||
|
// expected to fail
|
||||||
|
p0 :
|
||||||
|
assert property (eventually[0: 2] counter == 3);
|
||||||
|
|
||||||
|
endmodule
|
||||||
|
|
||||||
|
module sva_implies2 (
|
||||||
|
input a,
|
||||||
|
b
|
||||||
|
);
|
||||||
|
|
||||||
|
p0 :
|
||||||
|
assert property ((always a) implies (always a));
|
||||||
|
p1 :
|
||||||
|
assert property ((a or(always b)) implies (a or(always b)));
|
||||||
|
p2 :
|
||||||
|
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 :
|
||||||
|
assert property ((a until_with b) implies (a until_with b));
|
||||||
|
p7 :
|
||||||
|
assert property ((a s_until_with b) implies (a s_until_with b));
|
||||||
|
p8 :
|
||||||
|
assert property ((a |-> b) implies (a |-> b));
|
||||||
|
p9 :
|
||||||
|
assert property ((a #-# b) implies (a #-# b));
|
||||||
|
|
||||||
|
endmodule
|
||||||
|
|
||||||
|
module sva_iff2 (
|
||||||
|
input a,
|
||||||
|
b
|
||||||
|
);
|
||||||
|
|
||||||
|
p0 :
|
||||||
|
assert property ((always a) iff (always a));
|
||||||
|
p1 :
|
||||||
|
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 :
|
||||||
|
assert property ((a until_with b) iff (a until_with b));
|
||||||
|
p6 :
|
||||||
|
assert property ((a s_until_with b) iff (a s_until_with b));
|
||||||
|
p7 :
|
||||||
|
assert property ((a |-> b) iff (a |-> b));
|
||||||
|
p8 :
|
||||||
|
assert property ((a #-# b) iff (a #-# b));
|
||||||
|
|
||||||
|
endmodule
|
||||||
Loading…
Reference in New Issue