Delay-insensitive (DI) circuits are a class of asynchronous circuits that
operate correctly regardless of delays in components or wires. We model
such circuits on the basis of their traces, or sequences of events (signal
transitions) that occur during the operation of the circuit. As shown
previously, DI circuits can be characterized by certain properties
regarding swapping consecutive events in traces.
We focus on the exhaustive verification problem, which determines whether
there is any set of timing and environment conditions under which the
circuit may operate incorrectly. We show that the event-swapping
properties of DI circuits authorize us to verify exhaustively such
circuits by only examining certain special traces instead of all possible
traces.
