Predictive Reachability Using a Sample-Based Approach
BDD based reachability methods suffer from lack of robustness in performance, whereby it is difficult to estimate which one should be adopted for a given problem. We present a novel approach that examines a few short samples of the computation leading to an automatic, robust and modular way of reconciling the various methods for reachability. Our approach is able to intelligently integrate diverse reachability techniques such that each method can possibly get enhanced in efficiency. The method is in many cases orders of magnitude more efficient and it finishes all the invariant checking properties in VIS-Verilog benchmarks.
KeywordsShort Sample Symbolic Execution Reachability Analysis Benchmark Circuit Initial Reachability
- 2.Coudert, O., Berthet, C., Madre, J.C.: Verification of sequential machines based on symbolic execution. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407. Springer, Heidelberg (1990)Google Scholar
- 4.Narayan, A., et al.: Reachability Analysis Using Partitioned-ROBDDs. In: ICCAD, pp. 388–393 (1997)Google Scholar
- 6.Sahoo, D., Jain, J., Iyer, S., Dill, D.L., Allen Emerson, E.: Predictive reachability using a sample-based approach (2005), http://verify.stanford.edu/PAPERS/dsahoo-charme05-e.pdf
- 7.VIS. Verilog Benchmarks, http://vlsi.colorado.edu/~vis/