What is formal verification?

Formal verification is the use of mathematical techniques to ensure that a design conforms to some precisely expressed notion of functional correctness. Concretely, assume that you have (1) a model of a design, (2) some description of the environment that the design is supposed to operate in, and (3) some properties that the design is intended to fulfill. Given this information, you may want to search for some input patterns that the environment could generate that will violate the properties. Classical approaches to demonstrating that such input stimuli exist are random simulation, or directed test. Formal verification is an alternative approach that can be used both to search for inputs sequences that violate the properties, and prove that the properties always hold in the case when no such stimuli exist.Formal verification can be applied to designs described at many different levels of abstraction, ranging from the gate level, to RTL implementations, and in some cases even to transaction level models described in standardized programming languages.There are several different use models for formal verification. Some design teams use it to boost the coverage of random simulation and hunt for bugs, whereas others make full blown use of it to conclusively prove that certain properties hold. State-of-the-art tools integrate formal verification engines with simulation in a seamless way.A particular formal verification problem of great interest in EDA is equivalence checking. Here, the property that is checked is whether two different designs always have the same input/output behavior with respect to some notion of equivalence. Special algorithms are used when it is known that the two designs differ only in restricted ways, for example when combinational optimization only has been used to derive one from the other.Compute resources required by formal verification algorithms generally grow very quickly as design sizes increase. Current formal verification research aims to increase the capacity of the design analysis algorithms, and to make formal verification usable earlier in the design cycle. For equivalence checking, hot topics include better capacity for data path verification and support for verification of sequential transformations.