In this article, we discuss why formal verification adoption has been limited in industry, and how abstraction-based methodology in formal verification can help DV engineers become successful in adopting formal property checking more widely. Abstraction is the key to obtaining scalability and predictability. It provides an efficient bug-hunting technique and helps in establishing exhaustive proof convergence. We illustrate our methodology on a FIFO in this article, but similar methods are used in the verification of a range of designs ranging from a RISC-V processorto multi-million gate designs.
Despite its rich history, formal verification adoption is growing mainly through the usage of automated apps, but its full