Levitan This research is on verifying timing specifications for interconnection of modules in both synchronous and asynchronous digital systems. The notion of temporal behavior is being abstracted from the notion of functional behavior by focusing primarily on the control protocols of the modules and ignoring the data values computed by the modules. In this model, the interface protocols of each module are given along with the connectivity between modules. A static graph is built that describes the temporal relationships among all the external signals of all the modules. The verification process is based on a comparison between the possible behaviors of the system, represented by the graph, and the legal behaviors as represented by a set of constraints. The key constraint is that the temporal behavior of one module cannot violate the temporal constraints of another module within the system. The algorithms support multiple system states, state transitions, and checking of conditionals and loops within the protocols. This searching is tractable because functional behavior and data values generated by modules are not considered.
