Automatically Generated Nonlinear Analog Circuit Models Enclosing Variations with Intervals and Affine Forms for Reachability Analysis.

verfasst von: Malgorzata Rechmal-Lesse, Gerald Alexander Koroa, Yeremia Gunawan Adhisantoso, Markus Olbrich
Abstract: In contrast to the formal verification of digital circuits, analog formal verification requires appropriate tolerances of the device parameters. Enclosing these tolerances in set-valued models leads to unwanted overapproximation. In this paper, we present an automated modeling approach, which is applicable to nonlinear analog and mixed-signal circuits. We describe the behavioral circuit models as well as the device parameter variations and modeling errors by symbolic equations. We substitute these symbols with intervals and affine forms, respectively. In each case we provide semi-symbolic hybrid automata models. Then, we insert numerical values in these models for reachability analysis. The results of both reachability analyses are used to reduce the overapproximation.
Organisationseinheit(en): Fachgebiet Mixed-Signal-Schaltungen
Forschungszentrum L3S
Typ: Paper
Seiten: 1-4
Publikationsdatum: 2020
Publikationsstatus: Veröffentlicht
Peer-reviewed: Ja
ASJC Scopus Sachgebiete: Hardware und Architektur, Elektrotechnik und Elektronik, Sicherheit, Risiko, Zuverlässigkeit und Qualität
Elektronische Version(en): https://doi.org/10.1109/ddecs50862.2020.9095655 (Zugang: Geschlossen)