Source author record

J Strother Moore

J Strother Moore appears in the imported research catalog. Authorship, coauthor and topic links are available while profile ownership is still unclaimed.

ResearcherUnclaimed source record

Logic in Computer Science Mathematical Software Artificial Intelligence Symbolic Computation

Catalog footprint

What is connected

4works

4topics

3close collaborators

Actions

Connect this record

Open graph Browse works

Inspect adjacent papers, topics, institutions and collaborators without losing the researcher page.

Building this map preview

BZPEER is loading the nearby papers, people, topics and institutions for this page.

preprint2022arXiv

VWSIM: A Circuit Simulator

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.

preprint2014arXiv

Enhancements to ACL2 in Versions 6.2, 6.3, and 6.4

We report on improvements to ACL2 made since the 2013 ACL2 Workshop.

preprint2013arXiv

Enhancements to ACL2 in Versions 5.0, 6.0, and 6.1

We report on highlights of the ACL2 enhancements introduced in ACL2 releases since the 2011 ACL2 Workshop. Although many enhancements are critical for soundness or robustness, we focus in this paper on those improvements that could benefit users who are aware of them, but that might not be discovered in everyday practice.

preprint2011arXiv

How Can I Do That with ACL2? Recent Enhancements to ACL2

The last several years have seen major enhancements to ACL2 functionality, largely driven by requests from its user community, including utilities now in common use such as 'make-event', 'mbe', and trust tags. In this paper we provide user-level summaries of some ACL2 enhancements introduced after the release of Version 3.5 (in May, 2009, at about the time of the 2009 ACL2 workshop) up through the release of Version 4.3 in July, 2011, roughly a couple of years later. Many of these features are not particularly well known yet, but most ACL2 users could take advantage of at least some of them. Some of the changes could affect existing proof efforts, such as a change that treats pairs of functions such as 'member' and 'member-equal' as the same function.