Finding All DC Operating Points Using Interval Arithmetic Based Verification Algorithms
Itrat A. Akhter, Justin Reiher and Mark R. Greenstreet
The University of British Columbia
ABSTRACT
This paper applies interval-arithmetic based verification algorithms to circuit verification problems. In particular, we use Krawczyk’s operator to find all DC operating points of CMOS circuits. We present what we believe to be the first, completely automatic verification of the Rambus ring-oscillator start-up problem. Comparisons with the dReal and Z3 SMT shows large performance and scalability advantages to the interval verification approach. We provide an open-source implementation that supports state-of-the-art short-channel device models.
Keywords: AMS verification, Formal verification, Interval arithmetic, SMT solvers.
