54 lines
1.4 KiB
Plaintext
54 lines
1.4 KiB
Plaintext
[tasks]
|
|
prop_unique
|
|
prop_exact
|
|
prop_exactConditions
|
|
prop_getBase
|
|
prop_getTop
|
|
prop_getLength
|
|
prop_isInBounds
|
|
prop_setAddr
|
|
prop_fromToMem
|
|
prop_setBounds
|
|
|
|
[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
|
|
read -formal module_prop_setBounds.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
|
|
prop_setBounds: prep -top assert_prop_setBounds
|
|
|
|
[files]
|
|
assertions.sv
|
|
counterexamples/module_prop_unique.v
|
|
counterexamples/module_prop_exact.v
|
|
counterexamples/module_prop_exactConditions.v
|
|
counterexamples/module_prop_getBase.v
|
|
counterexamples/module_prop_getTop.v
|
|
counterexamples/module_prop_getLength.v
|
|
counterexamples/module_prop_isInBounds.v
|
|
counterexamples/module_prop_setAddr.v
|
|
counterexamples/module_prop_fromToMem.v
|