Formal Verification and Diagnosis of Combinational Circuit Designs with Propositional Logic

Article type: Research Article

Authors: Lee, Shie-Jue | Lin, Wei-Jer

Affiliations: Department of Electrical Engineering, National Sun Yat-Sen University, Kaohsiung, Taiwan 80424, [email protected]

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.

Keywords: specification, logic design, verification, diagnosis, models, heuristics

DOI: 10.3233/FI-1997-3117

Journal: Fundamenta Informaticae, vol. 31, no. 1, pp. 79-105, 1997