@ -7,6 +7,8 @@ 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](https://github.com/YosysHQ). 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](https://www.symbioticeda.com) for more information.
There is a branch named [ghdl-synth](https://github.com/tmeissner/formal_hw_verification/tree/ghdl-synth) which uses [ghdlsynth-beta](https://github.com/tgingold/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.
### alu
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.
