Advertisement

Predictive Reachability Using a Sample-Based Approach

  • Debashis Sahoo
  • Jawahar Jain
  • Subramanian K. Iyer
  • David Dill
  • E. Allen Emerson
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3725)

Abstract

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.

Keywords

Short Sample Symbolic Execution Reachability Analysis Benchmark Circuit Initial Reachability 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

References

  1. 1.
    Bryant, R.: Graph-based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computers C-35, 677–691 (1986)zbMATHCrossRefGoogle Scholar
  2. 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
  3. 3.
    Iyer, S., Sahoo, D., Stangier, C., Narayan, A., Jain, J.: Improved symbolic Verification Using Partitioning Techniques. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol. 2860, pp. 410–424. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  4. 4.
    Narayan, A., et al.: Reachability Analysis Using Partitioned-ROBDDs. In: ICCAD, pp. 388–393 (1997)Google Scholar
  5. 5.
    Sahoo, D., Iyer, S., Jain, J., Stangier, C., Narayan, A., Dill, D.L., Allen Emerson, E.: A partitioning methodology for bdd-based verification. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol. 3312, pp. 399–413. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  6. 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. 7.
    VIS. Verilog Benchmarks, http://vlsi.colorado.edu/~vis/

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Debashis Sahoo
    • 1
  • Jawahar Jain
    • 3
  • Subramanian K. Iyer
    • 2
  • David Dill
    • 1
  • E. Allen Emerson
    • 2
  1. 1.Stanford UniversityStanfordUSA
  2. 2.University of Texas at AustinAustinUSA
  3. 3.Fujitsu Lab. of America 

Personalised recommendations