Formal Verification and Diagnosis of Combinational Circuit Designs with Propositional Logic

Abstract

Zero-defect is extremely important for VLSI designs. Formal techniques for verifying the correctness of logic designs overcome the limits of test case simulation. Many formal systems have been proposed for verification purpose. However, verification of VLSI designs is not enough. It would be equally or more important to correct wrong designs. Little attention has been paid on diagnosis of logic designs. We propose a formal system, based on a propositional logic theorem prover, to verify a combinational logic design and to fix the design if it is incorrect. By referring to the models obtained for an incorrect design and applying some heuristics, the system can locate errors and correct the design in an intelligent way.