TY - GEN
T1 - Accelerating high-level bounded model checking
AU - Ganai, Malay K.
AU - Gupta, Aarti
N1 - Copyright:
Copyright 2008 Elsevier B.V., All rights reserved.
PY - 2006
Y1 - 2006
N2 - SAT-based Bounded Model Checking (BMC) has been found promising in finding deep bugs in industry designs and scaling well with design sizes. However, it has limitations due to requirement of finite data paths, inefficient translations and loss of high-level design information during the BMC problem formulation. These shortcomings inherent in Boolean-level BMC can be avoided by using high-level BMC. We propose a novel framework for high-level BMC, which includes several techniques that extract high-level design information from EFSM models to make the verification model "BMC friendly", and use it on-the-fly to simplify the BMC problem instances. Such techniques overcome the inherent limitations of Boolean-level BMC, while allowing integration of state-of-the-art techniques for BMC. In our controlled experiments we found signficant performance improvements achievable by the proposed techniques.
AB - SAT-based Bounded Model Checking (BMC) has been found promising in finding deep bugs in industry designs and scaling well with design sizes. However, it has limitations due to requirement of finite data paths, inefficient translations and loss of high-level design information during the BMC problem formulation. These shortcomings inherent in Boolean-level BMC can be avoided by using high-level BMC. We propose a novel framework for high-level BMC, which includes several techniques that extract high-level design information from EFSM models to make the verification model "BMC friendly", and use it on-the-fly to simplify the BMC problem instances. Such techniques overcome the inherent limitations of Boolean-level BMC, while allowing integration of state-of-the-art techniques for BMC. In our controlled experiments we found signficant performance improvements achievable by the proposed techniques.
UR - http://www.scopus.com/inward/record.url?scp=46149102489&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=46149102489&partnerID=8YFLogxK
U2 - 10.1109/ICCAD.2006.320122
DO - 10.1109/ICCAD.2006.320122
M3 - Conference contribution
AN - SCOPUS:46149102489
SN - 1595933891
SN - 9781595933898
T3 - IEEE/ACM International Conference on Computer-Aided Design, Digest of Technical Papers, ICCAD
SP - 794
EP - 801
BT - Proceedings of the 2006 International Conference on Computer-Aided Design, ICCAD
T2 - 2006 International Conference on Computer-Aided Design, ICCAD
Y2 - 5 November 2006 through 9 November 2006
ER -