Combining Symbolic Simulation and Interval Arithmetic for the Verification of AMS Designs

Abstract--Analog and mixed signal (AMS) designs are important integrated circuits that are usually needed at the interface between the electronic system and the real world. Recently, several formal techniques have been introduced for AMS verification. In this paper, we propose a difference equations based bounded model checking approach for AMS systems. We define model checking using a combined system of difference equations for both the analog and digital parts, where the state space exploration algorithm is handled with Taylor approximations over interval domains. We illustrate our approach on the verification of several AMS designs including modulator and oscillator circuits.

• Type: Conference
• Year: 2007
• Where: FMCAD
• Authors: Mohamed H. Zaki, Ghiath Al Sammane, Sofiène Tahar, Guy Bois
• Keywords: AMS Verification, Difference Equations, FMCAD 2007, Formal Methods, Model Checking