diff --git a/src/verilog.y b/src/verilog.y index d68171115..dfdcf3e80 100644 --- a/src/verilog.y +++ b/src/verilog.y @@ -6657,10 +6657,10 @@ pexpr: // IEEE: property_expr (The name pexpr is important as regex | ~o~pexpr yS_UNTIL_WITH pexpr { $$ = $1; BBUNSUP($2, "Unsupported: s_until_with (in property expression)"); } | ~o~pexpr yIMPLIES pexpr - { $$ = $1; BBUNSUP($2, "Unsupported: implies (in property expression)"); } + { $$ = new AstLogOr{$2, new AstLogNot{$2, $1}, $3}; } // // yIFF also used by event_expression | ~o~pexpr yIFF pexpr - { $$ = $1; BBUNSUP($2, "Unsupported: iff (in property expression)"); } + { $$ = new AstLogEq{$2, $1, $3}; } | yACCEPT_ON '(' expr/*expression_or_dist*/ ')' pexpr %prec yACCEPT_ON { $$ = $5; BBUNSUP($2, "Unsupported: accept_on (in property expression)"); } | yREJECT_ON '(' expr/*expression_or_dist*/ ')' pexpr %prec yREJECT_ON diff --git a/test_regress/t/t_property_pexpr.py b/test_regress/t/t_property_pexpr.py new file mode 100755 index 000000000..f989a35fb --- /dev/null +++ b/test_regress/t/t_property_pexpr.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.compile() + +test.execute() + +test.passes() diff --git a/test_regress/t/t_property_pexpr.v b/test_regress/t/t_property_pexpr.v new file mode 100644 index 000000000..7967fbfd2 --- /dev/null +++ b/test_regress/t/t_property_pexpr.v @@ -0,0 +1,76 @@ +// DESCRIPTION: Verilator: Verilog Test module +// +// This file ONLY is placed under the Creative Commons Public Domain, for +// any use, without warranty, 2025 by Wilson Snyder. +// SPDX-License-Identifier: CC0-1.0 + +`define stop $stop +`define checkh(gotv,expv) do if ((gotv) !== (expv)) begin $write("%%Error: %s:%0d: got=%0x exp=%0x (%s !== %s)\n", `__FILE__,`__LINE__, (gotv), (expv), `"gotv`", `"expv`"); `stop; end while(0); +`define checkd(gotv,expv) do if ((gotv) !== (expv)) begin $write("%%Error: %s:%0d: got=%0d exp=%0d\n", `__FILE__,`__LINE__, (gotv), (expv)); `stop; end while(0); + +module t(/*AUTOARG*/ + // Inputs + clk + ); + input clk; + + int cyc; + reg [63:0] crc; + + // Take CRC data and apply to testblock inputs + wire a = crc[0]; + wire b = crc[1]; + + /*AUTOWIRE*/ + + Test test(.*); + + // Test loop + always @(posedge clk) begin +`ifdef TEST_VERBOSE + $write("[%0t] cyc==%0d crc=%x result=%x\n", $time, cyc, crc); +`endif + cyc <= cyc + 1; + crc <= {crc[62:0], crc[63] ^ crc[2] ^ crc[0]}; + if (cyc == 0) begin + // Setup + crc <= 64'h5aef0c8d_d70a4497; + end + else if (cyc == 99) begin + `checkh(crc, 64'hc77bb9b3784ea091); + + // Result check + `checkd(test.count_hits_iff, 48); + `checkd(test.count_hits_implies, 24); + `checkd(test.count_hits_not, 47); + + $write("*-* All Finished *-*\n"); + $finish; + end + end + +endmodule + +module Test(input clk, + input int cyc, + input a, + input b); + + int count_hits_iff; + int count_hits_implies; + int count_hits_not; + + default disable iff cyc < 5; + + // property_expr1 iff property_expr2: true if (!property_expr1 && !property_expr2) || (property_expr1 && property_expr2) + assert property ( @(negedge clk) a iff b ) + else count_hits_iff = count_hits_iff + 1; + + // property_expr1 implies property_expr2: true if !property_expr1 || property_expr2 + assert property ( @(negedge clk) a implies b ) + else count_hits_implies = count_hits_implies + 1; + + assert property ( @(negedge clk) not a ) + else count_hits_not = count_hits_not + 1; + +endmodule diff --git a/test_regress/t/t_property_pexpr_unsup.out b/test_regress/t/t_property_pexpr_unsup.out index 52541ca1f..1744d8832 100644 --- a/test_regress/t/t_property_pexpr_unsup.out +++ b/test_regress/t/t_property_pexpr_unsup.out @@ -17,97 +17,91 @@ %Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:45:9: Unsupported: s_until_with (in property expression) 45 | a s_until_with b; | ^~~~~~~~~~~~ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:49:9: Unsupported: implies (in property expression) - 49 | a implies b; - | ^~~~~~~ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:53:9: Unsupported: #-# (in property expression) - 53 | a #-# b; +%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:49:9: Unsupported: #-# (in property expression) + 49 | a #-# b; | ^~~ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:57:9: Unsupported: #=# (in property expression) - 57 | a #=# b; +%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:53:9: Unsupported: #=# (in property expression) + 53 | a #=# b; | ^~~ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:61:7: Unsupported: nexttime (in property expression) - 61 | nexttime a; +%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:57:7: Unsupported: nexttime (in property expression) + 57 | nexttime a; | ^~~~~~~~ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:65:7: Unsupported: nexttime[] (in property expression) - 65 | nexttime [2] a; +%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:61:7: Unsupported: nexttime[] (in property expression) + 61 | nexttime [2] a; | ^~~~~~~~ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:69:7: Unsupported: s_nexttime (in property expression) - 69 | s_nexttime a; +%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:65:7: Unsupported: s_nexttime (in property expression) + 65 | s_nexttime a; | ^~~~~~~~~~ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:73:7: Unsupported: s_nexttime[] (in property expression) - 73 | s_nexttime [2] a; +%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:69:7: Unsupported: s_nexttime[] (in property expression) + 69 | s_nexttime [2] a; | ^~~~~~~~~~ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:77:16: Unsupported: always (in property expression) - 77 | nexttime always a; +%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:73:16: Unsupported: always (in property expression) + 73 | nexttime always a; | ^~~~~~ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:77:7: Unsupported: nexttime (in property expression) - 77 | nexttime always a; +%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:73:7: Unsupported: nexttime (in property expression) + 73 | nexttime 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:77:20: Unsupported: always (in property expression) + 77 | 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:77:7: Unsupported: nexttime[] (in property expression) + 77 | nexttime [2] always a; | ^~~~~~~~ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:85:16: Unsupported: eventually (in property expression) - 85 | nexttime eventually 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:85:7: Unsupported: nexttime (in property expression) - 85 | 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:89:20: Unsupported: always (in property expression) - 89 | nexttime [2] always 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:89:7: Unsupported: nexttime[] (in property expression) - 89 | 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:93:16: Unsupported: s_eventually (in property expression) - 93 | nexttime s_eventually 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:89:7: Unsupported: nexttime (in property expression) + 89 | nexttime s_eventually 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 a; + 93 | nexttime s_eventually [2:$] always a; | ^~~~~~~~ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:97:35: Unsupported: always (in property expression) - 97 | nexttime s_eventually [2:$] always a; - | ^~~~~~ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:97:16: Unsupported: s_eventually[] (in property expression) - 97 | nexttime s_eventually [2:$] always a; - | ^~~~~~~~~~~~ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:97:7: Unsupported: nexttime (in property expression) - 97 | nexttime s_eventually [2:$] always a; - | ^~~~~~~~ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:101:17: Unsupported: accept_on (in property expression) - 101 | accept_on (a) b; +%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:105:22: Unsupported: sync_accept_on (in property expression) - 105 | sync_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:109:17: Unsupported: reject_on (in property expression) - 109 | reject_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:113:22: Unsupported: sync_reject_on (in property expression) - 113 | sync_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:117:9: Unsupported: iff (in property expression) - 117 | a iff b; - | ^~~ -%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:120:27: Unsupported: property argument data type - 120 | property p_arg_propery(property inprop); +%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:123:27: Unsupported: sequence argument data type - 123 | property p_arg_seqence(sequence inseq); +%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:128:7: Unsupported: property case expression - 128 | 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:131:7: Unsupported: property case expression - 131 | case (a) default: b; 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:134:7: Unsupported: property case expression - 134 | if (a) b +%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:137:7: Unsupported: property case expression - 137 | if (a) b else c +%Error-UNSUPPORTED: t/t_property_pexpr_unsup.v:129:7: Unsupported: property case expression + 129 | 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 ec806a492..22c81989b 100644 --- a/test_regress/t/t_property_pexpr_unsup.v +++ b/test_regress/t/t_property_pexpr_unsup.v @@ -45,10 +45,6 @@ module t (/*AUTOARG*/ a s_until_with b; endproperty - property p_implies; - a implies b; - endproperty - property p_poundminuspound1; a #-# b; endproperty @@ -113,10 +109,6 @@ module t (/*AUTOARG*/ sync_reject_on (a) b; endproperty - property p_iff; - a iff b; - endproperty - property p_arg_propery(property inprop); inprop; endproperty