CoCEC: An Automatic Combinational Circuit Equivalence Checker Based on the Interactive Theorem Prover
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. The most common approaches to equivalence checking are based on simulation and model checking, which are constrained...
Main Authors: | Wilayat Khan, Farrukh Aslam Khan, Abdelouahid Derhab, Adi Alhudhaif |
---|---|
Format: | Article |
Language: | English |
Published: |
Hindawi-Wiley
2021-01-01
|
Series: | Complexity |
Online Access: | http://dx.doi.org/10.1155/2021/5525539 |
Similar Items
-
Formal Analysis of Language-Based Android Security Using Theorem Proving Approach
by: Wilayat Khan, et al.
Published: (2019-01-01) -
The linear resolution theorem prover
by: Chan, Nelson Hin-Fai
Published: (2010) -
An Exercise in Invariant-based Programming with Interactive and Automatic Theorem Prover Support
by: Ralph-Johan Back, et al.
Published: (2012-02-01) -
Generating pseudo-random theorems for testing theorem provers
by: Darwish, Nevin Mahmoud, 1952-
Published: (1978) -
A self-verifying theorem prover
by: Davis, Jared Curran
Published: (2010)