loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
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
ASCII Text
x 
 
Roy Armoni, Limor Fix, Ranan Fraer, Tamir Heyman, Moshe Vardi, Yakir Vizel, Yael Zbar, "Deeper Bound in BMC by Combining Constant Propagation and Abstraction," Asia and South Pacific Design Automation Conference, pp. 304-309, 2007 Asia and South Pacific Design Automation Conference, 2007.
 
 
BibTex
x
 
@article{ 10.1109/ASPDAC.2007.358003,
author = {Roy Armoni and Limor Fix and Ranan Fraer and Tamir Heyman and Moshe Vardi and Yakir Vizel and Yael Zbar},
title = {Deeper Bound in BMC by Combining Constant Propagation and Abstraction},
journal ={Asia and South Pacific Design Automation Conference},
volume = {0},
year = {2007},
isbn = {1-4244-0629-3},
pages = {304-309},
doi = {http://doi.ieeecomputersociety.org/10.1109/ASPDAC.2007.358003},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - CONF
JO - Asia and South Pacific Design Automation Conference
TI - Deeper Bound in BMC by Combining Constant Propagation and Abstraction
SN - 1-4244-0629-3
SP304
EP309
A1 - Roy Armoni,
A1 - Limor Fix,
A1 - Ranan Fraer,
A1 - Tamir Heyman,
A1 - Moshe Vardi,
A1 - Yakir Vizel,
A1 - Yael Zbar,
PY - 2007
KW - null
VL - 0
JA - Asia and South Pacific Design Automation Conference
ER -
 
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
Moshe Vardi, Rich University, Houston, Tx
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
Usage of this product signifies your acceptance of the Terms of Use.