Formal Property Verification by Abstraction Refinement with Formal, Simulation and Hybrid Engines

roperty 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. [e-mail], {pho, long, kukula, yunshan, tonyma, robertd}@synopsys.com We present RFN, a formal property verification tool based on ion refinement. Abstraction refinement is a strategy for verification. It iteratively refines an abstract model to better approximate the behavior of the original design in the t the abstract model alone will provide enough evidence to prove or disprove the property. previous work on abstraction refinement was only demonstrated on designs with up to 500 registers. We developed RFN to verify real-world designs that may contain thousands of registers. RFN differs from the previous work in several ways. First, instead of relying on a single engine, RFN employs multiple formal verification engines, in...

• Type: Conference
• Year: 2001
• Where: DAC
• Authors: Dong Wang, Pei-Hsin Ho, Jiang Long, James H. Kukula, Yunshan Zhu, Hi-Keung Tony Ma, Robert F. Damiano
• Keywords: Abstract Model, Abstraction Refinement, DAC 2001, Design Automation, Formal Verification Engines