Publikation
Formal Verification of Error Bounds for Resistive-Switching-based Multilevel Matrix-Vector Multipliers
Kemal Çağlar Coşkun; Chandan Jha; Muhammad Hassan; Rolf Drechsler
In: 26th International Symposium on Quality Electronic Design (ISQED'25). International Symposium on Quality Electronic Design (ISQED-2025), April 23-25, San Francisco, USA, 2025.
Zusammenfassung
The need for performance and energy efficiency by
expanding technologies such as internet-of-things devices and
artificial neural networks (ANNs) has led to the exploration of
in-memory computing paradigms, specifically utilizing resistiveswitching memory (RSM) based analog and multilevel matrixvector multipliers (MVMs). However, nonidealities in these MVMs
cause larger-than-expected deterioration in the output quality
and introduce errors with potentially catastrophic consequences
in safety-critical applications such as autonomous vehicles, medical diagnosis, and control systems. Therefore, to enable the
use of MVMs in such applications, the error bounds of the
MVMs must be formally verified, which, to our knowledge,
remains unaddressed. In this paper, we aim to address this
gap with a formal verification methodology for finding the
maximum possible error in resistive-switching-based multilevel
MVMs. We introduce three approaches to compute the maximum
error and provide a polynomial-time solution as our primary
contribution, which reduces the computation time by up to 2181
times. Additionally, we provide a tracing feature for error source
identification and debugging, enabling targeted enhancements of
the design. We demonstrate the methodology’s efficiency with a
timing analysis and its effectiveness through a case study using
the metrics of a fabricated design from the literature. We made
the source code of our software implementation publicly available
to promote further research in the use of multilevel MVMs in
safety-critical applications.