Examples of using PSL for functional and formal verification of VHDL with GHDL (and SymbiYosys)

[tmeissner]

ref: https://github.com/tmeissner/psl_with_ghdl
tags: [psl, ghdl, yosys, verification, formal-verification, assertions, symbiyosys, functional-coverage]
repo: tmeissner/psl_with_ghdl

A collection of examples of using PSL (Property Specification Language) 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.