Trying to verify Verilog/VHDL designs with formal methods and tools
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.

34 lines
2.7 KiB

6 years ago
6 years ago
6 years ago
  1. [![](https://img.shields.io/github/workflow/status/tmeissner/formal_hw_verification/Test/master?longCache=true&style=flat-square&label=Test&logo=GitHub%20Actions&logoColor=fff)](https://github.com/tmeissner/formal_hw_verification/actions?query=workflow%3ATest)
  2. The original repository is located on my own git-server at [https://git.goodcleanfun.de/tmeissner/formal_hw_verification](https://git.goodcleanfun.de/tmeissner/formal_hw_verification)
  3. It is mirrored to github with every push, so both should be in sync.
  4. # formal_hw_verification
  5. Tests and examples of using formal verification to check correctness of digital hardware designs. All tests are done with [SymbiYosys](https://github.com/YosysHQ/SymbiYosys), a front-end for formal verification flows based on [Yosys](https://github.com/YosysHQ/yosys).
  6. All stuff in the master branch uses [ghdl-yosys-plugin](https://github.com/ghdl/ghdl-yosys-plugin) and [GHDL](https://github.com/ghdl/ghdl) as VHDL front-end plugin for (Symbi)Yosys. Using GHDL as synthesis frontend allows using PSL as verification language.
  7. Some examples in the [verific branch](https://github.com/tmeissner/formal_hw_verification/tree/verific) use the commercial VHDL/SystemVerilog frontend plugin by Verific which isn't free SW and not included in the free Yosys version. See on the [Symbiotic EDA website](https://www.symbioticeda.com) for more information.
  8. You can use the `hdlc/formal:all` 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.
  9. ### alu
  10. A simple ALU design in VHDL. The formal checks contain various simple properties used by assert & cover directives which are proved with the SymbiYosys tool.
  11. ### counter
  12. A simple counter design in VHDL. The testbench contains various simple properties used by assert & cover directives which are proved with the SymbiYosys tool.
  13. ### fifo
  14. A simple synchronous FIFO with various checks for write/read pointers, data and flags.
  15. ### fwft_fifo
  16. A simple synchronous FIFO with first-word fall-through behaviour. Uses fifo as sub-unit. This design serves as an example how to verify designs with sub-units containing formal checks.
  17. ### vai_fifo
  18. A simple FIFO with valid-accept interface. Consists of fwft_fifo as sub-unit and some glue logic doing fifo<->vai interface conversion. This design serves as an example how to verify designs with sub-units containing formal checks.
  19. ### vai_reg
  20. A simple register file with VAI (valid-accept interface) which serves as test design to try formal verification of FSMs.