As VLSI fabrication technology progresses to 65nm feature sizes and smaller, transistors no longer operate as ideal switches. This motivates verifying digital circuits using continuous models. This paper presents the verification of the high-speed, toggle flip-flop proposed by Yuan and Svensson [1]. Our approach builds on the projection based methods originally proposed by Greenstreet and Mitchell [2], [3]. While they were only able to demonstrate their approach with two- and threedimensional systems, we apply projection based analysis to a seven-dimensional model for the flip-flop. We believe that this is the largest verification to date of a digital circuit using non-linear circuit-level models. In this paper, we describe how we overcame problems of numerical errors and instability associated with the original projection based methods. In particular, we present a novel linear-program solver and new methods for constructing accurate linear approximations of non-linear dynamics. We use the toggle flip-flop as an example and consider how these methods could be extended to verify a standard cell library for digital design.
展开▼
