Title :
A semi-formal verification methodology
Author :
Lu, Yuan ; Li, Weimin
Abstract :
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
Keywords :
application specific integrated circuits; circuit CAD; formal verification; integrated circuit design; ASIC; Broadcom Gigabit Ethernet switch; block-level design; environment modeling; human abstraction; random simulation; semi-formal verification methodology; system-level validation; Application specific integrated circuits; Computer bugs; Ethernet networks; Explosions; Formal verification; Humans; Law; Legal factors; Packet switching; Switches;
Conference_Titel :
ASIC, 2001. Proceedings. 4th International Conference on
Conference_Location :
Shanghai
Print_ISBN :
0-7803-6677-8
DOI :
10.1109/ICASIC.2001.982491