Automatic verification of asynchronous circuits using temporal logic

Abstract

A method is presented for automatically verifying asynchronous sequential circuits using temporal logic specifications. The method takes a circuit desctibed in terms of Boolean gates and Muller elements, and derves a state graph that summaries all possible circuit executions resulting from any set of finite delays on the outputs of the components. The correct behaviour of the circuit is expressed in CTL, a temporal logic. This specification is checked against the state graph using a model checker program. Using this method, a timing error in a published arbiter design is discovered. A corrected arbiter is given and verified