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.

119 lines
5.6 KiB

  1. [![simulation](https://github.com/tmeissner/psl_with_ghdl/workflows/simulation/badge.svg)](https://github.com/tmeissner/psl_with_ghdl/actions?query=workflow%3Asimulation) [![formal](https://github.com/tmeissner/psl_with_ghdl/workflows/formal/badge.svg)](https://github.com/tmeissner/psl_with_ghdl/actions?query=workflow%3Aformal)
  2. # psl_with_ghdl
  3. 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)).
  4. 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.
  5. 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.
  6. 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.
  7. For example the `hdlc/formal:min` docker image provided by the [hdl containers project](https://hdl.github.io/containers/) (recommended). Or you build a docker image on your own machine using my [Dockerfiles for SymbiYosys & GHDL](https://github.com/tmeissner/Dockerfiles). With both you have the latest tool versions available.
  8. Have fun!
  9. The next lists will grow during further development
  10. ## Supported by GHDL:
  11. ### Directives
  12. * `assert` directive
  13. * `cover` directive
  14. * `assume` directive (synthesis)
  15. * `restrict` directive (synthesis)
  16. ### Temporal operators (LTL style)
  17. * `always` operator
  18. * `never` operator
  19. * logical implication operator (`->`)
  20. * logical iff operator (`<->`)
  21. * `next` operator
  22. * `next[n]` operator
  23. * `next_a[i to j]` operator
  24. * `next_e[i to j]` operator
  25. * `next_event` operator
  26. * `next_event[n]` operator
  27. * `next_event_e[i to j]` operator
  28. * `until` operator
  29. * `until_` operator
  30. * `before` operator (GHDL crash with a specific invalid property, see [PSL before example](https://github.com/tmeissner/psl_with_ghdl/blob/master/src/psl_before.vhd#L53))
  31. * `eventually!` operator
  32. ### Sequential Extended Regular Expressions (SERE style)
  33. * Simple SERE
  34. * Concatenation operator (`;`)
  35. * Fusion operator (`:`)
  36. * Overlapping suffix implication operator (`|->`)
  37. * Non overlapping suffix implication operator (`|=>`)
  38. * Consecutive repetition operator (`[*]`, `[+]`, `[*n]`, `[*i to j]`)
  39. * Non consecutive repetition operator (`[=n]`, `[=i to j]`)
  40. * Non consecutive goto repetition operator (`[->]`, `[->n]`, `[->i to j]`)
  41. * Length-matching and operator (`&&`)
  42. * Non-length-matching and operator (`&`)
  43. * or operator (`|`)
  44. * `within` operator
  45. ### Other operators
  46. * `abort` operator
  47. * `async_abort` operator
  48. * `sync_abort` operator
  49. ### Built-in functions
  50. * `prev()` function (Synthesis only)
  51. * `stable()` function (Synthesis only)
  52. * `rose()` function (Synthesis only)
  53. * `fell()` function (Synthesis only)
  54. * `onehot()` function (Synthesis only)
  55. * `onehot0()` function (Synthesis only)
  56. ### Convenient stuff
  57. * Partial support of PSL vunits (synthesis only)
  58. * Partial support of named sequences (some parameter types missing)
  59. * Partial support of named properties (some parameter types missing)
  60. * Partial support of PSL `endpoint` (simulation only, in PSL comments)
  61. * vunit inhiterance (`inherit`, synthesis only)
  62. ### Yosys formal extensions (reference to [Symbiyosys docs](https://symbiyosys.readthedocs.io/en/latest/verilog.html#unconstrained-variables))
  63. * `anyconst` attribute (synthesis only)
  64. * `anyseq` attribute (synthesis only)
  65. ## Not yet supported by GHDL:
  66. * `forall` operator
  67. * `for` operator
  68. * Synthesis of built-in functions `countones()`, `isunknown()`
  69. * Synthesis of strong operator versions
  70. * Simulation of built-in functions
  71. * Simulation of PSL vunits
  72. * PSL macros (`%for`, `%if`)
  73. * `union` expression
  74. ## Supported, but under investigation
  75. * `before_` operator (Seems that LHS & RHS of operator have to be active at same cycle, see psl_before.vhd)
  76. * `next_event_a[i to j]` operator
  77. * `eventually!` behaviour with liveness proofs, see [GHDL issue 1345](https://github.com/ghdl/ghdl/issues/1345)
  78. ## Further Ressources
  79. * [Wikipedia about PSL](https://en.wikipedia.org/wiki/Property_Specification_Language)
  80. * [Doulos Designer's Guide To PSL](https://www.doulos.com/knowhow/psl/)
  81. * [Project VeriPage PSL Tutorial](http://www.project-veripage.com/psl_tutorial_1.php)
  82. * [FirstEDA Blog - An Introduction to Assertion-Based Verification](https://firsteda.com/news/an-introduction-to-assertion-based-verification-part-1)
  83. * [FirstEDA Blog - Achieving Better Coverage with VHDL](https://firsteda.com/news/achieving-better-coverage-with-vhdl-part-2)
  84. * [1850-2010 - IEEE Standard for PSL](https://standards.ieee.org/standard/1850-2010.html)
  85. * [A Practical Introduction to PSL Book](https://www.springer.com/gp/book/9780387361239)
  86. * [Formal Verification Book](https://www.elsevier.com/books/formal-verification/seligman/978-0-12-800727-3)
  87. * [PSL Specification for WISHBONE System-on-Chip (from the PROSYD project)](https://opencores.org/websvn/filedetails?repname=copyblaze&path=%2Fcopyblaze%2Ftrunk%2Fcopyblaze%2Fdoc%2Fdev%2FWishBone%2Fprosyd1.4_1_annex.pdf)
  88. * [GHDL documentation](https://ghdl.readthedocs.io)
  89. * [SymbiYosys documentation](https://symbiyosys.readthedocs.io)