Invited talk from Victor Konrad

Abstract: The problems of analog verification are daunting. There is not much to draw upon in the digital toolkit, because analog circuits exhibit characteristics that are very different from those of digital systems. Variables (time, voltages, currents etc.) are continuous, or "dense" rather than discrete; as a result, the state space of a circuit, even one of modest dimensionality, is huge. Compositionality is difficult, because any two connected components mutually affect each other. The behavior of analog components is governed by differential and algebraic, often nonlinear, equations rather than finite state machines. Furthermore, today's sophisticated device models render these equations so complicated that, for any circuit of realistic size, they are impossible to write down explicitly (let alone solve analytically), and the only way to examine the circuit~s behavior is to run Spice and eye-ball the resulting waveforms to ascertain that the circuit works as expected. This process is very computation-intensive and involves much human effort, especially when multiple Spice runs are required to test the behavior in multiple process corners. In addition, the advent of mixed-signal design, where some pieces are modeled as digital finite-state machines and some have continuous dynamics, has added challenges of its own.
Techniques and tools that have stood us in good stead in the digital world are only beginning to emerge in the analog domain. These include languages to specify analog properties, formal system analysis, mixed-mode modeling and simulation, and smart Monte Carlo exploration using Spice. This is a researcher's paradise.