Support property `iff` and `implies`.
This commit is contained in:
Wilson Snyder
parent
26c7f1adb6
commit
5a6d5ed96b
|
|
@ -6657,10 +6657,10 @@ pexpr<nodeExprp>: // 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
|
||||
|
|
|
|||
|
|
@ -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()
|
||||
|
|
@ -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
|
||||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Reference in New Issue