Formal Analysis of Quasi Delay Insensitive Circuits Behavior in the Presence of SEUs

Asynchronous circuits are often claimed as being an interesting alternative to design robust systems against faults. In this study, a method is proposed to model the behavior of quasi delay insensitive (QDI) asynchronous circuits in the presence of SEUs (memory bit flips). The circuits and the fault injection process are both described using this model. The method, based on symbolic simulation, consists of exploring all the reachable states in the presence of faults in order to draw up an exhaustive list of behaviors. A case study shows that this method enables us to verify some properties on the circuits. SEU resistance can be formally proven using this analysis.