Deeper Bound in BMC by Combining Constant Propagation and Abstraction

ound in BMC by Combining Constant Propagation and Abstraction Roy Armoni, Limor Fix1 , Ranan Fraer1 , Tamir Heyman1,3 , Moshe Vardi2 , Yakir Vizel1 , Yael Zbar1 1 Logic and Validation Technology, Intel Corporation, Haifa, Israel 2 Rich University, Houston, Tx 3 Carnegie Mellon University, Pittsburgh, PA Abstract 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 oof-based iterative abstraction technique for bounded model checking; and we show how the two techniques can be combined. The experimental results demonstrate o...

• Type: Conference
• Year: 2007
• Where: ASPDAC
• Authors: Roy Armoni, Limor Fix, Ranan Fraer, Tamir Heyman, Moshe Y. Vardi, Yakir Vizel, Yael Zbar
• Keywords: Abstraction Roy Armoni, ASPDAC 2007, Hardware, Model Checking, State Elements