Skip to content

Commit 2c17ab8

Browse files
committed
SVA: add tests for #-# and #=#
This adds tests for the SVA followed-by operators.
1 parent 8bbc75e commit 2c17ab8

File tree

2 files changed

+17
-0
lines changed

2 files changed

+17
-0
lines changed
Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
followed-by2.sv
3+
--bound 20
4+
^\[main\.p0\] always \(\(main\.a #-# main\.b\) iff \(not \(main\.a |-> \(not main\.b\)\)\)\): FAILURE: property not supported by BMC engine$
5+
^\[main\.p1\] always \(\(main\.a #=# main\.b\) iff \(not \(main\.a |=> \(not main\.b\)\)\)\): FAILURE: property not supported by BMC engine$
6+
^EXIT=10$
7+
^SIGNAL=0$
8+
--
9+
^warning: ignoring
10+
--
Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
module main(input clk, input a, input b);
2+
3+
// equivalences from 1800 2017 16.12.9
4+
p0: assert property ((a #-# b) iff (not (a |-> not b)));
5+
p1: assert property ((a #=# b) iff (not (a |=> not b)));
6+
7+
endmodule

0 commit comments

Comments
 (0)