Formal verification of speed-dependent asynchronous circuits using symbolic model checking of branching time regular temporal logic

Abstract

Firstly, we show how to deal with bounded uncertain delays of (speed-dependent) asynchronous circuits for symbolic model checking based on temporal logic. We adopt discrete-time model. In the modeling of uncertain delays, we consider two models, i.e. static delay and dynamic delay. These models are interpreted as parameterized sequential machines and nondeterministic sequential machines respecitively. Secondly, we show a symbolic model checking algorithm for the above sequential machines. As a specification description language, a temporal logic named Branching Time Regular Temporal Logic (BRTL) is employed. A prototype of verification system based on the proposed method has been implemented and some experimental results are reported.