To perform veri cation 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 speci cation 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.
Alan R. Martello, Steven P. Levitan