Link: https://eu02web.zoom-x.de/j/66719911736?pwd=N5n96kFJbauLi2u79eJI0ZD15hgNsi.1
4:30pm Central European time is (usually) 7:30am Pacific time and 11:30pm Beijing time
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.
Chandan Kumar Jha received his B.Tech degree from the National Institute of Technology, Meghalaya, India, in 2015 and his Ph.D. in Electrical Engineering from the Indian Institute of Technology, Gandhinagar, India, in 2020. During his B.Tech, he was awarded the Merit Scholarship, and he received both the Visvesvaraya Ph.D. Fellowship and the Intel India Ph.D. Fellowship for his doctoral studies. He has worked as a Postdoctoral Researcher at the Indian Institute of Technology Bombay, India, and the German Research Center for Artificial Intelligence, Germany. Currently, he is a Postdoctoral Researcher at the University of Bremen, Germany. His research focuses on the design and verification of emerging technologies and computations.
