Microcode verification using SDVS-the method and a case study
Author: 
Beth LevyAuthors Info & Claims
Abstract
This paper describes SDVS (State Delta Verification System), its application to microcode verification, and the verification of a particular example referred to as the H-machine example. The example illustrates how particular microcode that interprets a computer instruction set can be proved correct and how this proof is accomplished with an existing, automated verification system.
References
[1]
Stephen D. Crocker, State Deltas: A Formalism for Representing Segments of Computation. PhD dissertation, University of California, Los Angeles, 1977.
[2]
Mario R. Barbacci, Gary E. Barnes, Roderic G. Cattell, and Daniel P. Siewiorek, "The ISPS Computer Description Language," CMU-CS-79-137. Carnegie-Mellon University, Computer Science Department, August 1979.
[3]
Leo Marcus and Jeff Cook, "SDVS User Manual," Tech. report ATR-84(8478)-1, The Aerospace Corporation, 1984.
[4]
L. Marcus, "Dynamic and Static Reasoning in Program Verification," Tech. report ATR-82(8478)-2, The Aerospace Corporation, June 1982.
[5]
C.A.R. Hoare, "An Axiomatic Basis for Computer Programming," Communications of the ACM, Vol. 12, No. 10, October 1969, pp. 576-580, 583.
[6]
Beth Levy, "Microcode Verification Using SDVS: The Method and a Case Study," Tech. report TR-0084(4778)-1, The Aerospace Corporation, 1984.
Index Terms
- Microcode verification using SDVS-the method and a case study
Recommendations
Microcode verification using SDVS-the method and a case study
MICRO 17: Proceedings of the 17th annual workshop on MicroprogrammingThis paper describes SDVS (State Delta Verification System), its application to microcode verification, and the verification of a particular example referred to as the H-machine example. The example illustrates how particular microcode that interprets a ...
Assertion Based Verification using Yosys: A Case Study from Nuclear Domain
ISEC '23: Proceedings of the 16th Innovations in Software Engineering ConferenceAssertion Based Verification is a design methodology that integrates Formal Methods as part of the design process. As each module is designed, the designer expresses the functional, structural and interface requirements of the module as logical formulas ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Dec. 1984
302 pages
Copyright © 1984 Author.
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 01 December 1984
Published in SIGMICRO Volume 15, Issue 4
Check for updates
Qualifiers
- Article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations6Total Citations
- 206Total Downloads
- Downloads (Last 12 months)47
- Downloads (Last 6 weeks)8
Reflects downloads up to 12 Jan 2025
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in