[tasks]
prop_unique
prop_exact
prop_exactConditions
prop_getBase
prop_getTop
prop_getLength
prop_isInBounds
prop_setAddr

[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
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

[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