TY - GEN
T1 - Tunneling and slicing
T2 - 45th Design Automation Conference, DAC
AU - Ganai, Malay
AU - Gupta, Aarti
PY - 2008/9/17
Y1 - 2008/9/17
N2 - Bounded Model Checking (BMC) provides complete design coverage with respect to a correctness property up to a bounded depth. However, with successive unrolling of the design, each BMC instance at depth k becomes bigger in size and harder to solve. We propose a novel scalable approach to decompose disjunctively a BMC instance, into simpler and independent subproblems, based on tunnels i.e., a set of control paths. We simplify each subproblem using slicing, data path simplification and tunnel specific control flow constraints, and solve them independently. We implemented such a tunneling and slicing-based reduction (TSR) approach in Satisfiability-Modulo-Theory (SMT)-based BMC framework. Such a TSR-based approach improves the overall performance of BMC when applied to verification of lowlevel embedded industry programs.
AB - Bounded Model Checking (BMC) provides complete design coverage with respect to a correctness property up to a bounded depth. However, with successive unrolling of the design, each BMC instance at depth k becomes bigger in size and harder to solve. We propose a novel scalable approach to decompose disjunctively a BMC instance, into simpler and independent subproblems, based on tunnels i.e., a set of control paths. We simplify each subproblem using slicing, data path simplification and tunnel specific control flow constraints, and solve them independently. We implemented such a tunneling and slicing-based reduction (TSR) approach in Satisfiability-Modulo-Theory (SMT)-based BMC framework. Such a TSR-based approach improves the overall performance of BMC when applied to verification of lowlevel embedded industry programs.
UR - http://www.scopus.com/inward/record.url?scp=51549116150&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=51549116150&partnerID=8YFLogxK
U2 - 10.1109/DAC.2008.4555797
DO - 10.1109/DAC.2008.4555797
M3 - Conference contribution
AN - SCOPUS:51549116150
SN - 9781605581156
T3 - Proceedings - Design Automation Conference
SP - 137
EP - 142
BT - Proceedings of the 45th Design Automation Conference, DAC
Y2 - 8 June 2008 through 13 June 2008
ER -