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