Abstract
Executable formal specification can allow engineers to test (or simulate) the specified system on concrete data before the system is implemented. This is beginning to gain acceptance and is just the formal analogue of the standard practice of building simulators in conventional programming languages such as C. A largely unexplored but potentially very useful next step is symbolic simulation, the “execution” of the formal specification on indeterminant data. With the right interface, this need not require much additional training of the engineers using the tool. It allows many tests to be collapsed into one. Furthermore, it familiarizes the working engineer with the abstractions and notation used in the design, thus allowing team members to speak clearly to one another. We illustrate these ideas with a formal specification of a simple computing machine in ACL2. We sketch some requirements on the interface, which we call a symbolic spreadsheet.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
W. R. Bevier, W. A. Hunt, J. S. Moore and W. D. Young. Special Issue on System Verification Journal of Automated Reasoning 5(4), 1989.
R. S. Boyer and J S. Moore, Proving Theorems about Pure LISP Fucntions, JACM, 22(1), pp. 129–144, 1975.
R. S. Boyer, K. N. Levitt and B. Elspas, SELECT-A Formal System for Testing and Debugging Programs, Proceedings of the International Conference on Reliable Software, IEEE Catalogue Number 75CHO940-7CSR, pp. 234–245, 1975.
R. S. Boyer and J. S. Moore. Mechanized Formal Reasoning about Programs and Computing Machines. In R. Veroff (ed.), Automated Reasoning and Its Applications: Essays in Honor of Larry Wos, MIT Press, 1996.
R. S. Boyer and J. S. Moore. A Computational Logic Handbook, Second Edition. Academic Press, London, 1997.
B. Brock, M. Kaufmann, and J. S. Moore. ACL2 Theorems about Commercial Microprocessors. In Proceedings of Formal Methods in Computer-Aided Design (FMCAD’96), M. Srivas and A. Camilleri (eds.), Springer-Verlag, November, 1996, pp. 275–293.
J. Crow, S. Owre, J. Rushby, N. Shankar, and M. Srivas. A Tutorial Introduction to PVS, presented at Workshop on Industrial-Strength Formal Specification Techniques, Boca Raton, FL, April 1995 (see http://www.csl.sri.com/pvs.html).
S. Gilfeather, J. Gehman, and C. Harrison. Architecture of a Complex Arithmetic Processor for Communication Signal Processing in SPIE Proceedings, International Symposium on Optics, Imaging, and Instrumentation, 2296 Advanced Signal Processing: Algorithms, Architectures, and Implementations V, July, 1994, pp. 624–625.
D. A. Greve, Symbolic Simulation of the JEM1 Microprocessor, Technical Report, Advanced Technology Center, Rockwell Collins Avionics and Communications, Cedar Rapids, IA 52498, April, 1998 (also appearing in this volume, The Proceedings of FMCAD’ 98.
D. A. Greve, D. S. Hardin and M. M. Wilding, Efficient Simulation Using a Simple Formal Processor Model, Technical Report, Advanced Technology Center, Rockwell Collins Avionics and Communications, Cedar Rapids, IA 52498, April, 1998.
D. A. Greve and M. M. Wilding Stack-based Java a back-to-future step, Electronic Engineering Times, Jan. 12, 1998, pp. 92.
D. S. Hardin, M. M. Wilding, and D. A. Greve, Transforming the Theorem Prover into a Digital Design Tool: From Concept Car to Off-Road Vehicle, in A. J. Hu and M. Y. Vardi (eds.) Computed Aided Verification: 10th International Conference, CAV’ 98, Springer-Verlag LNCS 1427, pp. 39–44, 1998.
M. Kaufmann. ACL2 Support for Verification Projects. In 15th International Conference on Automated Deduction (CADE) (to appear, 1998).
M. Kaufmann and J. S. Moore. An Industrial Strength Theorem Prover for a Logic Based on Common Lisp. In IEEE Transactions on Software Engineering 23(4), April, 1997, pp. 203–213.
J. S. Moore, Computational Logic: Structure Sharing and Proof of Program Properties, Ph. D. dissertation, University of Edinburgh, Scotland, 1973.
D. M. Russinoff. A Mechanically Checked Proof of IEEE Compliance of the Floating Point Multiplication, Division, and Square Root Algorithms of the AMD-K7ℳ Processor URL http://www.onr.com/user/russ/david/k7-div-sqrt.html.
A. Wolfe. First Java-specific MPU Rolls Electronic Engineering Times, Sept 22, 1997, pp. 1.
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
Strother Moore, J. (1998). Symbolic Simulation: An ACL2 Approach. 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_22
Download citation
DOI: https://doi.org/10.1007/3-540-49519-3_22
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