|T. Meissner 30ef117823 Add short informations about the ghdl-synth branch||2 weeks ago|
|alu||1 year ago|
|counter||1 year ago|
|dlatchsr||1 year ago|
|vai_reg||9 months ago|
|.gitignore||1 year ago|
|LICENSE.md||1 year ago|
|README.md||2 weeks 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, together with a formal testbench written in SystemVerilog. The testbench contains various simple SVA properties used by assert & cover directives which are proved with the SymbiYosys tool.
A simple counter design in VHDL, together with a formal testbench written in SystemVerilog. The testbench contains various simple SVA 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.