Combining symbolic simulation and interval arithmetic for the verification of AMS designs
Mohamed H. Zaki, Ghiath Al-Sammane, Guy Bois · 2015
Abstract—Analog and mixed signal (AMS) designs are impor-tant integrated circuits that are usually needed at the interface be-tween 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 explo-ration 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. I.