Formal verification of hardware: misconception and reality

Formal verification in hardware, is a novel technique for validating the functional correctness of designs through the various phases of the design process, starting from the first specification. Simulation, the present industrial standard tool for verification, relies on propagating a set of input test vectors through the design and manually observing the validity of the outputs corresponding to the inputs. In contrast, formal verification does not require any input vectors and at the same time guarantees 100% correctness. The idea behind the formal verification engines is to use mathematical techniques to exercise all possible inputs and automatically check for outputs that are not in order. The use of formal verification for equivalence checking, especially at the lower levels of abstraction, is of real advantage. In spite of the various informalities which creep into the verification process it is definitely a boon for coping with the complexity of today's design. However, giant strides need to be taken by the FV tool vendors in developing an adequate environment for performing sequential equivalence checking and property checking on large industrial designs.