Details
| Original language | English |
|---|---|
| Pages | 1-4 |
| Publication status | Published - 2020 |
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.
Keywords
- formal verification, modeling errors, nonlinear analog circuit, parameter variations, piecewise linear model, reachability analysis
ASJC Scopus subject areas
- Computer Science(all)
- Hardware and Architecture
- Engineering(all)
- Electrical and Electronic Engineering
- Engineering(all)
- Safety, Risk, Reliability and Quality
Cite this
- Standard
- Harvard
- Apa
- Vancouver
- BibTeX
- RIS
2020. 1-4.
Research output: Contribution to conference › Paper › Research › peer review
}
TY - CONF
T1 - Automatically Generated Nonlinear Analog Circuit Models Enclosing Variations with Intervals and Affine Forms for Reachability Analysis.
AU - Rechmal-Lesse, Malgorzata
AU - Koroa, Gerald Alexander
AU - Adhisantoso, Yeremia Gunawan
AU - Olbrich, Markus
N1 - Funding information: The authors gratefully acknowledge financial support by the German Research Foundation (DFG) under project number 286525601
PY - 2020
Y1 - 2020
N2 - 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.
AB - 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.
KW - formal verification
KW - modeling errors
KW - nonlinear analog circuit
KW - parameter variations
KW - piecewise linear model
KW - reachability analysis
UR - http://www.scopus.com/inward/record.url?scp=85085864340&partnerID=8YFLogxK
U2 - 10.1109/ddecs50862.2020.9095655
DO - 10.1109/ddecs50862.2020.9095655
M3 - Paper
SP - 1
EP - 4
ER -