Statistical model checking of mixed-analog circuits with an application to a third order Δ - Σ modulator

Abstract

In this paper, we consider verifying properties of mixedsignal circuits, i.e., circuits for which there is an interaction between analog (continuous) and digital (discrete) quantities. We follow the statistical Model Checking approach of [You05, You06] that consists of evaluating the property on a representative subset of behaviors, generated by simulation, and answering the question of whether the circuit satisfies the property with a probability greater than or equal to some value. The answer is correct up to a certain probability of error, which is prespecified. The method automatically determines the minimal number of simulations needed to achieve the desired accuracy, thus providing a convenient way to control the trade-off between precision and computational cost. We propose a logic adapted to the specification of properties of mixed-signal circuits, in the temporal domain as well as in the frequency domain. Our logic is unique in that it allows us to compare the Fourier transform of two signals.We demonstrate the applicability of the method on a model of a third order Δ - Σ modulator for which previous formal verification attempts were too conservative and required excessive computation time. © Springer-Verlag Berlin Heidelberg 2009.