The bibliographic entry was discovered and compiled by a machine, and published without a person checking it against the publication. The publication itself is the authors' own work — this badge says nothing about it.
Formal Verification of Nonlinear Analog Circuits using State Space-Based Model Order Reduction
From OpenAlex, which stores abstracts as an
index of words and their positions: what is shown is rebuilt from that,
and reads fluently whether or not it is what the author wrote.
Abstract
Safety-relevant analog implementations of, e.g., sensor-actuator interfaces, demand formal verification methodologies. However, a direct formal verification is not feasible due to the complexity and nonlinearity of analog circuits. This paper employs a state space-based nonlinear model order reduction (MOR) approach with well-suited model order reduction techniques for linearization points. From the original method of sampling the nonlinear state space and clustering the sampled points into regions with similar dynamic behavior, we replaced the dominant pole MOR with a modified Krylov subspace projection method based on Padé-via-Lanczos (PVL). The reduced model quality improves and becomes numerically stable enough to handle analog circuits with hundreds or more (parasitic) poles. The generated Hybrid Automata (HA) can be utilized for formal verification via reachability analysis. We demonstrated the effectiveness of our approach on four nonlinear analog circuits accomplishing significantly less approximation errors of 25X compared to other MOR methods.
@misc{abuhaeyeh2024formal,
title = {Formal Verification of Nonlinear Analog Circuits using State Space-Based Model Order Reduction},
author = {Yasmine Abu-Haeyeh and Lars Hedrich},
year = {2024},
journal = {International Conference on Synthesis, Modeling, Analysis and Simulation Methods and Applications to Circuit Design},
pages = {1--4},
doi = {10.1109/smacd61181.2024.10745444},
}