Modelling timing assumption with trace theory

An extension of trace theory is described that allows for the verification of asynchronous circuits that are not speed-independent, but instead rely on assumptions about the delays of their components for correct operation. The theory has been implemented in an automatic verifier that checks whether a circuit satisfies a given formal specification in time linear in the number of states of both the specification and the circuit. The ability of the verifier to model timing assumptions greatly expands the class of circuits that can be automatically verified, making the verifier a more useful tool in the design of asynchronous circuits. The verifier is demonstrated on a self-timed queue element