In this paper, we present an optimized methodology for performing state-space-based equivalence checking of nonlinear analog circuits by using a gradient-ascent-based search algorithm to efficiently traverse a common state space. Essentially, the method searches for critical regions where the functional behaviors of two circuit designs show the greatest divergence. The key challenges in this approach are the mapping of both designs onto a common canonical state space, the computation of the gradient, and the exclusion of unreachable regions within the state space. To address the first challenge, we use locally linearized systems and leverage the Kronecker Canonical Form (KCF). To facilitate the computation of the gradient, we employ a purpose-built target function, and to exclude unreachable regions, we utilize vector projection techniques. Through experiments with nonlinear analog circuits and a scalability analysis, we demonstrate the successful and efficient computation performed with the proposed methodology, achieving speedups of up to 468 times.

In-Memory Computing (IMC) using memristors has gained significant interest in recent years as it addresses the issue of memory bottleneck in the von Neumann architectures. One of the most popular design styles that have been developed to perform memristor-based IMC is Memristor-Aided loGIC (MAGIC). MAGIC design style based NOR and NOT operations can be used to perform IMC on memristor crossbars. The state-of-the-art SIMPLER MAGIC tool is used to generate a mapping of any arbitrary Boolean function to MAGIC operations that are suitable for high-throughput applications. The correctness of the mapping is examined by tedious manual inspections and functional simulations which may not account for all the edge cases which is not desirable. In this work, we alleviate this issue to the best of our knowledge for the first time by proposing veriSIMPLER. veriSIMPLER is an automated formal verification methodology to ensure the functional correctness of the mapping obtained using the SIMPLER MAGIC tool. The veriSIMPLER methodology generates Boolean Satisfiability Formulas (SAT) of the mapping obtained using the SIMPLER MAGIC tool and the golden reference Verilog designs. These SAT formulas are verified against each other using the Z3 solver. The veriSIMPLER methodology identified a critical bug in the mapping obtained from the SIMPLER MAGIC tool when buffers are connected between input and output. We also propose a methodology to patch this bug to generate the correct mapping, which in turn extends the capability of the SIMPLER MAGIC tool to handle buffers on top of providing a formal verification methodology. We have used a variety of benchmark circuits from the widely used ISCAS’85, ISCAS’89, ITC’99, and IWLS’93 to show the efficacy of the veriSIMPLER methodology. We aim to make the formally verified mapping obtained using the veriSIMPLER methodology open-source to promote further research in this direction.

Recently, Signal Flow Graphs (SFGs) have been successfully leveraged to show equivalence for linear analog circuits at system-level and SPICE-level. However, this is clearly not sufficient as the true complexity stems from nonlinear analog circuits. In this paper, we go beyond linear analog circuits, i.e., we extend the SFGs and develop the Modified Signal-Flow Graph (MSFG), to show equivalence between system-level and SPICE-level representations of static nonlinear analog circuits. First, we map the nonlinear circuits to MSFGs. Afterwards, graph simplification and functional approximation (in particular Legendre polynomials) techniques are used to create minimal MSFG and canonical MSFG. This enables us to compare the MSFGs even if they have vastly different structures. Finally, we propose a similarity metric that calculates the similarity between SPICE-level and system-level models. By successfully applying the proposed equivalence checking technique to benchmark circuits, we demonstrate its applicability.

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, which provide speed benefits in comparison to SPICE 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. To overcome this, functional equivalence of system-level models to respective SPICE-level models needs to be demonstrated. In this paper, we develop a novel, graph-based methodology to formally check equivalence between system-level and SPICE-level representations of linear analog filter circuits, such as Low-Pass Filters (LPF). To do this, we propose an intermediate representation in the form of a Signal-flow Graph (SFG), which acts as a mapping function from the SPICE-level to the system-level. We create the intermediate representation with linear graph modeling from the SPICE-level model and use graph manipulation to transform the intermediate representation to the equivalent system-level model. We demonstrate the applicability of the proposed methodology by successfully applying it to two example filters.