Safety Verification of AMS Circuits with Piecewise-Linear System Reachability Analysis
Seyoung Kim, Heechun Park, Jaeha Kim · 2021
Reachability analysis is a key to safety verification, which computes the boundary of all possible states reachable by a system starting from a range of initial conditions. The challenge of extending the reachability analysis to analog/mixed-signal (AMS) circuits involves mitigating the curse of dimensionality when expressing the reachable set and computing their time evolution within the multi-dimensional continuous state space. The proposed method addresses this problem by modeling a nonlinear, analog circuit as a hybrid piecewise-linear (PWL) system and computing the exact trajectory of a parallelotope-shaped state region of a PWL subsystem using the Laplace-domain analysis. The experimental results with a DC-DC buck converter example demonstrate the runtime scaling of O(N2) when computing the exact reachable set of the circuit with N elements.