|T. Meissner 763c2f03c7 Fix badge URL; minor further changes||1 week ago|
|.github||1 week ago|
|alu||7 months ago|
|counter||7 months ago|
|fifo||2 weeks ago|
|vai_fifo||2 weeks ago|
|vai_reg||7 months ago|
|.gitignore||2 years ago|
|LICENSE.md||2 years ago|
|Makefile||1 week ago|
|README.md||1 week ago|
|tests.txt||1 week ago|
The original repository is located on my own git-server at https://git.goodcleanfun.de/tmeissner/formal_hw_verification
It is mirrored to github with every push, so both should be in sync.
Some examples in the verific branch 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 for more information.
You can use the
hdlc/formal:all docker image provided by the hdl containers project (recommended). Or you build a docker image on your own machine using my Dockerfiles for SymbiYosys & GHDL. With both you have the latest tool versions available.
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.
A simple counter design in VHDL. The testbench contains various simple properties used by assert & cover directives which are proved with the SymbiYosys tool.
A simple synchronous FIFO with various checks for write/read pointers, data and flags.
A simple FIFO with valid-accept-interface. Consists of 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.
A simple register file with VAI (valid-accept-interface) which serves as test design to try formal verification of FSMs.