Technical Report
Automated
Formal Verification of Analog/RF Circuits in the Presence of Noise
Rajeev
Narayanan, Behzad Akbarpour, Mohamed H. Zaki, Sofiene Tahar and Lawrence C.
Paulson
ABSTRACT
We model and verify analog/RF designs in the presence of noise and process variation using an automated theorem prover. We propose to use stochastic differential equations (SDE) to model the designs, due to the statistical nature of noise. We find a closed form solution for the SDEs based on stochastic calculus, and then integrate the device variation due to 0.18 micron fabrication process and verify properties using the MetiTarski theorem prover. Our approach is illustrated on an inverting Op-amp Integrator, a Band-Gap-Reference Bias and a Sample-and-Hold Bottom-Plate Mixer circuit.
|
|
|
|
