State of GHDL's support of PSL

[tmeissner]

This issue serves as a reference of the current state of GHDL's implementation of PSL. What's left and what are the most desired features. I take the information from my psl_with_ghdl repo and from issues which are marked with the psl tag.

Please check my psl_with_ghdl project for a more detailed list and examples which parts of PSL are supported by GHDL and which not. It would be tedious and wasteful work to copy and sync it into this issue.

I have to say, that the current PSL support is amazing, even if there are some features missing 👍 GHDL is the only free & open source tool I know with that wide support for Assertion Based Verification, even for use with formal methods (with SymbiYosys).

Hint: Support for synthesis means that it can also used for formal verification using SymbiYosys.

Currently not yet supported by GHDL:

I emphasized the features which I think are the most desired ones.

1. PSL functions (prev(), stable(),rose(), fell(), onehot()( & onehot0() are implemented for synthesis)
   Support of PSL functions #662 Supporting PSL functions for simulation #1498 Crash when using PSL stable in simulation #1530
2. PSL vunits (implemented for synthesis only)
   Not able to compile PSL verification unit file and bind to module.  #1027
3. Named properties & sequences (partial support, some parameter types missing)
   Allowing parameters for PSL sequences & properties #245 sem_psl_verification_unit: cannot handle IIR_KIND_PSL_DECLARATION #1889 Synth: add support for PSL declarations (sequences, properties) in inline PSL #1891
4. Using generic-derived constants
   Support generic-derived constants as "numbers" in PSL #600
5. Unclocked PSL
   Not able to compile PSL verification unit file and bind to module.  #1027
6. forall operator
   Request: PSL 'forall' support. #250
7. for operator
8. Synthesis of strong operator versions
9. PSL macros (%for, %if)
10. Multi-clock properties

I think the most desired thing is to streamline and align PSL support in simulation & synthesis. That is shown by point 1-3. Point 4 makes the life a lot easier when you want to check a lot of similar cases, as you could generate them using generate construct. It is also a workaround for missing forall, for operators and the macros.

Maybe we can have a discussion here - which features are realistic and easy to implement, which not.