T. Meissner 1b04fcf4c4 | 2 years ago | |
---|---|---|
.github/workflows | 5 years ago | |
formal | 3 years ago | |
issues | 2 years ago | |
sim | 4 years ago | |
src | 2 years ago | |
.gitignore | 4 years ago | |
LICENSE.md | 5 years ago | |
README.md | 2 years ago |
A collection of examples of using PSL for functional and formal verification of VHDL designs with GHDL (and Yosys / SymbiYosys).
This is a project with the purpose to get a current state of PSL implementation in GHDL. It probably will find unsupported PSL features, incorrect implemented features or simple bugs like GHDL crashs.
It is also intended for experiments with PSL when learning the language. You can play around with the examples, as they are pretty simple. You can comment out failing assertions if you want to have a successful proof or simulation if you want. You can change them to see what happens.
It is recommended to use an up-to-date version of GHDL as potential bugs are fixed very quickly. Especially the synthesis feature of GHDL is very new and still beta. You can build GHDL from source or use one of the Docker images which contain also the SymbiYosys toolchain.
For example the hdlc/formal:min
docker image provided by the hdl containers project (recommended). Or you build a docker image on your own machine using my Dockerfiles for SymbiYosys & GHDL. With both you have the latest tool versions available.
Have fun!
The next lists will grow during further development
assert
directivecover
directiveassume
directive (synthesis)restrict
directive (synthesis)always
operatornever
operator->
)<->
)next
operatornext[n]
operatornext_a[i to j]
operatornext_e[i to j]
operatornext_event
operatornext_event[n]
operatornext_event_e[i to j]
operatoruntil
operatoruntil_
operatorbefore
operator (GHDL crash with a specific invalid property, see PSL before example)eventually!
operator;
):
)|->
)|=>
)[*]
, [+]
, [*n]
, [*i to j]
)[=n]
, [=i to j]
)[->]
, [->n]
, [->i to j]
)&&
)&
)|
)within
operatorabort
operatorasync_abort
operatorsync_abort
operatorprev()
function (Synthesis only)stable()
function (Synthesis only)rose()
function (Synthesis only)fell()
function (Synthesis only)onehot()
function (Synthesis only)onehot0()
function (Synthesis only)endpoint
(simulation only, in PSL comments)inherit
, synthesis only)anyconst
attribute (synthesis only)anyseq
attribute (synthesis only)forall
operatorfor
operatorcountones()
, isunknown()
%for
, %if
)union
expressioneventually!
behaviour with liveness proofs, see GHDL issue 1345