Abstract
To embrace the fast growth of circuit complexity, verification researchers are probing new verification methods. Verification by composition, among others, is regarded as a promising direction.
Symbolic Trajectory Evaluation (STE) is a theory for digital circuit verification. In the last a few years, STE has been used in proving practical digital circuits and has been proven a practical methodology with a mathematical foundation in circuit verification. However, the circuit model used in the existing STE verification systems is, in general, not compositional.
In this paper, we present a compositional circuit model. This model distinguishes two different types of unknown circuit values, i.e. driven undefined value and undriven undefined value. This treatment makes composition of circuit model possible. Major results of the paper are the following:
-
1.
A language for describing finite state machines. This language is used to describe circuits behaviors. Expressions written in the language can be interpreted to the new model in this paper, as well as to the existing model. An operator in the language is designed for finite-state machine composition. The semantics of this operator is consistent to our intuitive understanding of “connecting two circuit node together”. The major theorem concerning this operator is that it preserves the properties of the finite-state machines being composed.
-
2.
The finite-state machine description can also be interpreted to the model which is used by the Voss system, a circuit verification system. A theorem shows that under certain conditions, two interpretations of the same finite-state machine description achieve the same verification results. This theorem allows us to perform circuit verification by using the well-developed STE verification system, and then to interpret the verification result in the model presented in this paper.
This research was supported, in part, by operating grants OGPO 109688 and OGPO O46196 from the Natural Sciences Research Council of Canada, fellowships from the Province of British Columbia Advanced Systems Institute, and by research contract 92-DJ-295 from the Semiconductor Research Corporation.
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
Seger, C.-J., and Bryant, R. Formal verification of digital circuits by symbolic evaluation of partially-ordered trajectories. Tech. Rep. Technical Report 93-8, The Computer Science Department, The University of British Columbia, The Computer Science Department, The University of B.C. Vancouver B.C. V6T 1Z4, 1993. To appear in Journal of Formal Methods in System Design.
Seger, C.-J. Voss — a formal hardware verification system, user's guide. Tech. Rep. Technical Report 93-45, The Computer Science Department, The University of British Columbia, The Computer Science Department, The University of B.C. Vancouver B.C. V6T 1Z4, 1993.
Joyce, J. Multi-level Verification of Microprocessor-Based Systems. PhD thesis, Computer Laboratory, Cambridge University, 1989.
Zhu, Z., Joyce, J., and Seger, C.-J. Verification of the tamarack-3 microprocessor in a hybrid verification environment. In Proceedings of 1993 international meeting on Higer Order Logic and its Applications, Lecture Notes in Computer Science, Vol. 780 (1993), Springer-Verlag.
Seger, C.-J., and Joyce, J. A mathematically precise two-level formal verification methodology”, Tech. Rep. Report-92-34, Computer Science Department, The University of British Columbia, 1992.
Joyce, J., and Seger, C.-J. Linking bdd-based symbolic evaluation to interactive theorem-proving. In Proceedings of 30th Design Automation Conference (1993).
Zhu, Z. Construction of circuit models from trajectory specifications. in progress, Janurary 1994.
Zhu, Z., and Seger, C.-J. Model construction from trajectory assertion and the completeness of a hardware inference system. In The proceedings of the Sixth International Conference on Computer Aided Verification (CAV94), Lecture Notes in Computer Science, Vol. 818 (1994), Springer-Verlag.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Zhu, Z. (1995). A compositional circuit model and verification by composition. In: Kumar, R., Kropf, T. (eds) Theorem Provers in Circuit Design. TPCD 1994. Lecture Notes in Computer Science, vol 901. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-59047-1_44
Download citation
DOI: https://doi.org/10.1007/3-540-59047-1_44
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-59047-7
Online ISBN: 978-3-540-49177-4
eBook Packages: Springer Book Archive