Trying to verify Verilog/VHDL designs with formal methods and tools
vhdl
verilog
assertions
formal
yosys
systemverilog
sva
T. Meissner 763c2f03c7 Fix badge URL; minor further changes 1 week ago
.github ci: add GitHub Actions workflow 'Test' 1 week ago
alu Use PSL functions instead of workarounds; add forgotten always to asserts in alu 7 months ago
counter Use PSL functions instead of workarounds; add forgotten always to asserts in alu 7 months ago
fifo Name assume & restrict directives 2 weeks ago
vai_fifo Use chformal to remove unreachable cover cells 2 weeks ago
vai_reg Use PSL functions instead of workarounds; add forgotten always to asserts in alu 7 months ago
.gitignore Makefile: add clean target; fixed Reset_n_i port dir in alu_t.sv 2 years ago
LICENSE.md Inital commit 2 years ago
Makefile ci: add GitHub Actions workflow 'Test' 1 week ago
README.md Fix badge URL; minor further changes 1 week ago
tests.txt ci: add GitHub Actions workflow 'Test' 1 week ago

README.md

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.

formal_hw_verification

Tests and examples of using formal verification to check correctness of digital hardware designs. All tests are done with SymbiYosys, a front-end for formal verification flows based on Yosys.

All stuff in the master branch uses ghdl-yosys-plugin and GHDL as VHDL front-end plugin for (Symbi)Yosys. Using GHDL as synthesis frontend allows using PSL as verification language.

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.

alu

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.

counter

A simple counter design in VHDL. The testbench contains various simple properties used by assert & cover directives which are proved with the SymbiYosys tool.

fifo

A simple synchronous FIFO with various checks for write/read pointers, data and flags.

vai_fifo

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.

vai_reg

A simple register file with VAI (valid-accept-interface) which serves as test design to try formal verification of FSMs.