-
Notifications
You must be signed in to change notification settings - Fork 9
/
Copy pathcheck.sby
50 lines (46 loc) · 1.18 KB
/
check.sby
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
[tasks]
prop_unique
prop_exact
prop_exactConditions
prop_getBase
prop_getTop
prop_getLength
prop_isInBounds
prop_setAddr
prop_fromToMem
[options]
depth 1
mode bmc
[engines]
smtbmc boolector
[script]
read -formal assertions.sv
read -formal module_prop_unique.v
read -formal module_prop_exact.v
read -formal module_prop_exactConditions.v
read -formal module_prop_getBase.v
read -formal module_prop_getTop.v
read -formal module_prop_getLength.v
read -formal module_prop_isInBounds.v
read -formal module_prop_setAddr.v
read -formal module_prop_fromToMem.v
prop_getBase: prep -top assert_prop_getBase
prop_getTop: prep -top assert_prop_getTop
prop_getLength: prep -top assert_prop_getLength
prop_isInBounds: prep -top assert_prop_isInBounds
prop_unique: prep -top assert_prop_unique
prop_exact: prep -top assert_prop_exact
prop_exactConditions: prep -top assert_prop_exactConditions
prop_setAddr: prep -top assert_prop_setAddr
prop_fromToMem: prep -top assert_prop_fromToMem
[files]
assertions.sv
module_prop_unique.v
module_prop_exact.v
module_prop_exactConditions.v
module_prop_getBase.v
module_prop_getTop.v
module_prop_getLength.v
module_prop_isInBounds.v
module_prop_setAddr.v
module_prop_fromToMem.v