Details
| Original language | English |
|---|---|
| Article number | 8428606 |
| Pages (from-to) | 1785-1798 |
| Number of pages | 14 |
| Journal | IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems |
| Volume | 38 |
| Issue number | 10 |
| Publication status | Published - Oct 2019 |
Abstract
Formal methods are a promising alternative to simulation-based verification of mixed-signal systems. However, in practice, such methods fail to scale with heterogeneity and complexity of today's analog/mixed-signal systems. Furthermore, it is unclear how they can be integrated into existing verification flows. This paper shows a path to overcome these obstacles. The idea is to use a hierarchical verification flow, in which components can be verified by formal methods or by multirun simulation. To transport verification results across hierarchies, we represent parameters and properties by affine arithmetic decision diagrams. We study to which extent this approach fulfills the needs of practical application by the verification of a phase-locked loop of an IEEE 802.15.4 transceiver system.
Keywords
- Affine arithmetic (AA), analog mixed-signal systems, compositional verification, formal verification
ASJC Scopus subject areas
- Computer Science(all)
- Software
- Computer Science(all)
- Computer Graphics and Computer-Aided Design
- Engineering(all)
- Electrical and Electronic Engineering
Cite this
- Standard
- Harvard
- Apa
- Vancouver
- BibTeX
- RIS
In: IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, Vol. 38, No. 10, 8428606, 10.2019, p. 1785-1798.
Research output: Contribution to journal › Article › Research › peer review
}
TY - JOUR
T1 - Hierarchical Verification of AMS Systems With Affine Arithmetic Decision Diagrams
AU - Zivkovic, Carna
AU - Grimm, Christoph
AU - Olbrich, Markus
AU - Scharf, Oliver
AU - Barke, Erich
N1 - Funding information: Manuscript received March 21, 2018; revised June 14, 2018; accepted July 14, 2018. Date of publication August 7, 2018; date of current version September 18, 2019. This work was supported in part by ANCONA Project within the IKT 2020 Program through the German Ministry of Education and Research under Grant 16ES021, in part by Robert Bosch AG, in part by Intel AG, and in part by Mentor Graphics GmbH. This paper was recommended by Associate Editor F. Bonani. (Corresponding author: Carna Zivkovic.) C. Zivkovic and C. Grimm are with the Design of Cyber-Physical Systems, University of Kaiserslautern, 67653 Kaiserslautern, Germany (e-mail: radojicic@cs.uni-kl.de).
PY - 2019/10
Y1 - 2019/10
N2 - Formal methods are a promising alternative to simulation-based verification of mixed-signal systems. However, in practice, such methods fail to scale with heterogeneity and complexity of today's analog/mixed-signal systems. Furthermore, it is unclear how they can be integrated into existing verification flows. This paper shows a path to overcome these obstacles. The idea is to use a hierarchical verification flow, in which components can be verified by formal methods or by multirun simulation. To transport verification results across hierarchies, we represent parameters and properties by affine arithmetic decision diagrams. We study to which extent this approach fulfills the needs of practical application by the verification of a phase-locked loop of an IEEE 802.15.4 transceiver system.
AB - Formal methods are a promising alternative to simulation-based verification of mixed-signal systems. However, in practice, such methods fail to scale with heterogeneity and complexity of today's analog/mixed-signal systems. Furthermore, it is unclear how they can be integrated into existing verification flows. This paper shows a path to overcome these obstacles. The idea is to use a hierarchical verification flow, in which components can be verified by formal methods or by multirun simulation. To transport verification results across hierarchies, we represent parameters and properties by affine arithmetic decision diagrams. We study to which extent this approach fulfills the needs of practical application by the verification of a phase-locked loop of an IEEE 802.15.4 transceiver system.
KW - Affine arithmetic (AA)
KW - analog mixed-signal systems
KW - compositional verification
KW - formal verification
UR - http://www.scopus.com/inward/record.url?scp=85051369233&partnerID=8YFLogxK
U2 - 10.1109/tcad.2018.2864238
DO - 10.1109/tcad.2018.2864238
M3 - Article
VL - 38
SP - 1785
EP - 1798
JO - IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems
JF - IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems
IS - 10
M1 - 8428606
ER -