Correctness verification of VLSI modules supported by a very efficient Boolean prover

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