Abstract. The problem of checking whether a system of incompletely specified Boolean functions is implemented by the given combinational circuit is considered. The task is reduced to testing out if two given logical descriptions are equivalent on the domain of one of them having functional indeterminacy. We present a novel SAT-based verification method that is used for testing whether the given circuit satisfies all the conditions represented by the system of incompletely specified Boolean functions.

Keywords: design automation, verification, simulation, SAT.

ACM Classification Keywords: B.6.2 Logic Design: Reliability and Testing; G.4 Mathematical Software: Verification; B.6.2 Reliability and Testing: Error-checking.

Link:

USING SAT FOR COMBINATIONAL IMPLEMENTATION CHECKING

Liudmila Cheremisinova, Dmitry Novikov

http://www.foibg.com/ibs_isc/ibs-07/IBS-07-p30.pdf