File tree Expand file tree Collapse file tree 6 files changed +124
-147
lines changed Expand file tree Collapse file tree 6 files changed +124
-147
lines changed Original file line number Diff line number Diff line change 1
1
CORE
2
2
eventually1.sv
3
3
--bound 20
4
- ^\[main\.p0\] always main\.counter == 1 implies \(eventually \[1:2\] main\.counter == 3\): PROVED up to bound 20$
4
+ ^\[main\.p0\] always \( main\.counter == 1 implies \(eventually \[1:2\] main\.counter == 3\) \): PROVED up to bound 20$
5
5
^EXIT=0$
6
6
^SIGNAL=0$
7
7
--
Original file line number Diff line number Diff line change 1
1
CORE
2
2
sva_and1.sv
3
3
--bound 0
4
- ^\[main\.p0\] always 1 and 1: PROVED up to bound 0$
5
- ^\[main\.p1\] always 1 and 0: REFUTED$
6
- ^\[main\.p2\] always 1 and 32'b0000000000000000000000000000000x: PROVED up to bound 0$
4
+ ^\[main\.p0\] always \( 1 and 1\) : PROVED up to bound 0$
5
+ ^\[main\.p1\] always \( 1 and 0\) : REFUTED$
6
+ ^\[main\.p2\] always \( 1 and 32'b0000000000000000000000000000000x\) : PROVED up to bound 0$
7
7
^EXIT=10$
8
8
^SIGNAL=0$
9
9
--
Original file line number Diff line number Diff line change 1
1
CORE
2
2
sva_iff1.sv
3
3
--bound 0
4
- ^\[main\.p0\] always 1 iff 1: PROVED up to bound 0$
5
- ^\[main\.p1\] always 1 iff 0: REFUTED$
6
- ^\[main\.p2\] always 1 iff 32'b0000000000000000000000000000000x: PROVED up to bound 0$
4
+ ^\[main\.p0\] always \( 1 iff 1\) : PROVED up to bound 0$
5
+ ^\[main\.p1\] always \( 1 iff 0\) : REFUTED$
6
+ ^\[main\.p2\] always \( 1 iff 32'b0000000000000000000000000000000x\) : PROVED up to bound 0$
7
7
^EXIT=10$
8
8
^SIGNAL=0$
9
9
--
Original file line number Diff line number Diff line change 1
1
CORE
2
2
sva_implies1.sv
3
3
--bound 0
4
- ^\[main\.p0\] always 1 implies 1: PROVED up to bound 0$
5
- ^\[main\.p1\] always 1 implies 0: REFUTED$
6
- ^\[main\.p2\] always 1 implies 32'b0000000000000000000000000000000x: PROVED up to bound 0$
4
+ ^\[main\.p0\] always \( 1 implies 1\) : PROVED up to bound 0$
5
+ ^\[main\.p1\] always \( 1 implies 0\) : REFUTED$
6
+ ^\[main\.p2\] always \( 1 implies 32'b0000000000000000000000000000000x\) : PROVED up to bound 0$
7
7
^EXIT=10$
8
8
^SIGNAL=0$
9
9
--
You can’t perform that action at this time.
0 commit comments