Skip to content

Commit 7505b1a

Browse files
committed
Instrument $past when generating SMV word level
This removes Verilog's $past when outputting SMV word level, which does not have an equivalent of $past.
1 parent 94015fc commit 7505b1a

File tree

2 files changed

+14
-0
lines changed

2 files changed

+14
-0
lines changed
Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
verilog5.sv
3+
--smv-word-level
4+
^INIT ebmc::\$past1@1 = FALSE$
5+
^TRANS next\(ebmc::\$past1@1\) = main\.in$
6+
^LTLSPEC G main\.in = \(X ebmc::\$past1@1\)$
7+
^EXIT=0$
8+
^SIGNAL=0$
9+
--
Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
module main(input clk, input in);
2+
3+
p1: assert property (in iff s_nexttime $past(in));
4+
5+
endmodule

0 commit comments

Comments
 (0)