Abstract
Symbolic simulation is the simulation of the execution of a computer system on an incompletely defined, or symbolic, state. This process results in a set of expressions that define the final machine state symbolically in terms of the initial machine state. We describe our use of symbolic simulation in conjunction with the development of the JEM1, the world’s first Java processor. We demonstrate that symbolic simulation can be used to detect microcode design errors and that it can be integrated into our current design process.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Robert S. Boyer, Bernard Elspas, and Karl N. Levitt. SELECT-a formal system for testing and debugging programs by symbolic execution. Technical report, Stanford Research Institute, Menlo Park, CA, 1975. CSL-20.
James Gosling, Bill Joy, and Guy Steele. The Java Language Specification, Addison Wesley, Reading, Massachusetts, 1996.
David Greve, Matthew Wilding, and David Hardin. Efficient simulation using a simple formal processor model. Technical report, Rockwell Collins Advanced Technology Center, April 1998. available at: http://home.plutonium.net/~hokie/docs/efm.ps.
David A. Greve and Matthew M. Wilding. Stack-based Java a back-to-future step. Electronic Engineering Times, page 92, January 12, 1998.
Robert B. Jones, Carl-Johan H. Seger, and David L. Dill. Self-consistency checking. In Mandayam Srivas and Albert Camilleri, editors, Formal Methods in Computer-Aided Design-FMCAD, volume 1166 of Lecture Notes in Computer Science. Springer-Verlag, 1996.
Tim Lindholm and Frank Yellin. The Java Virtual Machine Specification. Addison Wesley, Reading, Massachusetts, 1996.
Steven P. Miller, David A. Greve, Matthew M. Wilding, and Mandayam Srivas. Formal verification of the AAMP-FV microcode. Technical report, Rockwell Collins, Inc., Cedar Rapids, IA, 1996.
Steven P. Miller and Mandayam Srivas. Formal verification of the AAMP5 microprocessor: A case study in the industrial use of formal methods. In WIFT’95: Workshop on Industrial-Strength Formal Specification Techniques, Boca Raton, FL, 1995. IEEE Computer Society.
S. Owre, N. Shankar, and J.M. Rushby. The PVS Specification Language (Beta Release). Computer Science Laboratory, SRI International, Menlo Park, CA, February 1993.
S. Owre, N. Shankar, and J. M. Rushby. User Guide for the PVS Specification and Verification System (Beta Release). Computer Science Laboratory, SRI International, Menlo Park, CA, February 1993.
N. Shankar, S. Owre, and J. M. Rushby. The PVS Proof Checker: A Reference Manual (Beta Release). Computer Science Laboratory, SRI International, Menlo Park, CA, February 1993.
Matthew M. Wilding. Robust computer system proofs in PVS. In C. Michael Holloway and Kelly J. Hayhurst, editors, LFM97: Fourth NASA Langley Formal Methods Workshop. NASA Conference Publication no. 3356, 1997. http://atb-www.larc.nasa.gov/Lfm97/.
Alexander Wolfe. First Java-specific MPU rolls. Electronic Engineering Times, page 1, September 22, 1997.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Greve, D.A. (1998). Symbolic Simulation of the JEM1 Microprocessor. In: Gopalakrishnan, G., Windley, P. (eds) Formal Methods in Computer-Aided Design. FMCAD 1998. Lecture Notes in Computer Science, vol 1522. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-49519-3_21
Download citation
DOI: https://doi.org/10.1007/3-540-49519-3_21
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-65191-8
Online ISBN: 978-3-540-49519-2
eBook Packages: Springer Book Archive