VWSIM: A Circuit Simulator

Warren A. Hunt Jr.
(The University of Texas; ForrestHunt, Inc.)
Vivek Ramanathan
(The University of Texas; ForrestHunt, Inc.)
J Strother Moore
(The University of Texas; ForrestHunt, Inc.)

VWSIM is a circuit simulator for rapid, single-flux, quantum (RSFQ) circuits. The simulator is designed to model and simulate primitive-circuit devices such as capacitors, inductors, Josephson Junctions, and can be extended to simulate other circuit families, such as CMOS. Circuit models can be provided in the native VWSIM netlist format or as SPICE-compatible netlists, which are flattened and transformed into symbolic equations that can be manipulated and simulated. Written in the ACL2 logic, VWSIM provides logical guarantees about each of the circuit models it simulates. Note, our matrix solving and evaluation routines use Common Lisp floating-point numbers, and work is ongoing to admit these models into ACL2. We currently use VWSIM to help us design self-timed, RSFQ-based circuits. Our eventual goal is to prove properties of RSFQ circuit models. The ACL2-based definition of the VWSIM simulator offers a path for specifying and verifying RSFQ circuit models.

In Rob Sumners and Cuong Chau: Proceedings Seventeenth International Workshop on the ACL2 Theorem Prover and its Applications (ACL2 2022), Austin, Texas, USA, 26th-27th May 2022, Electronic Proceedings in Theoretical Computer Science 359, pp. 61–75.
Published: 24th May 2022.

ArXived at: http://dx.doi.org/10.4204/EPTCS.359.7 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org