ABSTRACT
Boolean satisfiability (SAT) based methods have traditionally been popular for formally verifying properties for digital circuits.
1. INTRODUCTION
Digital design flows have been helped considerably by CAD tools that enable designs with almost a billion devices today.
(page1, col 2)
The first attempts at applying digital verification techniques to the analog domain were presented in [11].
2. SPICE-BASED CIRCUIT SIMULATION
A circuit simulation problem that SPICE [14] solves is simply a
set of KCL (Kirchoff’s Current Law) equations.
3. SAT-BASED CIRCUIT SIMULATION
3.1 Interval representation of I-V characteristics
For constructing the table, we introduce the notion of independent
variables (x1, x2, ..., xN) and dependent variables (y1, y2, ..., yM)
for the voltage and current variables, respectively, for the different
devices.
There is no fixed methodology for choosing the set of voltage
or current variables as dependent or independent variable from an
algorithmic perspective.
(page 3)
The tables can be built with any transistor parameter (e.g., W,
L, vth, tox, etc.) as independent variable as well
3.2 Adding KVL and KCL Equations
3.3 Setting-up the Different Simulation Types
3.3.1 DC Simulation:
We label the current and voltage variables for a given circuit in
the same way as in an MNA analysis.
(page 3 col 2)
3.3.2 PSS Simulation:
We can extend the DC simulation methodology to pose PSS (Periodic
Steady State) simulations [10] as a SAT problem as well.
In our methodology, for a K-point PSS simulation, we would
createK copies of the DC simulation equations – one for each time
point.
Unlike Spectre, where one needs to specify an estimate of the
oscillation period for PSS analysis, in the SAT model, we can represent
the period of oscillation as an independent variable that also
needs to be solved by the SAT solver (This could be useful for simulating
oscillators where one does not know the exact period.). Making
T as a variable along with vj makes Eqn. 10 a quadratic equation.
Quadratic equations are generally harder to solve than linear.
