T. Meissner
9b34289045
Add example for SERE length mathcing and (&&) operator
5 years ago
T. Meissner
cee1bcf8aa
Add another assertion to the SERE or example
5 years ago
T. Meissner
eaf03a8be8
Add example for SERE or (|) operator
5 years ago
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