T. Meissner
83d3e05757
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
T. Meissner
dd3b18ef41
Add formal verification of Wishbone components
5 years ago
T. Meissner
ea5a71fdff
Use generics to set vector lenghts instead of unconstrained vectors
5 years ago
T. Meissner
dd494f0901
New Wishbone checks; Fix illegal PSL property
* A lot of new checks are added to WishboneCheckerE unit
trying to implement the rules of the Wishbone spec.
* An illegal use of the suffix implication instead of logical
implicationis fixed in WishboneMasterE unit
6 years ago
T. Meissner
e953cda1d8
Refactoring Wishbone tests & design
* Add 1st initial version of WishBone checker unit
* Add Wishbone package with component & type declarations
* Replace WB slave register by dictionary
7 years ago
T. Meissner
4086876e14
Add assert for WB reset; add coverage of Local write/read
9 years ago
T. Meissner
c1005badfc
Add PSL assertions to check initiating of WishBone write/read transfer
WB_WRITE & WB_READ check that a write/read transfer is started on the
WishBone bus if requested on the local port of the WishBoneMasterE unit
at the adequate time.
9 years ago
T. Meissner
285a25132e
react to slave ack in ADDRESS state
10 years ago
T. Meissner
7d60f0ae1b
add simple wishbone master and slave with support of classic single write and read as specified in the wishbone spec b4; add unit tests for wishbone m,aster & slave
10 years ago