tmeissner
/
libvhdl
1
0
Fork 0
Code Issues 0 Pull Requests 0 Releases 0 Activity
Library of reusable VHDL components
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
124 Commits
2 Branches
914 KiB
Tree: 9fb10aaf47
Branches Tags
${ item.name }
Create branch ${ searchTerm }
from '9fb10aaf47'
${ noResults }
libvhdl/formal/WishBoneSlaveE.sby

24 lines
582 B
Raw Normal View History

Add formal verification of Wishbone components
5 years ago
Add bmc mode; integrate simulation PSL checks * Add BMC mode to formal tests * Adapt wishbone simulation testbench to new generics * Integrate simulation PSL checks in Wishbone components * Add generic for Simulation PSL checks to Wishbone components
5 years ago
Add formal verification of Wishbone components
5 years ago
​
​
​
​
Add bmc mode; integrate simulation PSL checks * Add BMC mode to formal tests * Adapt wishbone simulation testbench to new generics * Integrate simulation PSL checks in Wishbone components * Add generic for Simulation PSL checks to Wishbone components
5 years ago
Add formal verification of Wishbone components
5 years ago
​
​
​
Add bmc mode; integrate simulation PSL checks * Add BMC mode to formal tests * Adapt wishbone simulation testbench to new generics * Integrate simulation PSL checks in Wishbone components * Add generic for Simulation PSL checks to Wishbone components
5 years ago
Add formal verification of Wishbone components
5 years ago
​
​
​
Add bmc mode; integrate simulation PSL checks * Add BMC mode to formal tests * Adapt wishbone simulation testbench to new generics * Integrate simulation PSL checks in Wishbone components * Add generic for Simulation PSL checks to Wishbone components
5 years ago
​
​
Add formal verification of Wishbone components
5 years ago
​
​
​
 
  1. [tasks]
  2. bmc
  3. prove
  4. cover
  5. 

  6. [options]
  7. depth 25
  8. bmc: mode bmc
  9. prove: mode prove
  10. cover: mode cover
  11. 

  12. [engines]
  13. bmc: smtbmc z3
  14. prove: abc pdr
  15. cover: smtbmc z3
  16. 

  17. [script]
  18. bmc: ghdl --std=08 -gFormal=true -gSimulation=false -gAddressWidth=32 -gDataWidth=32 WishBoneSlaveE.vhd -e wishboneslavee
  19. prove: ghdl --std=08 -gFormal=true -gSimulation=false -gAddressWidth=32 -gDataWidth=32 WishBoneSlaveE.vhd -e wishboneslavee
  20. cover: ghdl --std=08 -gFormal=true -gSimulation=false -gAddressWidth=32 -gDataWidth=32 WishBoneSlaveE.vhd -e wishboneslavee
  21. prep -auto-top
  22. 

  23. [files]
  24. ../syn/WishBoneSlaveE.vhd