Pub-processor-models
Processor Modeling and Hardware Verification
See also the previously mentioned book, Design
and Verification of Microprocessor Systems for High-Assurance
Applications (see pub-books), for a variety of papers by various authors on
processing modeling in ACL2 (and other systems).
- Industrial
Hardware and Software Verification with ACL2. Warren A. Hunt,
Jr., Matt Kaufmann, J Strother Moore, and Anna Slobodova.
In Verified Trustworthy Software Systems (Gardner, P., O'Hearn,
P., Gordon, M., Morrisett, G. and Schneider, F.B., Eds), Philosophical
Transactions A, vol 374, Royal Society Publishing, September, 2017.
- Using x86isa for Microcode Verification. Shilpi Goel and Rob
Sumners. In the Workshop on Instruction Set Architecture
Specification.
-
A
Hierarchical Approach to Formal Modeling and Verification of
Asynchronous Circuits. C. K. Chau. Department of Computer
Science, The University of Texas at Austin. Ph.D. dissertation, May
2019.
-
A
Hierarchical Approach to Self-Timed Circuit Verification.
C. Chau, W. A. Hunt Jr., M. Kaufmann, M. Roncken, and I. Sutherland. In Proceedings of
the 25th IEEE International Symposium on Asynchronous Circuits and Systems (ASYNC 2019),
Hirosaki, Japan, May 2019, pages 105-113. IEEE.
-
Data-Loop-Free Self-Timed Circuit
Verification.
C. Chau, W. A. Hunt Jr., M. Kaufmann, M. Roncken, and I. Sutherland. In Proceedings of
the 24th IEEE International Symposium on Asynchronous Circuits and Systems (ASYNC 2018),
Vienna, Austria, May 2018, pages 51-58. IEEE.
-
Adding
32-bit Mode to the ACL2 Model of the x86 ISA. Alessandro
Coglio and Shilpi Goel. In Proceedings of the 15th International
Workshop on the ACL2 Theorem Prover and Its Applications (ACL2
2018).
-
The x86isa Books: Features,
Usage, and Future Plans. Shilpi Goel. In Proceedings of the 14th
International Workshop on the ACL2 Theorem Prover and Its Applications
(ACL2 2017).
-
Formal
Verification of Application and System Programs Based on a Validation
x86 ISA Model. Shilpi Goel. Department of Computer Science, The
University of Texas at Austin. Ph.D. dissertation, December 2016.
-
Engineering
a Formal, Executable x86 ISA Simulator for Software
Verification. Shilpi Goel, Warren A. Hunt, Jr., and Matt
Kaufmann. In Provably Correct Systems (ProCoS), 2017.
-
Simulation and
Formal Verification of x86 Machine-Code Programs That Make System
Calls. Shilpi Goel, Warren A. Hunt, Jr., Matt Kaufmann, and
Soumava Ghosh. In Formal Methods in Computer-Aided Design (FMCAD),
2014.
-
Automated
Code Proofs on a Formal Model of the x86. Shilpi Goel and Warren
A. Hunt, Jr. In Verified Software: Theories, Tools, Experiments
(VSTTE), 2013.
- Abstract Stobjs and
Their Application to ISA Modeling. Shilpi Goel, Warren A. Hunt,
Jr., and Matt Kaufmann. In Proceedings of the 11th International
Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2013).
-
Modeling
and Verification of Industrial Flash Memories. S. Ray, J. Bhadra,
T. Portlock, and R. Syzdek. In P. Chatterjee and K. Gadepally,
editors, Proceedings of the 11th
International Symposium on Quality Electronic Design (ISQED 2010),
San Jose, CA, March 2010, pages 705-712. IEEE.
-
Optimizing
Equivalence Checking for Behavioral Synthesis. K. Hao, F. Xie,
S. Ray, and J. Yang. In Design, Automation & Test in
Europe (DATE 2010), Dresden, Germany, March 2010. IEEE.
-
Connecting
Pre-silicon and Post-silicon Verification.
S. Ray and W. A. Hunt, Jr.
In A. Biere and C.
Pixley, editors, Proceedings of the 9th International Conference on
Formal Methods in Computer-aided Design (FMCAD 2009), Austin, TX,
November 2009, pages 160-163. IEEE Computer
Society.
-
Formal
Verification for High-Assurance Behavioral Synthesis.
S. Ray, K. Hao, Y. Chen, F. Xie, and J. Yang.
In Z. Liu and A. P. Ravn, editors, Proceedings
of the 7th International
Symposium on Automated Technology for Verification and Analysis (ATVA
2009), Macao SAR, China, October 2009, volume 5799 of LNCS, pages
337-351. Springer.
-
Abstracting
and Verifying Flash Memories, Sandip Ray and Jayanta Bhadra. In K. Campbell, editor,
Proceedings of the 9th Non-Volatile
Memory Technology Symposium (NVMTS 2008), Pacific Grove, CA,
November 2008, pages 100-104. IEEE.
-
A
Mechanized Refinement Framework for Analysis of Custom Memories,
Sandip Ray and Jayanta Bhadra.
In J. Baumgartner and M. Sheeran, editors,
Proceedings of the 7th
International Conference on Formal Methods in Computer-aided Design
(FMCAD 2007), Austin, TX, November 2007, pages 239-242. IEEE Computer
Society.
-
Mechanized
Certification of Secure Hardware Designs, Sandip Ray and Warren
A. Hunt, Jr. In J. Bhadra, L. Wang, and M. S. Abadir,
editors, Proceedings of the 8th
International Workshop on Microprocessor Test and Verification, Common
Challenges and Solutions (MTV 2007), Austin, TX, December 2007.
IEEE Computer
Society.
- Formal Verification of Floating-Point RTL at AMD using the ACL2 Theorem Prover,
David Russinoff, Matt Kaufmann, Eric Smith, Robert Sumners. 17th IMACS World
Congress: Scientific Computation, Applied Mathematics and Simulation. July,
2005.
-
Deductive Verification of Pipelined Machines Using First-order
Quantification, Sandip Ray and Warren A. Hunt Jr.
In R. Alur and D. A. Peled, editors, Proceedings of the
16th International Conference on Computer-aided Verification (CAV 2004),
Boston, MA, July 2004, volume 3117 of LNCS, pages 31-43. Copyright Springer-Verlag.
- Formal Verification
of Microprocessors at AMD, Arthur Flatau, Matt Kaufmann, David F. Reed, David Russinoff,
Eric Smith, and Rob Sumners. Proceedings of Designing Correct Circuits 2002.
- High-Speed, Analyzable Simulators, David Greve, Matthew Wilding, and
David Hardin, Chapter 8 of Computer-Aided
Reasoning: ACL2 Case Studies (Kaufmann, Manolios, Moore, eds.) Kluwer,
2000.
(ACL2 scripts are available from
directory 1999/simulator/ in the community-books.)
High-speed simulation models are routinely developed during the
design of complex hardware systems in order to predict performance, detect
design flaws, and allow hardware/software co-design. Writing such an
executable model in ACL2 brings the additional benefit of formal analysis;
however, much care is required to construct an ACL2 model that is both fast
and analyzable. In this article, techniques are described for the
construction of high-speed formally analyzable simulators in ACL2. Their
utility is demonstrated on a simple processor model. The ACL2 scripts
referenced here provide the full details of the results described in the
article along with solutions to all the exercises in the article.
- Verification of a Simple Pipelined Machine Model, Jun Sawada, Chapter 9
of Computer-Aided Reasoning: ACL2 Case
Studies (Kaufmann, Manolios, Moore, eds.) Kluwer, 2000.
(ACL2 scripts are available from
directory 1999/pipeline/ in the community-books.)
An ACL2 model of a three-stage pipelined machine is defined,
along with a model of the corresponding sequential machine. Then a proof of
the equivalence between the two machines is presented. More importantly, the
method of decomposing the proof applies to much more complicated pipelined
architectures. The ACL2 scripts referenced here provide the full details of
the results described in the article along with solutions to all the
exercises in the article.
- Verification of Pipeline Circuits, Matt Kaufmann and David M. Russinoff, in
Proceedings of
ACL2 Workshop 2000.
- The DE Language, Warren Hunt, Jr., Chapter 10 of Computer-Aided Reasoning: ACL2 Case
Studies (Kaufmann, Manolios, Moore, eds.) Kluwer, 2000.
(ACL2 scripts are available from
directory 1999/de-hdl/ in the community-books.)
The DE language is an occurrence-oriented description language
that permits the hierarchical definition of finite-state machines in the
style of a hardware description language. The syntax and semantics of the
language are formalized and the formalization is used to prove the
correctness of a simple hardware circuit. Such formal HDLs have been used to
prove properties of much more complicated designs. The ACL2 scripts
referenced here provide the full details of the results described in the
article along with solutions to all the exercises in the article.
- Using Macros to Mimic VHDL, Dominique Borrione, Philippe Georgelin, and
Vanderlei Rodrigues, Chapter 11 of Computer-Aided Reasoning: ACL2 Case
Studies (Kaufmann, Manolios, Moore, eds.) Kluwer, 2000.
(ACL2 scripts are available from
directory 1999/vhdl/ in the community-books.)
The purpose of this project was to formalize a small
synthesizable behavioral subset of VHDL, preserving as much as possible the
syntactic flavor of VHDL and facilitating verification by symbolic simulation
and theorem proving. The ACL2 scripts referenced here provide the full
details of the results described in the article along with solutions to all
the exercises in the article.
- Efficent
Simulation of Formal Processor Models, Dave Hardin, Matt
Wilding, and Dave Greve, Rockwell Collins, Inc., Advanced Technology Center,
Cedar Rapids, IA, May, 1998. This paper describes some “hacks” by which
ACL2 array processing can be sped up to C speeds. A simple processor model,
comparable to the traditional “small machine” mentioned above, is used as
the benchmark. Native ACL2 achieves simulation speeds of about 19,000
“small machine” instructions per second when executing this model. After
modifying ACL2 as described, the model is executed at slightly over 2 million
instructions per second, comparable to a C model of the processor.
Technically, the techniques used in this paper render ACL2 unsound because
they assume (without the necessary syntactic checking) that ACL2 arrays are
used in a single-threaded way. However, the experiments done in this paper
and the techniques used are extremely illuminating. They also indicate
modifications that could be made to ACL2 to provide the efficiency needed in
industrial-scale modeling, while preserving soundness. The paper is highly
recommended.
- Transforming
the Theorem Prover into a Digital Design Tool: From Concept Car to Off-Road
Vehicle, Dave Hardin, Matt Wilding and Dave Greve, in A. J. Hu and
M. Y. Vardi (eds.) Computer Aided Verification: 10th International
Conference, CAV '98, Springer-Verlag LNCS 1427, 1998. The paper
suggests ways to integrate theorem proving into the microprocessor design
cycle. The paper was presented at CAV '98. During the talk, the authors
demonstrated an ACL2 model of the ALU of the JEM1 (a silicon Java Virtual
Machine) microprocessor, its transparent use to compute ALU results for a
C-based simulation tool for the processor and ACL2 proofs about the ALU.
This demonstration is not discussed in the paper but is indicative of the
ideas in the paper.
- Symbolic Simulation: An ACL2 Approach, J Moore,
in G. Gopalakrishnan and P. Windley (eds.)
Proceedings of the Second International Conference on Formal Methods
in Computer-Aided Design (FMCAD'98), Springer-Verlag LNCS 1522,
pp. 334-350, November, 1998.
(
ACL2 Script) This paper advocates the idea of symbolic simulation of
processor models, as a step from the familiar (namely, traditional simulation
of C models of designs) to the unfamiliar (namely, proofs about formal
models). The papers demonstrates how ACL2 can provide a symbolic simulation
capability for the “small machine” model. Some interesting performance
measures are also given.
