Details
| Original language | English |
|---|---|
| Title of host publication | 2020 18th IEEE International New Circuits and Systems Conference (NEWCAS) |
| Pages | 66-69 |
| Number of pages | 4 |
| ISBN (electronic) | 9781728170442 |
| Publication status | Published - 2020 |
Abstract
With the advancements in analog/mixed-signal (AMS) systems and continuously shrinking design sizes, there is an increased demand for reliable verification to ensure correct behavior. To overcome this obstacle, using formal verification is a promising option. We present a modeling system that automatically provides dependable set-valued models from circuit netlists in a form suitable for reachability analysis. Our method is based on local linearizations of the nonlinear circuit. Linearized locations are computed on-the-fly depending on which states are reachable to avoid the state-space explosion problem. The set-valued models include device parameter variations, modeling errors and uncertain input stimuli.
Keywords
- Formal verification, Nonlinear analog circuit, Piecewise linear model, Reachability analysis, Uncertainties
ASJC Scopus subject areas
- Computer Science(all)
- Signal Processing
- Engineering(all)
- Electrical and Electronic Engineering
- Engineering(all)
- Safety, Risk, Reliability and Quality
- Physics and Astronomy(all)
- Instrumentation
Cite this
- Standard
- Harvard
- Apa
- Vancouver
- BibTeX
- RIS
2020 18th IEEE International New Circuits and Systems Conference (NEWCAS). 2020. p. 66-69 9159822.
Research output: Chapter in book/report/conference proceeding › Conference contribution › Research › peer review
}
TY - GEN
T1 - Automated Model Generation Including Variations for Formal Verification of Nonlinear Analog Circuits.
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 - With the advancements in analog/mixed-signal (AMS) systems and continuously shrinking design sizes, there is an increased demand for reliable verification to ensure correct behavior. To overcome this obstacle, using formal verification is a promising option. We present a modeling system that automatically provides dependable set-valued models from circuit netlists in a form suitable for reachability analysis. Our method is based on local linearizations of the nonlinear circuit. Linearized locations are computed on-the-fly depending on which states are reachable to avoid the state-space explosion problem. The set-valued models include device parameter variations, modeling errors and uncertain input stimuli.
AB - With the advancements in analog/mixed-signal (AMS) systems and continuously shrinking design sizes, there is an increased demand for reliable verification to ensure correct behavior. To overcome this obstacle, using formal verification is a promising option. We present a modeling system that automatically provides dependable set-valued models from circuit netlists in a form suitable for reachability analysis. Our method is based on local linearizations of the nonlinear circuit. Linearized locations are computed on-the-fly depending on which states are reachable to avoid the state-space explosion problem. The set-valued models include device parameter variations, modeling errors and uncertain input stimuli.
KW - Formal verification
KW - Nonlinear analog circuit
KW - Piecewise linear model
KW - Reachability analysis
KW - Uncertainties
UR - http://www.scopus.com/inward/record.url?scp=85091344917&partnerID=8YFLogxK
U2 - 10.1109/newcas49341.2020.9159822
DO - 10.1109/newcas49341.2020.9159822
M3 - Conference contribution
SN - 978-1-7281-7045-9
SP - 66
EP - 69
BT - 2020 18th IEEE International New Circuits and Systems Conference (NEWCAS)
ER -