Adding support for the SVA implication operator. For partial fix of issue #1292.

This commit is contained in:
Peter Monsson 2019-12-23 20:24:59 +01:00
parent c1fb938a61
commit 5b841937e8
3 changed files with 104 additions and 0 deletions

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("wrong implication");
`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;