tmeissner
/
psl_with_ghdl
1
0
Fork 0
Code Issues 0 Pull Requests 0 Releases 0 Wiki Activity
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.
13 Commits
1 Branch
6.6 MiB
 
 
Tree: 9e29e0631e
Branches Tags
${ item.name }
Create branch ${ searchTerm }
from '9e29e0631e'
${ noResults }
 ZIP  TAR.GZ
T. Meissner 9e29e0631e Add example for eventually! operator 5 years ago
.github/workflows Add Github actions config file & badge, fixes #2 5 years ago
formal Add example for eventually! operator 5 years ago
src Add example for eventually! operator 5 years ago
.gitignore Add gitignore file 5 years ago
LICENSE.md Initial commit: add license file 5 years ago
README.md Add example for eventually! operator 5 years ago

README.md

tests

psl_with_ghdl

A collection of examples of using PSL for functional and formal verification of VHDL with GHDL (and SymbiYosys).

The next two lists will grow during further development

PSL features supported by GHDL:

  • assert directive
  • cover directive
  • assume directive (synthesis)
  • restrict directive (synthesis)
  • always operator
  • never operator
  • implication operator
  • next operator
  • next[n] operator
  • next_event operator
  • next_event[n] operator
  • until operator
  • until_ operator
  • eventually! operator (simulation, synthesis throws an error)

PSL features not yet supported by GHDL:

  • next_a[i:j] operator
  • next_e[i:j] operator
  • next_event_a[i:j] operator
  • next_event_e[i:j] operator