SimpleCAR

An Efficient Bug-Finding Tool Based on Approximate Reachability

Jianwen Li, Rohit Dureja, Geguang Pu, Kristin Y. Rozier, and Moshe Y. Vardi

This webpage contains further details and artifacts for reproducibility of the experiments in "SimpleCAR: An Efficient Bug-Finding Tool Based On Approximate Reachability" by J. Li, R. Dureja, G. Pu, K.Y. Rozier, M.Y. Vardi

---

Abstract

We present a new safety hardware model checker SimpleCAR that serves as a reference implementation for evaluating Complementary Approximate Reachability (CAR), a new SAT-based model checking framework inspired by classical reachability analysis. The tool gives a “bottom-line” performance measure for comparing future extensions to the framework. We demonstrate the performance of SimpleCAR on challenging benchmarks from the Hardware Model Checking Competition. Our experiments indicate that SimpleCAR is particularly suited for unsafety checking, or bug-finding; it is able to solve 7 unsafe instances within 1 hour that are not solvable by any other state-of-the-art techniques, including BMC and IC3/PDR, within 8 hours. We also identify a bug (reports safe instead of unsafe) and 48 counterexample generation errors in the tools compared in our analysis.