Sciweavers

Share
DAC
2001
ACM

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

12 years 6 months ago
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. dongw@cs.cmu.edu, {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...
Dong Wang, Pei-Hsin Ho, Jiang Long, James H. Kukul
Added 13 Nov 2009
Updated 13 Nov 2009
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
Comments (0)
books