Automated generation of hybrid system models for reachability analysis of nonlinear analog circuits

We address the problem of formally verifying nonlinear analog circuits with an uncertain initial set by computing their reachable set. A reachable set contains the union of all possible 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 nonlinear circuit, which naturally results in a piecewise-linear system. 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 proposed on-the-fly technique, the conversion to piecewise-linear systems is infeasible even for a few nonlinear semiconductor devices (discrete state-space explosion problem). Our method is fully automatic and only requires a circuit netlist. Piecewise-linear systems have gained popularity not only for verification, but also for accelerated simulation of nonlinear circuits. Our method provides a guaranteed bound on the number of linearization locations that have to be explicitly computed for such a nonlinear circuit.