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.

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 $\mathrm{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.

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.

This work contains the design and test of a control scheme for a fixed-wing aircraft to track 4-dimensional waypoints. The controller scheme is a multi-loop design that consists of an inner controller synthesized with the h-infinity loop-shaping method and an outer controller synthesized with the PID method. Multiple inner-loop controllers are synthesized in a state-machine configuration as a measure against saturation windup.