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.
Ulrich Stern was supported during this research by a scholarship from the German Academic Exchange Service (DAAD-Doktorandenstipendium HSP-II).
Chapter PDF
Similar content being viewed by others
Keywords
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
O. Amble and D. E. Knuth. Ordered hash tables. Computer Journal, 17(2):135–142, 1974.
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.
J. L. Carter and M. N. Wegman. Universal classes of hash functions. Journal of Computer and System Sciences, 18(2):143–154, 1979.
T. H. Cormen, C. E. Leiserson, and R. L. Rivest. Introduction to Algorithms. The MIT Press, 1990.
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.
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.
G. H. Gonnet and R. Baeza-Yates. Handbook of Algorithms and Data Structures. Addison-Wesley Publishing Company, 2nd edition, 1991.
R. L. Graham, D. E. Knuth, and O. Patashnik. Concrete Mathematics: A Foundation for Computer Science. Addison-Wesley Publishing Company, 1988.
G. J. Holzmann. Design and Validation of Computer Protocols. Prentice-Hall, 1991.
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.
IEEE Std 1596–1992, IEEE Standard for Scalable Coherent Interface (SCI).
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.
D. E. Knuth. The Art of Computer Programming, volume 3. Addison-Wesley Publishing Company, 1973.
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.
P. Wolper and D. Leroy. Reliable hashing without collision detection. Unpublished revised version of [16].
P. Wolper and D. Leroy. Reliable hashing without collision detection. In Computer Aided Verification. 5th International Conference, pages 59–70, 1993.
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.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Stern, U., Dill, D.L. (1995). Improved probabilistic verification by hash compaction. In: Camurati, P.E., Eveking, H. (eds) Correct Hardware Design and Verification Methods. CHARME 1995. Lecture Notes in Computer Science, vol 987. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60385-9_13
Download citation
DOI: https://doi.org/10.1007/3-540-60385-9_13
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-60385-6
Online ISBN: 978-3-540-45516-5
eBook Packages: Springer Book Archive