You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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.
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.
The text was updated successfully, but these errors were encountered:
tmeissner
changed the title
PSL: State of GHDL's support for PSL
State of GHDL's support for PSL
Jan 18, 2021
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.
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
Not able to compile PSL verification unit file and bind to module. #1027
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
Support generic-derived constants as "numbers" in PSL #600
Not able to compile PSL verification unit file and bind to module. #1027
forall
operatorRequest: PSL 'forall' support. #250
for
operator%for
,%if
)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 missingforall
,for
operators and the macros.Maybe we can have a discussion here - which features are realistic and easy to implement, which not.
The text was updated successfully, but these errors were encountered: