Abstract
To perform verification of digital systems with time bounded delays, it is essential to characterize the space of all possible system behaviors. In this paper, we describe our analysis technique which accepts a behavioral specification of the timing of a digital system and generates the set of all possible behaviors for the system. The ability to represent and reason about time ranges for events is a distinguishing characteristic of our technique and gives our analysis method both its power and complexity.
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.
We gratefully acknowledge the support of this research by the National Science Foundation grant number MIP-9102721.
Download to read the full chapter text
Chapter PDF
References
Thomas M. McWilliams, “Verification of Timing Constraints on Large Digital Systems,” Proc. 17th Design Automation Conference (June, 1980).
Robert B. Hitchcock, Sr., “Timing Verification and the Timing Analysis Program,” Proc. 19th Design Automation Conference (June, 1982).
John J. Wallace, “On Automatic Verification of SLIDE Descriptions,” Design Research Center, Carnegie-Mellon University, DRC-01-2-80, Pittsburgh, PA, Aug., 1979.
David E. Wallace, “Abstract Timing Verification for Synchronous Digital Systems,” Computer Science Division, Univ. of Calif. at Berkeley, UCB/CSD 88/425, Berkeley, CA, June 27, 1988.
David L. Dill, “Trace Theory for Automatic Hierarchical Verification of Speed-Independent Circuits,” Dept. of Computer Science, Carnegie-Mellon University, CMU-CS-88-119, Pittsburgh, PA, Feb., 1988.
M. Browne, E. Clarke, D. Dill & B. Mishra, “Automatic Verification of Sequential Circuits Using Temporal Logic,” Dept. of Computer Science, Carnegie-Mellon University, CMU-CS-85-100, Pittsburgh, PA, Dec, 1984.
Patrick C. McGeer & Robert K. Brayton, “Timing Analysis in Precharge/Unate Networks,” Proc. 27th Design Automation Conference (June, 1990).
Tod Amon & Gaetano Borriello, “On the Specification of Timing Behavior,” Proceedings of the 1990 ACM International Workshop on Timing Issues in the Specification and Synthesis of Digital Systems (TAU '90), New York, NY, SIGDA(Aug., 1990).
Dimitrie Doukas & Andrea S. LaPaugh, “CLOVER: A Timing Constraints Verification System,” Proceedings of the 1990 ACM International Workshop on Timing Issues in the Specification and Synthesis of Digital Systems (TAU '90), New York, NY, SIGDA (Aug., 1990).
F. Mavaddat & T. Gahlinger, “On Deducing Tight Bounds from Partial Timing Specifications,” Proceedings of the 1990 ACM International Workshop on Timing Issues in the Specification and Synthesis of Digital Systems (TAU '90), New York, NY, SIGDA (Aug., 1990).
Michael C. McFarland, “CPA: Giving an Account of Timed System Behavior,” Proceedings of the 1990 ACM International Workshop on Timing Issues in the Specification and Synthesis of Digital Systems (TAU '90), New York, NY, SIGDA(Aug., 1990).
Alan R. Martello & Steven P. Levitan, “Causal Timing Verification,” Proceedings of the 1990 ACM International Workshop on Timing Issues in the Specification and Synthesis of Digital Systems (TAU '90), New York, NY, SIGDA (Aug., 1990).
Alan R. Martello, Steven P. Levitan & Donald M. Chiarulli, “Timing Verification Using HDTV,” Proc. 27th Design Automation Conference (June, 1990).
Srinivas Devadas, Kurt Keutzer, Sharad Malik & Albert Wang, “Verification of Asynchronous Interface Circuits with Bounded Wire Delays,” Proc. 1992 Inter. Conf. for Computer-Aided Design (Nov., 1992).
Alan R. Martello, “Temporal Specification Verification,” Dept. of Elect. Eng., University of Pittsburgh, PhD. Dissertation (in preparation).
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Martello, A.R., Levitan, S.P. (1993). Temporal analysis of time bounded digital systems. In: Milne, G.J., Pierre, L. (eds) Correct Hardware Design and Verification Methods. CHARME 1993. Lecture Notes in Computer Science, vol 683. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0021712
Download citation
DOI: https://doi.org/10.1007/BFb0021712
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-56778-3
Online ISBN: 978-3-540-70655-7
eBook Packages: Springer Book Archive