Support implication operator "|->" in assertions, #2069.

Signed-off-by: Wilson Snyder <wsnyder@wsnyder.org>
This commit is contained in:
Peter Monsson 2019-12-23 16:49:18 -05:00 committed by Wilson Snyder
parent 0f0c3d4684
commit 9b998cf6b3
5 changed files with 118 additions and 4 deletions

View File

@ -6,6 +6,8 @@ The contributors that suggested a given feature are shown in []. Thanks!
*** Support bounded queues.
*** Support implication operator "|->" in assertions, #2069. [Peter Monsson]
*** Support string compare, ato*, etc methods, #1606. [Yutetsu TAKATSUKASA]
**** Support immediate cover statements.

View File

@ -4254,13 +4254,21 @@ elseStmtBlock<nodep>: // Part of concurrent_assertion_statement
property_spec<nodep>: // IEEE: property_spec
//UNSUP: This rule has been super-specialized to what is supported now
'@' '(' senitemEdge ')' yDISABLE yIFF '(' expr ')' expr
'@' '(' senitemEdge ')' yDISABLE yIFF '(' expr ')' property_expr
{ $$ = new AstPropClocked($1, $3, $8, $10); }
| '@' '(' senitemEdge ')' expr { $$ = new AstPropClocked($1, $3, NULL, $5); }
| yDISABLE yIFF '(' expr ')' expr { $$ = new AstPropClocked($4->fileline(), NULL, $4, $6); }
| expr { $$ = new AstPropClocked($1->fileline(), NULL, NULL, $1); }
| '@' '(' senitemEdge ')' property_expr { $$ = new AstPropClocked($1, $3, NULL, $5); }
| yDISABLE yIFF '(' expr ')' property_expr { $$ = new AstPropClocked($4->fileline(), NULL, $4, $6); }
| property_expr { $$ = new AstPropClocked($1->fileline(), NULL, NULL, $1); }
;
property_expr<nodep>: // IEEE: property_expr
//UNSUP: This rule has been super-specialized to what is supported now
expr yP_ORMINUSGT property_expr { $$ = new AstLogOr($2,new AstLogNot($2,$1),$3); }
//UNSUP expr yP_OREQGT property_expr { $$ = new AstLogOr($2,new AstLogNot($2,new AstPast($2,$1, NULL)),$3); } // This handles disable iff in the past time step incorrectly
| expr { $$ = $1; }
;
//************************************************
// Let

View File

@ -0,0 +1,21 @@
#!/usr/bin/perl
if (!$::Driver) { use FindBin; exec("$FindBin::Bin/bootstrap.pl", @ARGV, $0); die; }
# DESCRIPTION: Verilator: Verilog Test driver/expect definition
#
# Copyright 2003-2009 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.
scenarios(simulator => 1);
compile(
verilator_flags2 => ['--assert --cc'],
);
execute(
check_finished => 1,
);
ok(1);
1;

View File

@ -0,0 +1,57 @@
// DESCRIPTION: Verilator: Verilog Test module
//
// This file ONLY is placed into the Public Domain, for any use,
// without warranty, 2019 by Peter Monsson.
module t (/*AUTOARG*/
// Inputs
clk
);
input clk;
integer cyc; initial cyc=1;
Test test (/*AUTOINST*/
// Inputs
.clk (clk));
always @ (posedge clk) begin
if (cyc!=0) begin
cyc <= cyc + 1;
if (cyc==10) begin
$write("*-* All Finished *-*\n");
$finish;
end
end
end
endmodule
module Test
(
input clk
);
`ifdef FAIL_ASSERT_1
assert property (
@(posedge clk)
1 |-> 0
) else $display("[%0t] wrong implication", $time);
`endif
assert property (
@(posedge clk)
1 |-> 1
);
assert property (
@(posedge clk)
0 |-> 0
);
assert property (
@(posedge clk)
0 |-> 1
);
endmodule

View File

@ -0,0 +1,26 @@
#!/usr/bin/perl
if (!$::Driver) { use FindBin; exec("$FindBin::Bin/bootstrap.pl", @ARGV, $0); die; }
# DESCRIPTION: Verilator: Verilog Test driver/expect definition
#
# Copyright 2003-2009 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.
scenarios(simulator => 1);
top_filename("t/t_assert_implication.v");
compile(
v_flags2 => ['+define+FAIL_ASSERT_1'],
verilator_flags2 => ['--assert --cc'],
);
execute(
);
# We expect to get a message when this assert fires:
file_grep($Self->{run_log_filename}, qr/wrong implication/);
ok(1);
1;