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) values. We use a simulation-based approach that consists of evaluating
the property on a representative subset of behaviors and answering the question of whether the circuit satisfies the property
with a probability greater than or equal to some threshold. 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. We also demonstrate the applicability
of the method on different models of Δ–Σ modulators for which previous formal verification attempts were too conservative and required excessive computation time.
Keywords Probabilistic model-checking - Simulation-based techniques - Mixed-signals circuits verification - Delta-sigma modulators
This research was sponsored by the GSRC (University of California) under contract no. SA423679952, National Science Foundation
under contracts no. CCF0429120, no. CNS0411152, and no. CCF0541245, Semiconductor Research Corporation under contract no. 2005TJ1366,
Air Force (University of Vanderbilt) under contract no. 18727S3, International Collaboration for Advanced Security Technology
of the National Science Council, Taiwan, under contract no. 1010717, and a grant from the Belgian American Educational Foundation.
Two preliminary versions of this paper appear in the Proceedings of the 4th Haifa Verification Conference and in the Proceedings
of the 2nd Workshop on Formal Verification of Analog Circuits, respectively.