On simulation-based probabilistic model checking of mixed-analog circuits

13 years 3 months ago

Download www-verimag.imag.fr

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 satisﬁes the property with a probability greater than or equal to some threshold. We propose a logic adapted to the speciﬁcation 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 diﬀerent models of ∆−Σ modulators for which previous formal veriﬁcation attempts were too conservative and required excessive computation time. 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 Rese...

Edmund M. Clarke, Alexandre Donzé, Axel Leg

Real-time Traffic