Formal verification of mixed-signal designs using extended affine arithmetic

The complexity and heterogeneity of today's mixed-signal systems makes verification a challenge. A particular challenge is the sensitivity of analog parts to variations in parameters, inputs, or initial conditions. We present a methodology for formal verification of mixed-signal systems that verifies the impact of variations of parameters, inputs, or initial conditions on specified properties. Compared with state of the art, the proposed methodology can be integrated easily in existing design flows, handles analog and digital parts, and offers improved scalability. The method is applied on a third order ΣΔ Modulator for verifying the stability property. The results show that our approach is using one simulation run able to find the input sequence that could lead to the undesired system behavior. These values are often not trivial and most likely would never be detected by traditional simulation-based techniques.