psl_with_ghdl

Author	SHA1	Message	Date
T. Meissner	356f6a1678	Add example for SERE within operator	5 years ago
T. Meissner	4dd0f1b33c	Fixed assertion - combining SEREs isn't trivial ;)	5 years ago
T. Meissner	f6088fd9f2	Add some more links to ressources	5 years ago
T. Meissner	42e8e49bb0	Add example for cover directive	5 years ago
T. Meissner	f9233c605b	Add links to further ressources	5 years ago
T. Meissner	d2db77183e	Fix SERE, replacing within with && operator	5 years ago
T. Meissner	3e0daf5e51	Add SERE goto [->n] operator, was fixed by ghdl/ghdl#1322	5 years ago
T. Meissner	0a044db5d0	Fixed entity & file names of [=] examples	5 years ago
T. Meissner	97773515b8	Add SERE repeat [=n] operator, was fixed by ghdl/ghdl#1321	5 years ago
T. Meissner	f2b3d9d9ee	Add issue code for goto ([->]) operator (ghdl/ghdl#1322 )	5 years ago
T. Meissner	d9c8f521d4	Add issue code for [=n] operator (ghdl/ghdl#1321 )	5 years ago
T. Meissner	0595fd8afa	Add more repetition asserts; add comments	5 years ago
T. Meissner	9dc78f37c9	Simplify sequencer by removing intermediate character signal	5 years ago
T. Meissner	cd6c6449c2	Update next_event_a example to fixed ghdl/ghdl#1314	5 years ago
T. Meissner	8c273a68cf	Issues can be built using make now	5 years ago
T. Meissner	b57e7d842e	Addd code for (fixed) issues ghdl/ghdl#1288 & ghdl/ghdl#1292	5 years ago
T. Meissner	c26a90c588	Add code for issue ghdl/ghdl#1314	5 years ago
T. Meissner	d68ea88578	Add more asserts using variants of [*]	5 years ago
T. Meissner	e2ee755833	Add example for consecutive repetition operator and variants * Add example for [], [i to j], [] and [+] operator variants Add formal test for consecutive repetition operator example * Add consecutive repetition operator to supported list	5 years ago
T. Meissner	78013a2d4e	Change sby task name from prove to bmc (we do bmc, not unbounded prove)	5 years ago
T. Meissner	d346840704	Add example for \|=> (non overlapping suffix implication) operator * Add example for \|=> operator * Add formal test for \|=> operator example * Add \|=> to supported list	5 years ago
T. Meissner	3b669b037b	Add example for \|-> (overlapping suffix implication) operator * Add example for \|-> operator * Add formal test for \|-> operator example * Add \|-> to supported list	5 years ago
T. Meissner	1a7a3e9f68	Add example for simple SERE * Add example for simple SERE * Add formal test for simple SERE example * Restructure lists in README	5 years ago
T. Meissner	1a37ad78be	Add example for locical implication * Add example for -> operator * Add formal test for -> operator example * Sort entries in README lists	5 years ago
T. Meissner	54b2791f47	Add strong operator versions to unsupported list	5 years ago
T. Meissner	9437d2d272	Add more failing assertions (should hold, assuming GHDL bug) to next_event_a example	5 years ago
T. Meissner	2fdf7d99e3	PSL next_event_e operator now supported by GHDL :)	5 years ago
T. Meissner	1f01afb1a1	Add examples for not yet working next_event_a & next_event_e operators	5 years ago
T. Meissner	e744ab3a1b	Add some infos about getting the tools used by the tests	5 years ago
T. Meissner	d766f79dc6	Add some more waveforms & asserts to PSL next_a example	5 years ago
T. Meissner	44f6dc1f1c	PSL next_e operator now supported by GHDL :)	5 years ago
T. Meissner	b9bc7270af	Add example for next_e operator * Add example for next_e operator * Add formal test for next_e operator example	5 years ago
T. Meissner	2e64182dda	Add example for next_a operator * Add example for next_a operator * Add formal test for next_a operator example * Move next_a from unsupported to supported list	5 years ago
T. Meissner	fb993953cb	Minor fixes, beauty care * Minor fixes to README * Add psl_before & psl_eventually to formal test list	5 years ago
T. Meissner	5c8ced0752	Add examples of before & before_ operators * Add example for before & before_ operator * Add formal test for both operators * Add before operator to supported list * Add before_ operator to wrong behaviour list	5 years ago
T. Meissner	9e29e0631e	Add example for eventually! operator * Add example for eventually! operator * Add formal test for eventually! operator (throws an error during synthesis) * Add eventually! to supported list with hint to failing synthesis	5 years ago
T. Meissner	ffe07fd5b4	Add example of until & until_ operators * Add example for until & until_ operator * Add formal test for both operators * Add both operators to supported list	5 years ago
T. Meissner	5e5be8afe6	Add gitignore file	5 years ago
T. Meissner	105d44d7d0	Add example for next_event[n] operator * Add example for next_event[n] operator * Add formal test for next_event[n] operator * Add next_event[n] to supported list * Add next_event_a[n] & next_event_e[n] to unsupported list	5 years ago
T. Meissner	dec05012d7	Handle ambiguous PLS/VHDL assert, add some hints	5 years ago
T. Meissner	c23f3b4736	Add Github actions config file & badge, fixes #2	5 years ago
T. Meissner	00ac16a888	Add tests for formal verification; optimizations; fixes #3 * Minor optimization in sequencer unit * Add Makefile & SymbiYosys command files for formal verification tests	5 years ago
T. Meissner	0923a44b44	Add example for next_event operator	5 years ago
T. Meissner	c6028fd198	Add example for next_event operator	5 years ago
T. Meissner	96c459e027	Add readme and psl_next, psl_next[] operators	5 years ago
T. Meissner	c223fc2037	Add 4-bit version of sequencer	5 years ago
T. Meissner	263dcae830	Add sequencer and first examples * sequencer for easy waveform generation of simple 1 bit std_logic signals * Package with sequencer component delaration * Examples for always & never operator	5 years ago
T. Meissner	dd500a736f	Initial commit: add license file	5 years ago

48 Commits (356f6a16784b7e7b2e268b4ac4812165323c3f34) All Branches Search

48 Commits (356f6a16784b7e7b2e268b4ac4812165323c3f34)

All Branches