veriSIMPLER: An Automated Formal Verification Methodology for SIMPLER MAGIC Design Style Based In-Memory Computing

IEEE Transactions on Circuits and Systems I Regular Papers, vol. 71, pp. 4169–4179

Abstract

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.

Authors 8

1. Chandan Kumar Jha

   University of Bremen

   Affiliation as printed

   Institute of Computer Science, University of Bremen, Bremen, Germany

2. Khushboo Qayyum

   German Research Centre for Artificial Intelligence

   Affiliation as printed

   German Research Centre for Artificial Intelligence (DFKI), Bremen, Germany

3. Kemal Çağlar Coşkun

   University of Bremen

   Affiliation as printed

   Institute of Computer Science, University of Bremen, Bremen, Germany

4. Simranjeet Singh

   Indian Institute of Technology Bombay

   Affiliation as printed

   Department of Electrical Engineering, Indian Institute of Technology Bombay, Mumbai, India

5. Muhammad Hassan

   University of Bremen

   Affiliation as printed

   Institute of Computer Science, University of Bremen, Bremen, Germany

6. Rainer Leupers Aachen Institute for Communication Technologies and Embedded Systems

   RWTH Aachen University

   Affiliation as printed

   Institute for Communication Technologies and Embedded Systems, RWTH Aachen University, Aachen, Germany

7. Farhad Merchant

   Newcastle University

   Affiliation as printed

   School of Engineering, Newcastle University, Newcastle upon Tyne, U.K

8. Rolf Drechsler

   University of Bremen

   Affiliation as printed

   Institute of Computer Science, University of Bremen, Bremen, Germany