Automatic Verification of Asynchronous Circuits

Asynchronous circuits are often used in interface circuitry where traditional, synchronous design methods are not applicable. However, the verification of asynchronous designs is difficult, because standard simulation techniques will often fail to reveal design errors that are only manifested under rare circumstances. In this paper, we show how asynchronous designs can be modeled as programs in the Synchronized Transitions language, and how this representation facilitates rigorous and efficient verification of the designs using ordered binary diagrams (OBDDs). We illustrate our approach with two examples: a novel design of a transition arbiter and a design of a toggle element from the literature. The arbiter design was derived by correcting an error in an earlier attempt. It is noteworthy that the error in the original design, found very quickly using the methods described in this paper, went unnoticed during more than 50 hours of CPU time simulation 2³¹ state transitions.