Temporal analysis for time-bounded causal digital systems
Alan R. Martello · 1993
This dissertation presents a methodology for performing temporal verification of digital systems with time-bounded delays. We have built a system which performs an analysis and verification of an input specification, represented as causal timing relationships between pairs of signals and temporal requirements which must be maintained for proper system operation. The verification process is the determination whether or not any sequence of causal relations can result in a violation of any requirement. This verification is accomplished by generating the possible system behaviors from a set of initial states, and testing whether these behaviors satisfy the requirements specified. The initial states which are used to generate the behaviors are determined automatically from the requirements and the input description. Our fundamental contribution is the ability to correctly generate all possible system behaviors given a causal description and an initial state. This process is complicated by the interaction of bounded time ranges and system state during the generation of the system behaviors. The ability to represent and reason about time ranges for transitions in the system is a distinguishing characteristic of our technique and gives our analysis method both its power and complexity.