First steps towards SAT-based formal analog verification

Boolean satisfiability (SAT) based methods have traditionally been popular for formally verifying properties for digital circuits. We present a novel methodology for formulating a SPICE-type circuit simulation problem as a satisfiability problem. We start with a circuit level netlist, capture the non-linear behavior of the circuits at the transistor level via conservative approximations and transform the simulation problem into a search problem that can be exhaustively explored via a SAT solver. Thus, for DC as well as fixed time-step based transient and periodic steady state (PSS) simulation formulations, the solutions produced by the solver are formal in nature. We also present algorithms for abstraction refinement and smart interval generation to improve the computational efficiency of our proposed solution scheme. We have implemented our ideas into a tool called fSpice which is the first attempt at building a formal SPICE engine. We demonstrate the applicability of our ideas by showing experimental results using pruned versions of real designs that faced challenges during chip tape-out.