Logical Equivalence Checks with CIRCT
- Mentors
- Jonathan Balkind, Fabian Schuiki, Martin Erhart
- Organization
- Free and Open Source Silicon Foundation
- Technologies
- llvm, c++, mlir, Z3, CIRCT
- Topics
- formal methods, HDL, SAT, SMT, formal verification
The CIRCT project is an open-source effort to develop Circuit Intermediate Representations, Compilers, and Tools by applying the MLIR and LLVM development methodology and best practices to the domain of hardware design tools.
In particular, it could act as a common platform and accelerate the development of interoperable design and verification tools, as opposed to today’s landscape of proprietary tools implementing their own disjoint and incompatible IRs.
This project's idea is to demonstrate said verification prowess by implementing "circt-lec", a basic LEC (Logical Equivalence Checker) tool for combinational CIRCT designs. Specifically, it has to translate two circuits into their fundamental boolean equations and formally prove or disprove their equivalence through the aid of an existing SMT solver (an engine for determining whether mathematical formulas are satisfiable).