Formal design techniques-theory and engineering reality

The explosion in the complexity of today´s chips is rapidly pushing the traditional simulation based verification approach to its limits. This paper examines formal verification techniques as solutions to this problem. The term is used for mathematically rigorous design checking from formal proof processes to relatively computationally `easy´ structural equivalence checking. It is argued that there is a need for processes which have for a long time been the realm of mathematicians and theoretical computer scientists to migrate into the world of engineers and be adopted as part of standard design methodologies. This migration can already be seen in the form of sequential equivalence and model checking, although the adoption of formal proof engines is some way in the future