[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