Tutorial T4B: Formal Assertion-Based Verification in Industrial Setting

Increased complexities of hardware designs have made exhaustive simulation of designs near impossible - thereby creating a need for some complementary verification technique. This has generated a renewed interest in use of formal analysis on industrial hardware designs. Formal analysis of hardware design involves use of mathematical techniques to prove that the design implementation confirms to the specification. The specification is a set of properties which should hold on the design under verification. Advances in formal analysis techniques with more sophisticated heuristics, have made them usable on big blocks of hardware. In this tutorial, we begin by giving a brief theoretical introduction to various methods applied in formal hardware verification, and then discuss various automated and manual techniques to handle the state explosion problem. Application of formal analysis techniques on appropriate designs and in a methodical way is key to successful verification. In this tutorial we elaborate on how one can effectively plan for formal verification, and successfully close verification. We illustrate these techniques using several case studies. Finally we present the future directions for commercial tools in this domain