From f9233c605bf86b73c5b345a60aeb986d9cee30d2 Mon Sep 17 00:00:00 2001 From: tmeissner Date: Mon, 18 May 2020 17:34:44 +0200 Subject: [PATCH] Add links to further ressources --- README.md | 15 +++++++++++---- 1 file changed, 11 insertions(+), 4 deletions(-) diff --git a/README.md b/README.md index bf1a3c7..e06f911 100644 --- a/README.md +++ b/README.md @@ -2,7 +2,7 @@ # psl_with_ghdl -A collection of examples of using PSL for functional and formal verification of VHDL with GHDL (and SymbiYosys). +A collection of examples of using [PSL](https://en.wikipedia.org/wiki/Property_Specification_Language) for functional and formal verification of VHDL designs with [GHDL](https://github.com/ghdl/ghdl) (and [Yosys](https://github.com/YosysHQ/yosys) / [SymbiYosys](https://github.com/YosysHQ/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. @@ -17,7 +17,7 @@ Have fun! The next lists will grow during further development -## PSL features supported by GHDL: +## Supported by GHDL: ### Directives @@ -54,12 +54,19 @@ The next lists will grow during further development * Length-matching and operator (&&) * within operator -## PSL features not yet supported by GHDL: +## Not yet supported by GHDL: * forall statement * Synthesis of strong operator versions -## PSL features under investigation +## Under investigation * 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 + +## Further Ressources + +* [Wikipedia about PSL](https://en.wikipedia.org/wiki/Property_Specification_Language) +* [Doulos Designer's Guide To PSL](https://www.doulos.com/knowhow/psl/) +* [Project VeriPage PSL Tutorial](http://www.project-veripage.com/psl_tutorial_1.php) +* [1850-2010 - IEEE Standard for PSL](https://standards.ieee.org/standard/1850-2010.html)