CoCEC: An Automatic Combinational Circuit Equivalence Checker Based on the Interactive Theorem Prover
2021
Checking the equivalence of two Boolean functions, or combinational circuits modeled as Boolean functions, is often desired
when reliable and correct hardware components are required. )e most common approaches to equivalence checking are based
on simulation and model checking, which are constrained due to the popular memory and state explosion problems. Furthermore,
such tools are often not user-friendly, thereby making it tedious to check the equivalence of large formulas or circuits. An
alternative is to use mathematical tools, called interactive theorem provers, to prove the equivalence of two circuits; however, this
requires human effort and expertise to write multiple output functions and carry out interactive proof of their equivalence. In this
paper, we (1) define two simple, one formal and the other informal, gate-level hardware description languages, (2) design and
develop a formal automatic combinational circuit equivalence checker (CoCEC) tool, and (3) test and evaluate our tool. )e tool
CoCEC is based on human-assisted theorem prover Coq, yet it checks the equivalence of circuit descriptions purely automatically
through a human-friendly user interface. It either returns a machine-readable proof (term) of circuits’ equivalence or a
counterexample of their inequality. )e interface enables users to enter or load two circuit descriptions written in an easy and
natural style. It automatically proves, in few seconds, the equivalence of circuits with as many as 45 variables (3.5 × 1013 states).
CoCEC has a mathematical foundation, and it is reliable, quick, and easy to use. )e tool is intended to be used by digital logic
circuit designers, logicians, students, and faculty during the digital logic design course.
- Correction
- Source
- Cite
- Save
- Machine Reading By IdeaReader
14
References
0
Citations
NaN
KQI