|T. Meissner f2e4f71292 Add infos about fifo model to README||1 month ago|
|alu||3 months ago|
|counter||3 months ago|
|fifo||1 month ago|
|vai_reg||3 months ago|
|.gitignore||1 year ago|
|LICENSE.md||1 year ago|
|README.md||1 month 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.
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. The alu, counter & vai_reg designs can be verified with that combination at the moment.
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.
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 register file with VAI (valid-accept-interface) which serves as test design to try formal verification of FSMs.