Abstract :
In his landmark 1986 article titled, No Silver Bullet: Essence and Accidents of Software Engineering [1], Dr. Fred Brooks observed that the inherent complexity of today´s software systems are derived from four elements: 1. the complexity of the problem domain, 2. the difficulty of managing the development process, 3. the flexibility possible through software, and 4. the problems of characterizing the behavior of discrete systems. Certainly, it can be argued that there is no silver bullet when it comes to hardware verification closure as a result of the same inherent complexities. So what do we mean by there is no silver bullet when it comes to hardware verification? It is simply this: there is no single tool or process we can apply to all classes of design problems to achieve verification closure. For example, even the simplest 32-bit combinatorial comparator can take hundreds of thousands of years to exhaustively simulate¿even with the fastest simulators on the market. Static formal verification enables us to automatically explore all possible corner cases for designer-sized blocks using exhaustive mathematical techniques versus incomplete simulation techniques (for example, we could exhaustively prove the previous 32-bit comparator example in a matter of seconds). Yet static formal verification suffers state explosion for large designs, and it is not applicable to all classes of design components (for example, an MPEG decoder is not a good candidate for static formal verification).
