SAT-based Verification for Analog and Mixed-signal Circuits

摘要

The wide application of analog and mixed-signal (AMS) designs makes the verification of AMS circuits an important task. However, verification of AMS circuits remains as a significant challenge even though verification techniques for digital circuits design have been successfully applied in the semiconductor industry.In this thesis, we propose two techniques for AMS verification targeting DC and transient verifications, respectively. The proposed techniques leverage a combination of circuit modeling, satisfiability (SAT) and circuit simulation techniques.For DC verification, we first build bounded device models for transistors. The bounded models are conservative approximations to the accurate BSIM3/4 models. Then we formulate a circuit verification problem by gathering the circuit's KCL/KVL equations and the I-V characteristics which are constrained by the bounded models. A nonlinear SAT solver is then recursively applied to the problem formula to locate a candidate region which is guaranteed to enclose the actual DC equilibrium of the original circuit. In the end, a refinement technique is applied to reduce the size of candidate region to a desired resolution. To demonstrate the application of the proposed DC verification technique, we apply it to locate the DC equilibrium points for a set of ring oscillators. The experimental results show that the proposed DC verification technique is efficient in terms of runtime.For transient verification, we perform reachability analysis to verify the dynamic property of a circuit. Our method combines circuit simulation SAT to take advantage of the efficiency of simulation and the soundness of SAT. The novelty of the proposed transient verification lies in the fact that a significant part of the reachable state space is discovered via fast simulation while the full coverage of the reachable state space is guaranteed by the invoking of a few SAT runs. Furthermore, a box merging algorithm is presented to efficiently represent the reachable state space using grid boxes. The proposed technique is used to verify the startup condition of a tunnel diode oscillator and the phase-locking of a phase-locked loop (PLL). The experimental results demonstrate that the proposed transient verification technique can perform reachability analysis for reasonable complex circuits over a great number of time steps.