Advertisement

Improved probabilistic verification by hash compaction

  • Ulrich Stern
  • David L. Dill
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 987)

Abstract

We present and analyze a probabilistic method for verification by explicit state enumeration, which improves on the “hashcompact” method of Wolper and Leroy. The hashcompact method maintains a hash table in which compressed values for states instead of full state descriptors are stored. This method saves space but allows a non-zero probability of omitting states during verification, which may cause verification to miss design errors (i.e. verification may produce “false positives”). Our method improves on Wolper and Leroy's by calculating the hash and compressed values independently, and by using a specific hashing scheme that requires a low number of probes in the hash table. The result is a large reduction in the probability of omitting a state. Hence, we can achieve a given upper bound on the probability of omitting a state using fewer bits per compressed state. For example, we can reduce the number of bytes stored for each state from the eight recommended by Wolper and Leroy to only five, and still enumerate state spaces of up to 80 million reachable states while keeping the probability of missing even one state to less than 0.13%.

The new verification scheme was tried on some large, industrial examples. The results predicted by the theoretical analysis were confirmed by the outcomes of these examples. We also discuss some practical issues in choosing the number of bits for the compressed state representation, along with some of our experiences in implementing the scheme.

Keywords

Hash Function Hash Table Probe Sequence State Table Reachable State 
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.
    O. Amble and D. E. Knuth. Ordered hash tables. Computer Journal, 17(2):135–142, 1974.Google Scholar
  2. 2.
    J. R. Burch, E. M. Clarke, K. L. McMillan, and D. L. Dill. Sequential circuit verification using symbolic model checking. In 27th ACM/IEEE Design Automation Conference, pages 46–51, 1990.Google Scholar
  3. 3.
    J. L. Carter and M. N. Wegman. Universal classes of hash functions. Journal of Computer and System Sciences, 18(2):143–154, 1979.Google Scholar
  4. 4.
    T. H. Cormen, C. E. Leiserson, and R. L. Rivest. Introduction to Algorithms. The MIT Press, 1990.Google Scholar
  5. 5.
    D. L. Dill, A. J. Drexler, A. J. Hu, and C. H. Yang. Protocol verification as a hardware design aid. In IEEE International Conference on Computer Design: VLSI in Computers and Processors, pages 522–5, 1992.Google Scholar
  6. 6.
    D. L. Dill, S. Park, and A. G. Nowatzyk. Formal specification of abstract memory models. In Symposium on Research on Integrated Systems, pages 38–52, 1993.Google Scholar
  7. 7.
    G. H. Gonnet and R. Baeza-Yates. Handbook of Algorithms and Data Structures. Addison-Wesley Publishing Company, 2nd edition, 1991.Google Scholar
  8. 8.
    R. L. Graham, D. E. Knuth, and O. Patashnik. Concrete Mathematics: A Foundation for Computer Science. Addison-Wesley Publishing Company, 1988.Google Scholar
  9. 9.
    G. J. Holzmann. Design and Validation of Computer Protocols. Prentice-Hall, 1991.Google Scholar
  10. 10.
    A. J. Hu, G. York, and D. L. Dill. New techniques for efficient verification with implicitly conjoined BDDs. In 31st Design Automation Conference, pages 276–82, 1994.Google Scholar
  11. 11.
    IEEE Std 1596–1992, IEEE Standard for Scalable Coherent Interface (SCI).Google Scholar
  12. 12.
    C. N. Ip and D. L. Dill. Efficient verification of symmetric concurrent systems. In IEEE International Conference on Computer Design: VLSI in Computers and Processors, pages 230–234, 1993.Google Scholar
  13. 13.
    D. E. Knuth. The Art of Computer Programming, volume 3. Addison-Wesley Publishing Company, 1973.Google Scholar
  14. 14.
    U. Stern and D. L. Dill. Automatic verification of the SCI cache coherence protocol. In IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods, 1995.Google Scholar
  15. 15.
    P. Wolper and D. Leroy. Reliable hashing without collision detection. Unpublished revised version of [16].Google Scholar
  16. 16.
    P. Wolper and D. Leroy. Reliable hashing without collision detection. In Computer Aided Verification. 5th International Conference, pages 59–70, 1993.Google Scholar
  17. 17.
    L. Yang, D. Gao, J. Mostoufi, R. Joshi, and P. Loewenstein. System design methodology of UltraSPARCTM-I. In 32nd Design Automation Conference, pages 7–12, 1995.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1995

Authors and Affiliations

  • Ulrich Stern
    • 1
  • David L. Dill
    • 1
  1. 1.Department of Computer ScienceStanford UniversityStanford

Personalised recommendations