Examples of using PSL for functional and formal verification of VHDL with GHDL (and SymbiYosys)
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
 
 
T. Meissner e3a6fd38ab Add issue code for ghdl/ghdl#1658 2 months ago
.github/workflows Add GHA workflow for simulation tests 11 months ago
formal Add example for PSL abort operator 2 months ago
issues Add issue code for ghdl/ghdl#1658 2 months ago
sim Add example for PSL abort operator 2 months ago
src Add example for PSL abort operator 2 months ago
.gitignore Remove sublime text project files 2 months ago
LICENSE.md Add strong operator versions to unsupported list 12 months ago
README.md Add example for PSL abort operator 2 months ago

README.md

simulation formal

psl_with_ghdl

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

Supported by GHDL:

Directives

  • assert directive
  • cover directive
  • assume directive (synthesis)
  • restrict directive (synthesis)

Temporal operators (LTL style)

  • always operator
  • never operator
  • logical implication operator (->)
  • logical iff operator (<->)
  • next operator
  • next[n] operator
  • next_a[i to j] operator
  • next_e[i to j] operator
  • next_event operator
  • next_event[n] operator
  • next_event_e[i to j] operator
  • until operator
  • until_ operator
  • before operator (GHDL crash with a specific invalid property, see PSL before example)
  • eventually! operator

Sequential Extended Regular Expressions (SERE style)

  • Simple SERE
  • Concatenation operator (;)
  • Fusion operator (:)
  • Overlapping suffix implication operator (|->)
  • Non overlapping suffix implication operator (|=>)
  • Consecutive repetition operator ([*], [+], [*n], [*i to j])
  • Non consecutive repetition operator ([=n], [=i to j])
  • Non consecutive goto repetition operator ([->], [->n], [->i to j])
  • Length-matching and operator (&&)
  • Non-length-matching and operator (&)
  • or operator (|)
  • within operator

Built-in functions

  • prev() function (Synthesis only)
  • stable() function (Synthesis only)
  • rose() function (Synthesis only)
  • fell() function (Synthesis only)
  • onehot() function (Synthesis only)
  • onehot0() function (Synthesis only)

Convenient stuff

  • Partial support of PSL vunits (synthesis only)
  • Partial support of named sequences (simulation only)
  • Partial support of named properties (simulation only)
  • Partial support of PSL endpoint (simulation only, in PSL comments)

Yosys formal extensions (reference to Symbiyosys docs)

  • anyconst attribute (synthesis only)
  • anyseq attribute (synthesis only)

Not yet supported by GHDL:

  • forall operator
  • for operator
  • Synthesis of built-in functions countones(), isunknown()
  • Synthesis of strong operator versions
  • Synthesis of named sequences & properties
  • Simulation of built-in functions
  • Simulation of PSL vunits
  • PSL macros (%for, %if)
  • union expression

Supported, but under investigation

  • abort operator (Seems to be a sync_abort, while it has to be a async_abort)
  • before_ operator (Seems that LHS & RHS of operator have to be active at same cycle, see psl_before.vhd)
  • next_event_a[i to j] operator
  • eventually! behaviour with liveness proofs, see GHDL issue 1345

Further Ressources