Formal verification of an ASIC ethernet switch block

Traditionally, validation at the ASIC block level relies primarily upon simulation based verification. Specific components that are “hot spots” are then considered as candidates for Formal Verification. Under this usage model, the hurdles to Formal Verification are intractability and poor specifications. In this paper, we outline an alternate approach, where we used Formal Verification as the “first line of defense” in the course of validating a Packet Switch. This block had several components that were complex and hard to verify, including components that required liveness guarantees, where responses are event bound, and not cycle bound. To surmount typical hurdles, an early collaboration was formed between design and verification engineer, both to influence the design as well as to identify relevant manual abstraction techniques upfront. All significant components were formally verified at the module level. This approach was successful in identifying most bugs during the design phase itself and drastically minimized bugs during verification/emulation phases of the project. This paper illustrates the strengths of such an approach. It describes our overall methodology and the proof techniques utilized. The overall effort yielded a total of 55 bugs found (52 during the design phase and only 3 bugs during the verification phase). No bugs were found subsequently during emulation. As a result, this block was deemed “tape out ready” 2 months prior to other blocks of similar complexity.