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

authored by

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.

Organisation(s)

Mixed-Signal Circuits Section
L3S Research Centre

Type

Paper

Pages

1-4

Publication date

2020

Publication status

Published

Peer reviewed

Yes

ASJC Scopus subject areas

Hardware and Architecture, Electrical and Electronic Engineering, Safety, Risk, Reliability and Quality

Electronic version(s)

https://doi.org/10.1109/ddecs50862.2020.9095655 (Access: Closed)