TY - GEN
T1 - Safety model checking with complementary approximations
AU - Li, Jianwen
AU - Zhu, Shufang
AU - Zhang, Yueling
AU - Pu, Geguang
AU - Vardi, Moshe Y.
N1 - Publisher Copyright:
© 2017 IEEE.
PY - 2017/12/13
Y1 - 2017/12/13
N2 - Formal-verification techniques, such as model checking, are becoming popular in hardware design. SAT-based model checking techniques, such as IC3/PDR, have gained a significant success in the hardware industry. In this paper, we present a new framework for SAT-based safety model checking, named Complementary Approximate Reachability (CAR). CAR is based on standard reachability analysis, but instead of maintaining a single sequence of reachable-state sets, CAR maintains two sequences of over- and under-approximate reachable-state sets, checking safety and unsafety at the same time. To construct the two sequences, CAR uses standard Boolean-reasoning algorithms, based on satisfiability solving, one to find a satisfying cube of a satisfiable Boolean formula, and one to provide a minimal unsatisfiable core of an unsatisfiable Boolean formula. We applied CAR to 548 hardware model-checking instances, and compared its performance with IC3/PDR. Our results show that CAR is able to solve 42 instances that cannot be solved by IC3/PDR. When evaluated against a portfolio that includes IC3/PDR and other approaches, CAR is able to solve 21 instances that the other approaches cannot solve. We conclude that CAR should be considered as a valuable member of any algorithmic portfolio for safety model checking.
AB - Formal-verification techniques, such as model checking, are becoming popular in hardware design. SAT-based model checking techniques, such as IC3/PDR, have gained a significant success in the hardware industry. In this paper, we present a new framework for SAT-based safety model checking, named Complementary Approximate Reachability (CAR). CAR is based on standard reachability analysis, but instead of maintaining a single sequence of reachable-state sets, CAR maintains two sequences of over- and under-approximate reachable-state sets, checking safety and unsafety at the same time. To construct the two sequences, CAR uses standard Boolean-reasoning algorithms, based on satisfiability solving, one to find a satisfying cube of a satisfiable Boolean formula, and one to provide a minimal unsatisfiable core of an unsatisfiable Boolean formula. We applied CAR to 548 hardware model-checking instances, and compared its performance with IC3/PDR. Our results show that CAR is able to solve 42 instances that cannot be solved by IC3/PDR. When evaluated against a portfolio that includes IC3/PDR and other approaches, CAR is able to solve 21 instances that the other approaches cannot solve. We conclude that CAR should be considered as a valuable member of any algorithmic portfolio for safety model checking.
UR - https://www.scopus.com/pages/publications/85043530525
U2 - 10.1109/ICCAD.2017.8203765
DO - 10.1109/ICCAD.2017.8203765
M3 - 会议稿件
AN - SCOPUS:85043530525
T3 - IEEE/ACM International Conference on Computer-Aided Design, Digest of Technical Papers, ICCAD
SP - 95
EP - 100
BT - 2017 IEEE/ACM International Conference on Computer-Aided Design, ICCAD 2017
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 36th IEEE/ACM International Conference on Computer-Aided Design, ICCAD 2017
Y2 - 13 November 2017 through 16 November 2017
ER -