Formal verification of analog transistor level circuits is still an open problem. In this paper we present a methodology which automatically abstracts a very accurate sampled analog circuit block using a reachability tool with SPICE-accuracy. The resulting hybrid automata (HA) models the - in most analog circuits desired - linear behavior, but also the technology dependent nonlinear and limiting behavior.We present several abstraction variants and evaluate the accuracy of the model using some simulations of the SPICE-netlist and the HA. Finally, we show that it can be used for formal verification on high level with reachability tools.
展开▼
