Abstract: The problem under discussion is to check whether a given combinational network realizes a system of incompletely specified Boolean functions. SAT-based procedure is discussed that formulates the overall problem as conventional conjunctive normal form (CNF) on the basis of encoding of multiple-output cubes the Boolean functions are specified on and checking whether the combinational network realizes them using a SAT solver. The novel method is proposed that speeds up the SAT-based procedure due to suggested efficient procedure of logarithmic encoding multiple-output cubes that allows reducing the number of variables to be additionally introduced into the CNF under construction.

Keywords: design automation, verification, simulation, CNF satisfiability.

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:

SAT-BASED METHOD OF VERIFICATION USING LOGARITHMIC ENCODING

Liudmila Cheremisinova, Dmitry Novikov

http://www.foibg.com/ibs_isc/ibs-15/ibs-15-p14.pdf