Automated Generation of Hybrid System Models for Reachability Analysis of Nonlinear Analog Circuits

Abstract — We address the problem of formally verifying non-linear analog circuits with an uncertain initial set by computing their reachable set. A reachable set contains the union of all possi-ble system trajectories for a set of uncertain states and as such can be used to provably check whether undesired behavior is possible or not. Our method is based on local linearizations of the non-linear circuit, which naturally results in a piecewise-linear sys-tem. To substantially limit the number of required locations, our approach computes linearized locations on-the-fly depending on which states are reachable. We can show that without the pro-posed on-the-fly technique, the conversion to piecewise-linear sys-tems is infeasible even for a few nonlinear semiconductor devices (discrete state-space explosion problem). Our method is fully au-tomatic and only requires a circuit netlist. Piecewise-linear sys-tems have gained popularity not only for verification, but also for accelerated simulation of nonlinear circuits. Our method pro-vides a guaranteed bound on the number of linearization loca-tions that have to be explicitly computed for such a nonlinear cir-cuit. I