Safety Verification of Analog Mixed-Signal Circuits Using Reachability Analysis

Abstract

This dissertation proposes a methodology to verify the safe operation of analog mixed-signal (AMS) circuits under formal specifications. With integrating many AMS integrated circuits (IC) in a car, assuring the safety of the system is getting a critical issue for developing such safety-critical systems. While the operating ranges of analog circuits and their semiconductor devices such as MOSFETs and diodes should be limited under safe-operating area (SOA) specified in the process design kit (PDK) or datasheets, the existing verification procedures relying on SPICE simulations in industry lack of capability to cover all possible dynamic behavior that causes the change of the applied terminal voltages or branch current of the devices. The formal verification algorithm, especially reachability analysis (RA), can prove that the system is safe by computing all reachable states from the specified initial conditions and finding if the reachable set of states intersects with the unsafe set of states causing failures of devices or circuits. However, computing the reachable set is burdensome for practical circuits since it takes too long to compute reachable sets in a high dimensional system dynamically operating in a high frequency, due to the continuous nature of the states that require quantization to many discrete steps of continuous value. This dissertation addresses the challenges while applying reachable analysis to AMS circuits and proposes an efficient way to compute reachable sets. The proposed RA algorithm can compute the reachable set of analog mixed-signal circuits in a fast and accurate way by proposing a novel trajectory form of zonotope, combining two main ideas using scalable geometric set representation, such as zonotope and the XMODEL algorithm that computes analog signals in a trajectory form that represents the signal in a closed functional form with few algebraic coefficients. Any analog circuits, even those containing nonlinear components can be analyzed using the efficient piecewise-linear (PWL) approximation technique that only partitions the state space of the circuit depending on the operating modes of the included devices. The resulting PWL system in the partitioned state space with several sub-regions is more difficult to be computed with conventional RA algorithms relying on time discretization since it calls for many additional computationally expensive geometric intersection operations, resulting in exponentially increasing runtimes with the number of transitions over sub-regions. Applying the proposed trajectory form is not straightforward because the intersection between the trajectory form and the switching boundary can not maintain the same form, requiring additional segmentation of the set shapes to keep the original form as before. Recognizing that every state after the intersection starts from the boundary plane, by computing the time evolution of the boundary itself, it has been shown that the associated computation can be done with the proposed trajectory form without increasing runtime. The proposed method was demonstrated by verifying the exemplary DC-DC switching converters, yielding over 107x speed-up than the existing reachability analysis algorithm in SpaceEx. The computational complexity for state dimensions was reduced by two orders than SpaceEx without losing accuracy, compared to the bound obtained equivalent Monte-Carlo simulations. Finally, SOA for DC-DC converters varying circuit parameters was derived and compared to typical 90-nm process criteria, showing the proposed method usable for verifying SOA specification of AMS circuits.