diff --git a/src/verilog.y b/src/verilog.y index bc535ad1d..38821427b 100644 --- a/src/verilog.y +++ b/src/verilog.y @@ -6311,7 +6311,9 @@ property_port_itemDirE: ; property_declarationBody: // IEEE: part of property_declaration - assertion_variable_declarationList + assertion_variable_declarationList property_spec + { $$ = nullptr; BBUNSUP($1->fileline(), "Unsupported: property variable declaration"); DEL($1); } + | assertion_variable_declarationList property_spec ';' { $$ = nullptr; BBUNSUP($1->fileline(), "Unsupported: property variable declaration"); DEL($1); } // // IEEE-2012: Incorrectly has yCOVER ySEQUENCE then property_spec here. // // Fixed in IEEE 1800-2017 @@ -6384,6 +6386,8 @@ property_spec: // IEEE: property_spec { $$ = new AstPropSpec{$1, $3, $8, $10}; } | '@' '(' senitem ')' pexpr { $$ = new AstPropSpec{$1, $3, nullptr, $5}; } + | '@' senitemVar pexpr + { $$ = new AstPropSpec{$1, $2, nullptr, $3}; } // // Disable applied after the event occurs, // // so no existing AST can represent this | yDISABLE yIFF '(' expr ')' '@' '(' senitemEdge ')' pexpr @@ -6567,7 +6571,7 @@ sexpr: // ==IEEE: sequence_expr (The name sexpr is important as reg // // IEEE: "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: - cycle_delay_range sexpr %prec yP_POUNDPOUND + cycle_delay_range ~p~sexpr %prec yP_POUNDPOUND { $$ = $2; BBUNSUP($2->fileline(), "Unsupported: ## (in sequence expression)"); } | ~p~sexpr cycle_delay_range sexpr %prec prPOUNDPOUND_MULTI { $$ = $1; BBUNSUP($2->fileline(), "Unsupported: ## (in sequence expression)"); } @@ -6589,7 +6593,8 @@ sexpr: // ==IEEE: sequence_expr (The name sexpr is important as reg // // '(' sequence_expr {',' sequence_match_item } ')' [ boolean_abbrev ] // // "'(' sexpr ')' boolean_abbrev" matches "[sexpr:'(' expr ')'] boolean_abbrev" so we can drop it | '(' ~p~sexpr ')' { $$ = $2; } - //UNSUP '(' ~p~sexpr ',' sequence_match_itemList ')' { } + | '(' ~p~sexpr ',' sequence_match_itemList ')' + { $$ = $2; BBUNSUP($3, "Unsupported sequence match items"); } // // // AND/OR are between pexprs OR sexprs | ~p~sexpr yAND ~p~sexpr diff --git a/test_regress/t/t_property_pexpr.v b/test_regress/t/t_property_pexpr.v index 7967fbfd2..aff72bfc9 100644 --- a/test_regress/t/t_property_pexpr.v +++ b/test_regress/t/t_property_pexpr.v @@ -28,7 +28,7 @@ module t(/*AUTOARG*/ // Test loop always @(posedge clk) begin `ifdef TEST_VERBOSE - $write("[%0t] cyc==%0d crc=%x result=%x\n", $time, cyc, crc); + $write("[%0t] cyc==%0d crc=%x\n", $time, cyc, crc); `endif cyc <= cyc + 1; crc <= {crc[62:0], crc[63] ^ crc[2] ^ crc[0]}; @@ -43,12 +43,17 @@ module t(/*AUTOARG*/ `checkd(test.count_hits_iff, 48); `checkd(test.count_hits_implies, 24); `checkd(test.count_hits_not, 47); + `checkd(test.count_hits_event, 1); $write("*-* All Finished *-*\n"); $finish; end end + always @(negedge clk) begin + if (cyc == 10) -> test.e; + end + endmodule module Test(input clk, @@ -59,6 +64,8 @@ module Test(input clk, int count_hits_iff; int count_hits_implies; int count_hits_not; + int count_hits_event; + event e; default disable iff cyc < 5; @@ -73,4 +80,6 @@ module Test(input clk, assert property ( @(negedge clk) not a ) else count_hits_not = count_hits_not + 1; + assert property ( @e not a ) + else count_hits_event = count_hits_event + 1; endmodule diff --git a/test_regress/t/t_property_sexpr_unsup.out b/test_regress/t/t_property_sexpr_unsup.out new file mode 100644 index 000000000..aa80d23e8 --- /dev/null +++ b/test_regress/t/t_property_sexpr_unsup.out @@ -0,0 +1,122 @@ +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:46:35: Unsupported: ## () cycle delay range expression + 46 | assert property (@(posedge clk) ##2 val) + | ^~ + ... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:46:39: Unsupported: ## (in sequence expression) + 46 | assert property (@(posedge clk) ##2 val) + | ^~~ +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:49:35: Unsupported: ## () cycle delay range expression + 49 | assert property (@(posedge clk) ##1 1 |=> 0) + | ^~ +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:49:39: Unsupported: ## (in sequence expression) + 49 | assert property (@(posedge clk) ##1 1 |=> 0) + | ^ +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:52:35: Unsupported: ## () cycle delay range expression + 52 | assert property (@(posedge clk) ##1 1 |=> not (val)) + | ^~ +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:52:39: Unsupported: ## (in sequence expression) + 52 | assert property (@(posedge clk) ##1 1 |=> not (val)) + | ^ +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:55:35: Unsupported: ## () cycle delay range expression + 55 | assert property (@(posedge clk) ##1 val) + | ^~ +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:55:39: Unsupported: ## (in sequence expression) + 55 | assert property (@(posedge clk) ##1 val) + | ^~~ +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:58:35: Unsupported: ## () cycle delay range expression + 58 | assert property (@(posedge clk) ##1 (val)) + | ^~ +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:58:40: Unsupported: ## (in sequence expression) + 58 | assert property (@(posedge clk) ##1 (val)) + | ^~~ +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:61:36: Unsupported: ## () cycle delay range expression + 61 | assert property (@(posedge clk) (##1 (val))) + | ^~ +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:61:41: Unsupported: ## (in sequence expression) + 61 | assert property (@(posedge clk) (##1 (val))) + | ^~~ +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:64:36: Unsupported: ## () cycle delay range expression + 64 | assert property (@(posedge clk) (##1 (val))) + | ^~ +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:64:41: Unsupported: ## (in sequence expression) + 64 | assert property (@(posedge clk) (##1 (val))) + | ^~~ +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:67:40: Unsupported: ## () cycle delay range expression + 67 | assert property (@(posedge clk) not (##1 val)) + | ^~ +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:67:44: Unsupported: ## (in sequence expression) + 67 | assert property (@(posedge clk) not (##1 val)) + | ^~~ +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:70:35: Unsupported: ## () cycle delay range expression + 70 | assert property (@(posedge clk) ##1 1 |=> 1) + | ^~ +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:70:39: Unsupported: ## (in sequence expression) + 70 | assert property (@(posedge clk) ##1 1 |=> 1) + | ^ +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:73:35: Unsupported: ## () cycle delay range expression + 73 | assert property (@(posedge clk) ##1 val |=> not val) + | ^~ +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:73:39: Unsupported: ## (in sequence expression) + 73 | assert property (@(posedge clk) ##1 val |=> not val) + | ^~~ +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:76:35: Unsupported: ## () cycle delay range expression + 76 | assert property (@(posedge clk) ##1 (val) |=> not (val)) + | ^~ +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:76:40: Unsupported: ## (in sequence expression) + 76 | assert property (@(posedge clk) ##1 (val) |=> not (val)) + | ^~~ +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:82:57: Unsupported: ## () cycle delay range expression + 82 | assert property (@(posedge clk) disable iff (cyc < 3) ##1 1 |=> cyc > 3) + | ^~ +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:82:61: Unsupported: ## (in sequence expression) + 82 | assert property (@(posedge clk) disable iff (cyc < 3) ##1 1 |=> cyc > 3) + | ^ +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:85:36: Unsupported: ## () cycle delay range expression + 85 | assert property (@(posedge clk) (##1 val) |=> (##1 val)) + | ^~ +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:85:40: Unsupported: ## (in sequence expression) + 85 | assert property (@(posedge clk) (##1 val) |=> (##1 val)) + | ^~~ +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:85:50: Unsupported: ## () cycle delay range expression + 85 | assert property (@(posedge clk) (##1 val) |=> (##1 val)) + | ^~ +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:85:54: Unsupported: ## (in sequence expression) + 85 | assert property (@(posedge clk) (##1 val) |=> (##1 val)) + | ^~~ +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:103:14: Unsupported sequence match items + 103 | ($rose(a), l_b = b) |-> ##[3:10] q[l_b]; + | ^ +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:103:29: Unsupported: ## range cycle delay range expression + 103 | ($rose(a), l_b = b) |-> ##[3:10] q[l_b]; + | ^~ +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:103:39: Unsupported: ## (in sequence expression) + 103 | ($rose(a), l_b = b) |-> ##[3:10] q[l_b]; + | ^ +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:102:13: Unsupported: property variable declaration + 102 | integer l_b; + | ^~~ +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:120:16: Unsupported sequence match items + 120 | (count == 0, l_t = $realtime) ##1 (count == 7)[->1] |-> $realtime - l_t < 50.5; + | ^ +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:120:35: Unsupported: ## () cycle delay range expression + 120 | (count == 0, l_t = $realtime) ##1 (count == 7)[->1] |-> $realtime - l_t < 50.5; + | ^~ +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:120:51: Unsupported: [-> boolean abbrev expression + 120 | (count == 0, l_t = $realtime) ##1 (count == 7)[->1] |-> $realtime - l_t < 50.5; + | ^~~ +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:120:54: Unsupported: boolean abbrev (in sequence expression) + 120 | (count == 0, l_t = $realtime) ##1 (count == 7)[->1] |-> $realtime - l_t < 50.5; + | ^ +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:120:37: Unsupported: ## (in sequence expression) + 120 | (count == 0, l_t = $realtime) ##1 (count == 7)[->1] |-> $realtime - l_t < 50.5; + | ^ +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:118:14: Unsupported: property variable declaration + 118 | realtime l_t; + | ^~~ +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:124:31: Unsupported: ## () cycle delay range expression + 124 | assert property (@clk not a ##1 b); + | ^~ +%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:124:33: Unsupported: ## (in sequence expression) + 124 | assert property (@clk not a ##1 b); + | ^ +%Error: Exiting due to diff --git a/test_regress/t/t_property_sexpr_unsup.py b/test_regress/t/t_property_sexpr_unsup.py new file mode 100755 index 000000000..c8e1cbe53 --- /dev/null +++ b/test_regress/t/t_property_sexpr_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('vlt') + +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_sexpr_unsup.v b/test_regress/t/t_property_sexpr_unsup.v new file mode 100644 index 000000000..00379507a --- /dev/null +++ b/test_regress/t/t_property_sexpr_unsup.v @@ -0,0 +1,125 @@ +// DESCRIPTION: Verilator: Verilog Test module +// +// This file ONLY is placed into the Public Domain, for any use, +// without warranty, 2025 by Antmicro. +// SPDX-License-Identifier: CC0-1.0 + +module t ( /*AUTOARG*/ + // Inputs + clk +); + + input clk; + integer cyc = 1; + bit val = 0; + + Test test ( /*AUTOINST*/ + // Inputs + .clk(clk), + .val(val), + .cyc(cyc) + ); + + Ieee ieee(); + + always @(posedge clk) begin + if (cyc != 0) begin + cyc <= cyc + 1; + val = ~val; +`ifdef TEST_VERBOSE + $display("cyc=%0d, val=%0d", cyc, val); +`endif + if (cyc == 10) begin + $write("*-* All Finished *-*\n"); + $finish; + end + end + end +endmodule + +module Test ( + input clk, + input bit val, + input integer cyc +); + + assert property (@(posedge clk) ##2 val) + else $display("[%0t] assertion triggered, fileline:%d", $time, `__LINE__); + + assert property (@(posedge clk) ##1 1 |=> 0) + else $display("[%0t] assertion triggered, fileline:%d", $time, `__LINE__); + + assert property (@(posedge clk) ##1 1 |=> not (val)) + else $display("[%0t] assertion triggered, fileline:%d", $time, `__LINE__); + + assert property (@(posedge clk) ##1 val) + else $display("[%0t] assertion triggered, fileline:%d", $time, `__LINE__); + + assert property (@(posedge clk) ##1 (val)) + else $display("[%0t] assertion triggered, fileline:%d", $time, `__LINE__); + + assert property (@(posedge clk) (##1 (val))) + else $display("[%0t] assertion triggered, fileline:%d", $time, `__LINE__); + + assert property (@(posedge clk) (##1 (val))) + else $display("[%0t] assertion triggered, fileline:%d", $time, `__LINE__); + + assert property (@(posedge clk) not (##1 val)) + else $display("[%0t] assertion triggered, fileline:%d", $time, `__LINE__); + + assert property (@(posedge clk) ##1 1 |=> 1) + else $display("[%0t] assertion triggered, fileline:%d", $time, `__LINE__); + + assert property (@(posedge clk) ##1 val |=> not val) + else $display("[%0t] assertion triggered, fileline:%d", $time, `__LINE__); + + assert property (@(posedge clk) ##1 (val) |=> not (val)) + else $display("[%0t] assertion triggered, fileline:%d", $time, `__LINE__); + + assert property (@(posedge clk) ((val) |=> not (val))) + else $display("[%0t] assertion triggered, fileline:%d", $time, `__LINE__); + + assert property (@(posedge clk) disable iff (cyc < 3) ##1 1 |=> cyc > 3) + else $display("[%0t] assertion triggered, fileline:%d", $time, `__LINE__); + + assert property (@(posedge clk) (##1 val) |=> (##1 val)) + else $display("[%0t] assertion triggered, fileline:%d", $time, `__LINE__); +endmodule + +// Test parsing only +module Ieee; + // IEEE 1800-2023 16.6 + bit a; + integer b; + byte q[$]; + logic clk; + + property p1; + $rose(a) |-> q[0]; + endproperty + + property p2; + integer l_b; + ($rose(a), l_b = b) |-> ##[3:10] q[l_b]; + endproperty + + bit [2:0] count = 0; + realtime t; + always @(posedge clk) begin + if (count == 0) t = $realtime; + count++; + end + property p3; + @(posedge clk) + count == 7 |-> $realtime - t < 50.5; + endproperty + + property p4; + realtime l_t; + @(posedge clk) + (count == 0, l_t = $realtime) ##1 (count == 7)[->1] |-> $realtime - l_t < 50.5; + endproperty + + // IEEE 1800-2023 16.12.3 + assert property (@clk not a ##1 b); +endmodule diff --git a/test_regress/t/t_property_var_unsup.out b/test_regress/t/t_property_var_unsup.out index 9790a8e62..1ce9a82b4 100644 --- a/test_regress/t/t_property_var_unsup.out +++ b/test_regress/t/t_property_var_unsup.out @@ -1,11 +1,10 @@ +%Error-UNSUPPORTED: t/t_property_var_unsup.v:18:13: Unsupported sequence match items + 18 | (valid, prevcyc = cyc) |=> (cyc == prevcyc + 1); + | ^ + ... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest %Error-UNSUPPORTED: t/t_property_var_unsup.v:17:11: Unsupported: property variable declaration 17 | int prevcyc; | ^~~~~~~ - ... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest -%Error: t/t_property_var_unsup.v:18:7: syntax error, unexpected '(', expecting endproperty - 18 | (valid, prevcyc = cyc) |=> (cyc == prevcyc + 1); - | ^ - ... See the manual at https://verilator.org/verilator_doc.html?v=latest for more assistance. %Error-UNSUPPORTED: t/t_property_var_unsup.v:24:31: Unsupported: property variable default value 24 | property with_def(int nine = 9); | ^