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