AUTOMATIC VERIFICATION OF ASYNCHRONOUS CIRCUITS USING TEMPORAL LOGIC

A method is presented for automatically verifying asynchronous sequential circuits using temporal logic specifications. The method takes a circuit described in terms of Boolean gates and Muller elements, and derives a state graph that summarises 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.