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

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. 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...

• Type: Journal
• Year: 2010
• Where: FMSD
• Authors: Edmund M. Clarke, Alexandre Donzé, Axel Legay
• Keywords: Computer Science Department, FMSD 2010, Formal Verification, Mixed-signal Circuits