Reachability Analysis for Nonlinear Analog/Mixed-Signal Circuits With Trajectory-Based Reachable Sets

This paper presents an efficient and scalable reachability analysis algorithm for nonlinear analog/mixed-signal circuits. In particular, it addresses the challenges in computing the time evolution of the reachable set of the circuit's continuous states and its intersection with the guard planes, i.e., the partitioning planes of the equivalent piecewise-linear system modeling the circuit's dynamics. The proposed algorithm utilizes a trajectory form of the reachable set, which can describe its exact evolution over time using analytical expressions until the set crosses one of the guard planes of the system. When it does, a naive computation of the reachable set may require splitting the set into multiple sub-sets, each using its own trajectory form. This is problematic since the number of reachable sets may grow indefinitely over time. To mitigate this, this work proposes a way of processing a group of reachable sets together that cross a common guard plane during a finite time interval. This method can keep the number of sets and the associated computational cost constant over time. The experimental results with a DC-DC converter example demonstrate that the proposed algorithm can achieve the average speed-ups of 79-107x compared to the existing algorithms with errors of less than 2%.