2007 Asia and South Pacific Design Automation Conference
Deeper Bound in BMC by Combining Constant Propagation and Abstraction
Yokohama
January 23-January 26
ISBN: 1-4244-0629-3
Limor Fix, Logic and Validation Technology, Intel Corporation, Haifa, Israel
Ranan Fraer, Logic and Validation Technology, Intel Corporation, Haifa, Israel
Tamir Heyman, Logic and Validation Technology, Intel Corporation, Haifa, Israel; Carnegie Mellon University, Pitts
Yakir Vizel, Logic and Validation Technology, Intel Corporation, Haifa, Israel
Yael Zbar, Logic and Validation Technology, Intel Corporation, Haifa, Israel
The most successful technologies for automatic verification of large industrial circuits are bounded model checking, abstraction, and iterative refinement. Previous work has demonstrated the ability to verify circuits with thousands of state elements achieving bounds of at most a couple of hundreds. In this paper we present several novel techniques for abstraction-based bounded model checking. Specifically, we introduce a constant-propagation technique to simplify the formulas submitted to the CNF SAT solver; we present a new proof-based iterative abstraction technique for bounded model checking; and we show how the two techniques can be combined. The experimental results demonstrate our ability to handle circuit with several thousands state elements reaching bounds nearing 1,000.
Citation:
Roy Armoni, Limor Fix, Ranan Fraer, Tamir Heyman, Moshe Vardi, Yakir Vizel, Yael Zbar, "Deeper Bound in BMC by Combining Constant Propagation and Abstraction," asp-dac, pp.304-309, 2007 Asia and South Pacific Design Automation Conference, 2007
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb