RAT-based formal verification of QDI asynchronous controllers

This paper presents a new method for formally verifying asynchronous circuits with a symbolic model checking tool called RAT. The main idea is to use a PSL description which models the circuit and gate behaviors. For each circuit, the behavior correctness is formally checked with RAT. The gates are abstracted by their PSL properties. As the gates are assembled together to build a larger circuit, the PSL properties can also be combined to describe the resulting circuit behavior. Therefore this circuit behavior can also be checked by the same method and then abstracted by PSL properties. The method can be applied hierarchically which prevents this formal verification from any explosion of the state number. In order to illustrate this technique, a case study-a QDI controller based on communicating elements called sequencers-is presented.