Formal Property Verification by Abstraction Refinement with.pdfVIP

Formal Property Verification by Abstraction Refinement with Formal, Simulation and Hybrid Engines Dong Wang † , Pei-Hsin Ho ‡ , Jiang Long ‡ , James Kukula ‡ Yunshan Zhu ‡ , Tony Ma ‡ , Robert Damiano ‡ † Carnegie Mellon University ‡ Advanced Technology Group, Synopsys Inc. dongw@, {pho, long, kukula, yunshan, tonyma, robertd}@ ABSTRACT BDD-based symbolic model checking [4][11] is still the most widely used technology for formal property verification. We present RFN, a formal property verification tool based on However, the capacity of symbolic model checking is restricted abstraction refinement. Abstraction refinement is a strategy for to designs that contain a couple of hundred sequential cells (flops property verification. It iteratively refines an abstract model to or latches). To verify real-world designs, the user must obtain better approximate the behavior of the original design in the from the RTL design an abstract model that is within the hope that the abstract model alone will provide enough evidence capacity of the symbolic model checker. to prove or disprove the property.