veriSiM: Formal Verification of SPICE Netlists for MAGIC-Based Logic-in-Memory

Feb 1, 2026 by C. Jha, Simranjeet Singh, Khushboo Qayyum, Ankit Bende, Muhammad Hassan, Vikas Rana, Farhad Merchant, Rolf Drechsler (IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems)

DOI 10.1109/TCAD.2025.3583199

We built veriSiM, an automated formal verifier that proves SPICE netlists generated for MAGIC memristor Logic-in-Memory are semantically equivalent to the golden Verilog, sidestepping slow SPICE simulation; we translate netlists and Verilog into clauses and piggyback Z3 to check equivalence under clearly defined SPICE-to-clause conditions. This lets you scale correctness checks for medium-to-large MAGIC LiM designs without waiting on circuit-level sims.

source S2, crossref, openalex