Analog Circuit Verification by Statistical Model Checking

From bibtex.

Abstract

With increasing integration density and substantially smaller feature sizes, a greater concern of analog designers is circuit resiliency under heavy process variability. Since process variation brings stochastic effects into the model, verifying an analog circuit becomes the problem of verifying that a stochastic system satisfies a certain property. This paper applies statistical model checking to analog circuit models simulated by SPICE: randomly sampled system traces are generated sequentially using SPICE and passed to a trace checker for a bounded linear temporal logic specification until the desired statistical strength is achieved. Sequential Bayesian hypothesis testing and Bayesian estimation are used, so the technique cannot guarantee a correct answer, but the probability of giving a wrong answer can be made arbitrarily small. Results are compared against Monte Carlo sampling on transient properties of analog circuits.