Title :
Correctness verification of VLSI modules supported by a very efficient Boolean prover
Author :
Lammens, P. ; Claesen, L. ; De Man, H.
Author_Institution :
Interuniv. Micro Electron. Center, Leuven, Belgium
Abstract :
A description is given of efficient techniques for checking tautology of a Boolean expression, i.e. whether two Boolean expressions are equivalent, taking into account `don´t care´ behavior if necessary. If two Boolean expressions appear to be not equivalent, a test case is generated. The tautology checker has been developed to perform functional and logical verification of combinational modules and is integrated in an environment for formal electrical verification. Its efficiency is based on a delicate and optimized interaction between a carefully chosen set of Boolean rewriting rules and a number of heuristics. A number of test cases show its performance as compared to existing tautology checkers. Figures on industrial PLAs are included
Keywords :
Boolean algebra; VLSI; circuit layout CAD; digital integrated circuits; logic CAD; Boolean expressions equivalence; Boolean prover; don´t care behavior; formal electrical verification; industrial PLAs; logical verification of combinational modules; number of heuristics; set of Boolean rewriting rules; tautology; tautology checker; test cases; verification of VLSI modules; Boolean algebra; Computational modeling; NP-hard problem; Parallel machines; Programmable logic arrays; Runtime; Silicon compiler; Testing; Very large scale integration;
Conference_Titel :
Computer Design: VLSI in Computers and Processors, 1989. ICCD '89. Proceedings., 1989 IEEE International Conference on
Conference_Location :
Cambridge, MA
Print_ISBN :
0-8186-1971-6
DOI :
10.1109/ICCD.1989.63368
