Trying to verify Verilog/VHDL designs with formal methods and tools

vhdl verilog assertions formal yosys systemverilog sva

T. Meissner 12e20b1da2 Some small improvements * Adopt init state generation for initial reset constraining * Add assume about inactive reset after initial active * Replaced OPC consts by macros * Replace SVA reset check by simple unclocked immediate assertion		6 years ago
alu	Some small improvements	6 years ago
counter	Make the unbounded prove work	6 years ago
dlatchsr	Add example for dlatchsr error	6 years ago
.gitignore	Makefile: add clean target; fixed Reset_n_i port dir in alu_t.sv	6 years ago
LICENSE.md	Inital commit	6 years ago
README.md	Remove gitignore from alu folder; added link to Yosys	6 years ago

README.md

formal_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. Some examples use the VHDL/SystemVerilog parser 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.

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.