Partial-Order Correctness-Preserving Properties of Delay-Insensitive Circuits

Delay-insensitive (DI) circuits are a class of asynchronous circuits that operate correctly regardless of delays in components or wires. We model such circuits using their traces, or sequences of events (signal transitions) that occur during the operation of the circuit. As shown in [16], [9], and [18], 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.