Automatic Verification of Asynchronous Circuits Using Temporal Logic

CMU-CS-85-125

David L. Dill, Edmund M. Clarke

May 1985

We present a method 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 summarizes all possible circuit executions resulting from any set of finite delays on the outputs of the components. The correct behavior 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, we discover a timing error in a published arbiter design. We give a corrected arbiter, and verify it.

17 pages

Return to: SCS Technical Report Collection
School of Computer Science homepage

This page maintained by [email protected]