Establishing Reachset Conformance for the Formal Analysis of Analog Circuits.

authored by

Niklas Kochdumper, Ahmad Tarraf, Malgorzata Rechmal, Markus Olbrich, Lars Hedrich, Matthias Althoff

Abstract

We present the first work on the automated generation of reachset conformant models for analog circuits. Our approach applies reachset conformant synthesis to add nondeterminism to piecewise-linear circuit models so that they enclose all recorded behaviors of the real system. To achieve this, we present a novel technique to compute the required nondeterminism for the piecewise-linear models. The effectiveness of our approach is demonstrated on a real analog circuit. Since the resulting models enclose all measurements, they can be used for formal verification.

Organisation(s)

Mixed-Signal Circuits Section

External Organisation(s)

Technical University of Munich (TUM)
Goethe University Frankfurt

Type

Conference contribution

Pages

199-204

No. of pages

6

Publication date

2020

Publication status

Published

Peer reviewed

Yes

ASJC Scopus subject areas

Electrical and Electronic Engineering, Computer Science Applications, Computer Graphics and Computer-Aided Design

Electronic version(s)

http://mediatum.ub.tum.de/node?id=1521218 (Access: Open)
https://doi.org/10.1109/ASP-DAC47756.2020.9045120 (Access: Closed)