[tasks]
bmc
prf
cvr

[options]
bmc: mode bmc
bmc: depth 50
prf: mode prove
prf: depth 17
cvr: mode cover
cvr: depth 90	# 72 should be sufficient
multiclock on

[engines]
smtbmc

[script]
~prf: read -formal -DBMC wbxclk.v
prf:  read -formal       wbxclk.v
read -formal afifo.v
read -formal fwb_slave.v
read -formal fwb_master.v
cvr: hierarchy -top wbxclk -chparam LGFIFO 3
prep -top wbxclk

[files]
../../rtl/afifo.v
../../rtl/wbxclk.v
fwb_slave.v
fwb_master.v