T. Meissner 36d6da1943 | 5 years ago | |
---|---|---|
alu | 6 years ago | |
counter | 6 years ago | |
dlatchsr | 6 years ago | |
vai_reg | 6 years ago | |
.gitignore | 6 years ago | |
LICENSE.md | 6 years ago | |
README.md | 5 years 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.
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. Some examples use the 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.
There is a branch named ghdl-synth which uses ghdlsynth-beta as VHDL frontend plugin for SymbiYosys. Furthermore using GHDL(synth) as synthesis frontend allows using PSL as verification language. Only the vai_reg design can be verified in this branch at the moment.
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 test design which generates the Unsupported cell type $dlatchsr
error using with Verific plugin.
A simple register file with VAI (valid-accept-interface) which serves as test design to try formal verification of FSMs.