Formal verification of analog circuit parameters across variation utilizing SAT

A fast technique for proving steady-state analog circuit operation constraints is described. Based on SAT, the technique is applicable to practical circuit design and modeling scenarios as it does not require algebraic device models. Despite the complexity of representing accurate transistor I/V characteristics, run-time and problem scaling behavior is excellent.