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. Categories and Subject Descriptors I.6.5 [Simulation and Modeling]: Model Development General Terms Algorithms, Design

We present a waveform based variational static timing analysis methodology. It is a timing paradigm that lies midway between convention static delay approximations and full dynamic (SPICE-level) analysis. The core idea is to break the modulation of waveforms processed by a circuit into two parts: (a) non-linear circuit elements e.g., transistors, diodes etc. and (b) linear elements: transmission line, RLC network etc. The non-linear and linear parts of the circuit are then solved using a combination of current-source modeling, model order reduction methodology, perturbation analysis and learning-based Galerkin methods which helps us get SPICE-like accuracies. The proposed method is potentially as robust and 10-20times faster than current-source based gate modeling methodologies

Pareto surfaces in the performance space determine the range of feasible performance values for a circuit topology in a given technology. We present a non-dominated sorting based global optimization algorithm to generate the nominal pareto front efficiently using a simulator-in-a-loop approach. The solutions on this pareto front combined with efficient Monte Carlo approximation ideas are then used to compute the yield-aware pareto fronts. We show experimental results for both the nominal and yield-aware pareto fronts for power and phase noise for a voltage controlled oscillator (VCO) circuit. The presented methodology computes yield-aware pareto fronts in approximately 5-6 times the time required for a single circuit synthesis run and is thus practically efficient. We also show applications of yield-aware paretos to find the optimal VCO circuit to meet the system level specifications of a phase locked loop.

Trajectory-based methods offer an attractive methodology for automated, on-demand generation of macromodels for custom circuits. These models are generated by sampling the state trajectory of a circuit as it simulates in the time domain, and building macromodels by reducing and interpolating among the linearizations created at a suitably spaced subset of the time points visited during training simulations. However, a weak point in conventional trajectory models is the reliance on a single, global reduction matrix for the state space. We develop a new, faster method that generates and weaves together a larger set of smaller localized linearizations for the trajectory samples. The method not only improves speedups to 30X over SPICE, but as a side benefit also provides a platform for parametric small-signal simulation of circuits with variational device/process parameters, at a speedup of roughly 200X over SPICE.

Trajectory methods sample the state trajectory of a circuit as it simulates in the time domain, and build macromodels by reducing and interpolating among the linearizations created at a suitably spaced subset of the time points visited during training simulations. Unfortunately, moving from simple to industrial circuits requires more extensive training, which creates models too large to interpolate efficiently. To make trajectory methods practical, we describe a scalable interpolation architecture, and the first implementation of a complete trajectory "infrastructure" inside a full SPICE engine. The approach supports arbitrarily large training runs, automatically prunes redundant trajectory samples, supports limited hierarchy, enables incremental macromodel updates, and gives 3-10X speedups for larger circuits.