Automatic verification of asynchronous circuits using temporal logic

TLDR

The paper proposes an automatic verification method for asynchronous sequential circuits based on temporal logic specifications. The approach models the circuit with Boolean gates and Muller elements, constructs a state graph of all possible executions under finite delays, encodes correct behavior in CTL, and verifies it using a model checker. The method uncovered a timing error in a published arbiter design and produced a corrected, verified version.

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