Sciweavers

ICCAD
2009
IEEE

First steps towards SAT-based formal analog verification

13 years 7 months ago
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 e. 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 ex...
Saurabh K. Tiwary, Anubhav Gupta, Joel R. Phillips
Added 18 Feb 2011
Updated 18 Feb 2011
Type Journal
Year 2009
Where ICCAD
Authors Saurabh K. Tiwary, Anubhav Gupta, Joel R. Phillips, Claudio Pinello, Radu Zlatanovici
Comments (0)