diff --git a/src/verilog.y b/src/verilog.y index ca53c686c..768db997a 100644 --- a/src/verilog.y +++ b/src/verilog.y @@ -6334,9 +6334,9 @@ property_port_itemDirE: property_declarationBody: // IEEE: part of property_declaration 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 ';' - { $$ = 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. // // Fixed in IEEE 1800-2017 | property_spec { $$ = $1; } @@ -6445,14 +6445,16 @@ property_spec: // IEEE: property_spec property_statementCaseIf: // IEEE: property_statement - minus pexpr yCASE '(' expr/*expression_or_dist*/ ')' property_case_itemList yENDCASE { $$ = new AstConst{$1, AstConst::BitFalse{}}; - BBUNSUP($1, "Unsupported: property case expression"); } + BBUNSUP($1, "Unsupported: property case expression"); + DEL($3, $5); } | yCASE '(' expr/*expression_or_dist*/ ')' yENDCASE { $$ = new AstConst{$1, AstConst::BitFalse{}}; - BBUNSUP($1, "Unsupported: property case expression"); } + BBUNSUP($1, "Unsupported: property case expression"); + DEL($3); } | yIF '(' expr/*expression_or_dist*/ ')' pexpr %prec prLOWER_THAN_ELSE - { $$ = $5; BBUNSUP($1, "Unsupported: property case expression"); } + { $$ = $5; BBUNSUP($1, "Unsupported: property case expression"); DEL($3); } | yIF '(' expr/*expression_or_dist*/ ')' pexpr yELSE pexpr - { $$ = $5; BBUNSUP($1, "Unsupported: property case expression"); } + { $$ = $5; BBUNSUP($1, "Unsupported: property case expression"); DEL($3, $7); } ; property_case_itemList: // IEEE: {property_case_item} @@ -6523,9 +6525,9 @@ pexpr: // IEEE: property_expr (The name pexpr is important as regex | property_statementCaseIf { $$ = $1; } // | ~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 - { $$ = $3; BBUNSUP($2, "Unsupported: #=# (in property expression)"); } + { $$ = $1; BBUNSUP($2, "Unsupported: #=# (in property expression)"); DEL($3); } | yNEXTTIME pexpr { $$ = $2; BBUNSUP($1, "Unsupported: nexttime (in property expression)"); } | yS_NEXTTIME pexpr @@ -6540,22 +6542,20 @@ pexpr: // IEEE: property_expr (The name pexpr is important as regex { $$ = $3; BBUNSUP($1, "Unsupported: always[] (in property expression)"); DEL($2); } | yS_ALWAYS anyrange pexpr %prec yS_ALWAYS { $$ = $3; BBUNSUP($1, "Unsupported: s_always (in property expression)"); DEL($2); } - | yEVENTUALLY pexpr - { $$ = $2; BBUNSUP($1, "Unsupported: eventually (in property expression)"); } | yS_EVENTUALLY pexpr { $$ = $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 { $$ = $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 - { $$ = $1; BBUNSUP($2, "Unsupported: until (in property expression)"); } + { $$ = $1; BBUNSUP($2, "Unsupported: until (in property expression)"); DEL($3); } | ~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 - { $$ = $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 - { $$ = $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 { $$ = new AstLogOr{$2, new AstLogNot{$2, $1}, $3}; } // // yIFF also used by event_expression @@ -6594,15 +6594,15 @@ sexpr: // ==IEEE: sequence_expr (The name sexpr is important as reg // // 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: 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 - { $$ = $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 ] // // Note expression_or_dist includes "expr"! // // sexpr/*sexpression_or_dist*/ --- Hardcoded below | ~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 ]" // // version without sequence_abbrev looks just like normal function call @@ -6616,7 +6616,7 @@ sexpr: // ==IEEE: sequence_expr (The name sexpr is important as reg // // "'(' sexpr ')' boolean_abbrev" matches "[sexpr:'(' expr ')'] boolean_abbrev" so we can drop it | '(' ~p~sexpr ')' { $$ = $2; } | '(' ~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 | ~p~sexpr yAND ~p~sexpr @@ -6627,18 +6627,18 @@ sexpr: // ==IEEE: sequence_expr (The name sexpr is important as reg BBUNSUP($2, "Unsupported: or (in sequence expression)"); } // // Intersect always has an sexpr rhs | ~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 ')' - { $$ = 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 ')' - { $$ = 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 - { $$ = $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 // // IEEE: 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 //UNSUP clocking_event ~p~sexpr %prec prSEQ_CLOCKING { } // @@ -6664,7 +6664,7 @@ cycle_delay_range: // IEEE: ==cycle_delay_range // // the sv-ac committee has been asked to clarify (Mantis 1901) | yP_POUNDPOUND anyrange { $$ = new AstConst{$1, AstConst::BitFalse{}}; - BBUNSUP($1, "Unsupported: ## range cycle delay range expression"); } + BBUNSUP($1, "Unsupported: ## range cycle delay range expression"); DEL($2); } | yP_POUNDPOUND yP_BRASTAR ']' { $$ = new AstConst{$1, AstConst::BitFalse{}}; BBUNSUP($1, "Unsupported: ## [*] cycle delay range expression"); } @@ -6691,7 +6691,7 @@ boolean_abbrev: // ==IEEE: boolean_abbrev yP_BRASTAR constExpr ']' { $$ = $2; BBUNSUP($1, "Unsupported: [*] boolean abbrev expression"); } | yP_BRASTAR constExpr ':' constExpr ']' - { $$ = $2; BBUNSUP($1, "Unsupported: [*] boolean abbrev expression"); } + { $$ = $2; BBUNSUP($1, "Unsupported: [*] boolean abbrev expression"); DEL($4); } | yP_BRASTAR ']' { $$ = new AstConst{$1, AstConst::BitFalse{}}; BBUNSUP($1, "Unsupported: [*] boolean abbrev expression"); } @@ -6702,12 +6702,12 @@ boolean_abbrev: // ==IEEE: boolean_abbrev | yP_BRAEQ constExpr ']' { $$ = $2; BBUNSUP($1, "Unsupported: [= boolean abbrev expression"); } | yP_BRAEQ constExpr ':' constExpr ']' - { $$ = $2; BBUNSUP($1, "Unsupported: [= boolean abbrev expression"); } + { $$ = $2; BBUNSUP($1, "Unsupported: [= boolean abbrev expression"); DEL($4); } // // IEEE: goto_repetition | yP_BRAMINUSGT constExpr ']' { $$ = $2; BBUNSUP($1, "Unsupported: [-> boolean abbrev expression"); } | yP_BRAMINUSGT constExpr ':' constExpr ']' - { $$ = $2; BBUNSUP($1, "Unsupported: [-> boolean abbrev expression"); } + { $$ = $2; BBUNSUP($1, "Unsupported: [-> boolean abbrev expression"); DEL($4); } ; //************************************************ diff --git a/test_regress/t/t_assert_always_unsup.out b/test_regress/t/t_assert_always_unsup.out index 018505ca2..2e537171c 100644 --- a/test_regress/t/t_assert_always_unsup.out +++ b/test_regress/t/t_assert_always_unsup.out @@ -5,9 +5,22 @@ %Error-UNSUPPORTED: t/t_assert_always_unsup.v:25:7: Unsupported: s_always (in property expression) 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; - | ^ - ... See the manual at https://verilator.org/verilator_doc.html?v=latest for more assistance. -%Error: Cannot continue - ... This fatal error may be caused by the earlier error(s); resolve those first. + | ^~~~~~~~~~ +%Error-UNSUPPORTED: t/t_assert_always_unsup.v:33:7: Unsupported: s_eventually[] (in property expression) + 33 | s_eventually [2:5] a; + | ^~~~~~~~~~~~ +%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 diff --git a/test_regress/t/t_assert_always_unsup.v b/test_regress/t/t_assert_always_unsup.v index 32f96aec1..f273e5493 100644 --- a/test_regress/t/t_assert_always_unsup.v +++ b/test_regress/t/t_assert_always_unsup.v @@ -1,7 +1,7 @@ // DESCRIPTION: Verilator: Verilog Test module // // 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 module t (/*AUTOARG*/ @@ -29,10 +29,6 @@ module t (/*AUTOARG*/ eventually [2:5] a; endproperty - property p_ev2; - eventually [2] a; - endproperty - property p_s_ev; s_eventually [2:5] a; endproperty diff --git a/test_regress/t/t_dist_copyright.py b/test_regress/t/t_dist_copyright.py index d2efab4f1..283f77a42 100755 --- a/test_regress/t/t_dist_copyright.py +++ b/test_regress/t/t_dist_copyright.py @@ -43,6 +43,7 @@ EXEMPT_FILES_LIST = """ test_regress/t/t_flag_f__3.v test_regress/t/t_fuzz_eof_bad.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_inc.v test_regress/t/uvm/dpi diff --git a/test_regress/t/t_property_pexpr_unsup.out b/test_regress/t/t_property_pexpr_unsup.out index 1744d8832..fb003c30c 100644 --- a/test_regress/t/t_property_pexpr_unsup.out +++ b/test_regress/t/t_property_pexpr_unsup.out @@ -47,61 +47,55 @@ %Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:77:7: Unsupported: nexttime[] (in property expression) 77 | nexttime [2] always a; | ^~~~~~~~ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:81:16: Unsupported: eventually (in property expression) - 81 | nexttime eventually 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:81:20: Unsupported: always (in property expression) + 81 | nexttime [2] always a; | ^~~~~~ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:85:7: Unsupported: nexttime[] (in property expression) - 85 | nexttime [2] always a; +%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:81:7: Unsupported: nexttime[] (in property expression) + 81 | nexttime [2] always a; | ^~~~~~~~ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:89:16: Unsupported: s_eventually (in property expression) - 89 | nexttime s_eventually a; +%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:85:16: Unsupported: s_eventually (in property expression) + 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) - 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) - 93 | nexttime s_eventually [2:$] always a; - | ^~~~~~ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:93:16: Unsupported: s_eventually[] (in property expression) - 93 | nexttime s_eventually [2:$] always a; - | ^~~~~~~~~~~~ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:93:7: Unsupported: nexttime (in property expression) - 93 | nexttime s_eventually [2:$] always a; - | ^~~~~~~~ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:97:17: Unsupported: accept_on (in property expression) - 97 | accept_on (a) b; +%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:93:17: Unsupported: accept_on (in property expression) + 93 | accept_on (a) b; | ^ -%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:97:22: Unsupported: sync_accept_on (in property expression) + 97 | 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:101:17: Unsupported: reject_on (in property expression) + 101 | 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:105:22: Unsupported: sync_reject_on (in property expression) + 105 | 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:108:27: Unsupported: property argument data type + 108 | property p_arg_propery(property inprop); | ^~~~~~~~ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:115:27: Unsupported: sequence argument data type - 115 | property p_arg_seqence(sequence inseq); +%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:111:27: Unsupported: sequence argument data type + 111 | property p_arg_seqence(sequence inseq); | ^~~~~~~~ -%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:116:7: Unsupported: property case expression + 116 | case (a) endcase | ^~~~ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:123:7: Unsupported: property case expression - 123 | case (a) default: b; endcase +%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:119:7: Unsupported: property case expression + 119 | case (a) default: b; endcase | ^~~~ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:126:7: Unsupported: property case expression - 126 | if (a) b +%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:122:7: Unsupported: property case expression + 122 | if (a) b | ^~ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:129:7: Unsupported: property case expression - 129 | if (a) b else c +%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:125:7: Unsupported: property case expression + 125 | 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 22c81989b..e8143e993 100644 --- a/test_regress/t/t_property_pexpr_unsup.v +++ b/test_regress/t/t_property_pexpr_unsup.v @@ -77,10 +77,6 @@ module t (/*AUTOARG*/ nexttime [2] always a; endproperty - property p_nexttime_eventually; - nexttime eventually a; - endproperty - property p_nexttime_eventually2; nexttime [2] always a; endproperty diff --git a/test_regress/t/t_property_unsup.out b/test_regress/t/t_property_unsup.out new file mode 100644 index 000000000..4a00f5d06 --- /dev/null +++ b/test_regress/t/t_property_unsup.out @@ -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 diff --git a/test_regress/t/t_property_unsup.py b/test_regress/t/t_property_unsup.py new file mode 100755 index 000000000..9acc8bd21 --- /dev/null +++ b/test_regress/t/t_property_unsup.py @@ -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() diff --git a/test_regress/t/t_property_unsup.v b/test_regress/t/t_property_unsup.v new file mode 100644 index 000000000..aaee26c34 --- /dev/null +++ b/test_regress/t/t_property_unsup.v @@ -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