Graph-Based, Formal Equivalence Checking Method

A new research paper titled “Equivalence Checking of System-Level and SPICE-Level Models of Linear Circuits” was published by researchers at University of Bremen and DFKI GmbH.

Abstract:
“Due to the increasing complexity of analog circuits and their integration into System-on-Chips (SoC), the analog design and verification industry would greatly benefit from an expansion of system-level methodologies using SystemC AMS. These can provide a speed increase of over 100,000× in comparison to SPICE-level simulations and allow interoperability with digital tools at the system-level. However, a key barrier to the expansion of system-level tools for analog circuits is the lack of confidence in system-level models implemented in SystemC AMS. Functional equivalence of single Laplace Transfer Function (LTF) system-level models to respective SPICE-level models was successfully demonstrated recently. However, this is clearly not sufficient, as the complex systems comprise multiple LTF modules. In this article, we go beyond single LTF models, i.e., we develop a novel graph-based methodology to formally check equivalence between complex system-level and SPICE-level representations of Single-Input Single-Output (SISO) linear analog circuits, such as High-Pass Filters (HPF). To achieve this, first, we introduce a canonical representation in the form of a Signal-Flow Graph (SFG), which is used to functionally map the two representations from separate modeling levels. This canonical representation consists of the input and output nodes and a single edge between them with an LTF as its weight. Second, we create an SFG representation with linear graph modeling for SPICE-level models, whereas for system-level models we extract an SFG from the behavioral description. We then transform the SFG representations into the canonical representation by utilizing three graph manipulation techniques, namely node removal, parallel edge unification, and reflexive edge elimination. This allows us to establish functional equivalence between complex system-level models and SPICE-level models. We demonstrate the applicability of the proposed methodology by successfully applying it to complex circuits.”

Find the open access technical paper here. Published June 2022.

Coşkun, K.Ç.; Hassan, M.; Drechsler, R. Equivalence Checking of System-Level and SPICE-Level Models of Linear Circuits. Chips 2022, 1, 54-71. https://doi.org/10.3390/chips1010006.