libvhdl

914 KiB

Author	SHA1	Message	Date
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	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	6659dbbe31	Fix PSL assertions for local wen and local ren The second logical implication was made the whole property holding when the part after the 1st implication didn't hold. So, the 2nd implication is replaced by an and in combination with the next operator. Now the property fails when one of the two and'ed parts after the implication fails.	9 years ago
T. Meissner	021bab3762	Add PSL assertions to check WishBone & Local IF Various new PSL assertions to check ports during Wishbone write & read transfer and reset state	9 years ago
T. Meissner	f0e490142e	moved register write into ADDRESS state, decreasing the write to one cycle only	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

8 Commits (eacf18cc49ac3d73b5741da5d4294b3dfb14052e)