Automatically Generated Nonlinear Analog Circuit Models Enclosing Variations with Intervals and Affine Forms for Reachability Analysis

In contrast to the formal verification of digital circuits, analog formal verification requires appropriate tolerances of the device parameters. Enclosing these tolerances in set-valued models leads to unwanted overapproximation. In this paper, we present an automated modeling approach, which is applicable to nonlinear analog and mixed-signal circuits. We describe the behavioral circuit models as well as the device parameter variations and modeling errors by symbolic equations. We substitute these symbols with intervals and affine forms, respectively. In each case we provide semi-symbolic hybrid automata models. Then, we insert numerical values in these models for reachability analysis. The results of both reachability analyses are used to reduce the overapproximation.