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 Delta-I pound modulators for which previous formal verification attempts were too conservative and required excessive computation time.