[tasks]
prf4x8_buflp	nxm opt_dblbuffer opt_lowpower
prf4x8_buf	nxm opt_dblbuffer
prf4x8_lp       nxm               opt_lowpower
prf4x8_cheap    nxm
cvr4x8_buflp	nxm opt_dblbuffer opt_lowpower cvr
cvr4x8_buf	nxm opt_dblbuffer              cvr
cvr4x8_lp       nxm               opt_lowpower cvr
cvr4x8_cheap    nxm                            cvr
prf4x8_buflpko	nxm opt_dblbuffer opt_lowpower opt_timeout
prf4x8_bufko	nxm opt_dblbuffer              opt_timeout
prf4x8_lpko     nxm               opt_lowpower opt_timeout
prf4x8_cheapko  nxm                            opt_timeout
prf4x8_buflpkos	nxm opt_dblbuffer opt_lowpower opt_timeout opt_starvation
prf4x8_bufkos	nxm opt_dblbuffer              opt_timeout opt_starvation
prf4x8_lpkos    nxm               opt_lowpower opt_timeout opt_starvation
prf4x8_cheapkos nxm                            opt_timeout opt_starvation
prf1x8_buflp	oxm opt_dblbuffer opt_lowpower
prf1x8_buf	oxm opt_dblbuffer
prf1x8_lp       oxm               opt_lowpower
prf1x8_cheap    oxm
cvr1x3_buflp	oxl opt_dblbuffer opt_lowpower cvr
cvr1x3_buf	oxl opt_dblbuffer              cvr
cvr1x3_lp       oxl               opt_lowpower cvr
cvr1x3_cheap    oxl                            cvr
prf1x8_buflpko	oxm opt_dblbuffer opt_lowpower opt_timeout
prf1x8_bufko	oxm opt_dblbuffer              opt_timeout
prf1x8_lpko     oxm               opt_lowpower opt_timeout
prf1x8_cheapko  oxm                            opt_timeout
prf1x8_buflpkos	oxm opt_dblbuffer opt_lowpower opt_timeout opt_starvation
prf1x8_bufkos	oxm opt_dblbuffer              opt_timeout opt_starvation
prf1x8_lpkos    oxm               opt_lowpower opt_timeout opt_starvation
prf1x8_cheapkos oxm                            opt_timeout opt_starvation
prf4x1_buflp	nxo opt_dblbuffer opt_lowpower
prf4x1_buf	nxo opt_dblbuffer
prf4x1_lp       nxo               opt_lowpower
prf4x1_cheap    nxo
cvr4x1_buflp	nxo opt_dblbuffer opt_lowpower cvr
cvr4x1_buf	nxo opt_dblbuffer              cvr
cvr4x1_lp       nxo               opt_lowpower cvr
cvr4x1_cheap    nxo                            cvr
prf4x1_buflpko	nxo opt_dblbuffer opt_lowpower opt_timeout
prf4x1_bufko	nxo opt_dblbuffer              opt_timeout
prf4x1_lpko     nxo               opt_lowpower opt_timeout
prf4x1_cheapko  nxo                            opt_timeout
prf4x1_buflpkos	nxo opt_dblbuffer opt_lowpower opt_timeout opt_starvation
prf4x1_bufkos	nxo opt_dblbuffer              opt_timeout opt_starvation
prf4x1_lpkos    nxo               opt_lowpower opt_timeout opt_starvation
prf4x1_cheapkos nxo                            opt_timeout opt_starvation

[options]
~cvr: mode prove
~cvr: depth 6
cvr: mode cover
cvr: depth 64

[engines]
smtbmc boolector
# smtbmc yices
# smtbmc z3


[script]
read -formal addrdecode.v
read -formal skidbuffer.v
read -formal wbxbar.v
read -formal fwb_slave.v
read -formal fwb_master.v
--pycode-begin--
cmd = "hierarchy -top wbxbar"
if ("nxm" in tags):
	cmd += " -chparam  NM 4 -chparam NS 8"
if ("oxm" in tags):
	cmd += " -chparam  NM 1 -chparam NS 8"
if ("oxl" in tags):
	cmd += " -chparam  NM 1 -chparam NS 3"
if ("nxo" in tags):
	cmd += " -chparam  NM 4 -chparam NS 1"
cmd += " -chparam OPT_DBLBUFFER %d" % (1  if "opt_dblbuffer" in tags else 0)
cmd += " -chparam OPT_LOWPOWER  %d" % (1  if "opt_lowpower"  in tags else 0)
cmd += " -chparam OPT_TIMEOUT   %d" % (20 if "opt_timeout"   in tags else 0)
cmd += " -chparam OPT_STARVATION_TIMEOUT %d" % (1 if "opt_starvation" in tags else 0)
output(cmd)
--pycode-end--
prep -top wbxbar

[files]
../../rtl/skidbuffer.v
../../rtl/addrdecode.v
../../rtl/wbxbar.v
fwb_slave.v
fwb_master.v