A semi-formal verification methodology

Formal verification techniques attract great attention from industry because of their ability to discover subtle design errors where simulation fails. However, due to the state explosion problem, formal techniques usually cannot handle large designs. This paper introduces a semi-formal verification methodology in which formal techniques and simulation are tightly coupled. In this methodology, we apply formal techniques to verify a few "difficult" block level designs. The verified properties and valid traces are carried over in the random simulation based system level validation. These properties and legal traces not only can discover new design errors but also help to define the "thoroughness" of the system level validation. The block level formal verification usually requires human abstraction and environment modeling. Due to human mistakes, it is possible that system level validation violates a property while the formal model satisfies the property. In this case, we formally re-verify the property again after revising the environment or abstraction. In this way, a complete block level verification may be achieved. As a practice, we are applying this methodology to verify a Broadcom Gigabit Ethernet switch design