Statistical Model Checking : An Overview <s> Verifying Circuits <s> In this paper we demonstrate a potential extension of formal verification methodology in order to deal with time-domain properties of analog and mixed-signal circuits whose dynamic behavior is described by differential algebraic equations. To model and analyze such circuits under all possible input signals and all values of parameters, we build upon two techniques developed in the context of hybrid (discrete-continuous) control systems. First, we extend our algorithm for approximating sets of reachable sets for dense-time continuous systems to deal with differential algebraic equations (DAEs) and apply it to a biquad low-pass filter. To analyze more complex circuits, we resort to bounded horizon verification. We use optimal control techniques to check whether a Δ-Σ modulator, modeled as a discrete-time hybrid automaton, admits an input sequence of bounded length that drives it to saturation. <s> BIB001 </s> Statistical Model Checking : An Overview <s> Verifying Circuits <s> We show how model checking methods developed for hybrid dynamic systems may be usefully applied for analog circuit verification. Finite-state abstractions of the continuous analog behavior are automatically constructed using polyhedral outer approximations to the flows of the underlying continuous differential and difference equations. In contrast to previous approaches, we do not discretize the entire continuous state space, and our abstraction captures the relevant behaviors for verification in terms of the transitions between "states" (regions of the continuous state space) as a finite state machine in the hybrid system model. The approach is illustrated for two circuits, a standard oscillator benchmark, and a much larger and more realistic delta-sigma (AI) modulator. <s> BIB002 </s> Statistical Model Checking : An Overview <s> Verifying Circuits <s> In this paper, we consider verifying properties of mixed-signal 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 pre-specified. 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. <s> BIB003
In BIB003  , we applied SPRT to verifying properties of mixed-signal circuits, i.e., circuits for which there is an interaction between analog (continuous) and digital (discrete) values. Our first contribution was to propose a version of stochastic discrete-time event systems that fits into the framework introduced by Younes with the additional advantage that it explicitly handles analog and digital signals. We also introduced probabilistic signal linear temporal logic, a logic adapted to the specification of properties for mixed-signal circuits in the temporal domain and in the frequency domain. Our second contribution was the analysis of a ∆−Σ modulator. A ∆−Σ modulator is an efficient Analog-to-Digital Converter circuit, i.e., a device that converts analog signals into digital signals. A common critical issue in this domain is the analysis of the stability of the internal state variables of the circuit. The concern is that the values that are stored by these variables can grow out of control until reaching a maximum value, at which point we say that the circuit saturates. Saturation is commonly assumed to compromise the quality of the analog-to-digital conversion. In BIB001 and BIB002 reachability techniques developed in the area of hybrid systems are used to analyze the stability of a third-order modulator. Their idea is to use such techniques to guarantee that for every input signal in a given range, the states of the system remain stable. While this reachability-based approach is sound, it has important drawbacks such as (1) signals with long duration cannot be practically analyzed, and (2) properties that are commonly specified in the frequency domain rather than in the time domain cannot be checked. Our results show that a simulation-based approach makes it possible to handle properties and signals that are beyond the scope of the reachability-based approach. As an example, in our experiments, we analyze discrete-time signals with 24000 sampling points in seconds, while the approach in BIB001 takes hours to analyze signals with up to 31 sampling points. We are also able to provide insight into a question left open in BIB001 by observing that saturation does not always imply an improper signal conversion. This can be done by comparing the Fourier transform of each of the input analog signals with the Fourier transform of its corresponding digital signal. Such a property can easily be expressed in our logic and Model Checked with our simulation-based approach. We are unaware of other formal verification techniques that can solve this problem. Indeed, numerical techniques cannot reason on an execution at a time.