article

Free access

SDVS: A system for verifying microcode correctness

Authors:

Leo Marcus,

Stephen D. Crocker,

Jaisook R. LandauerAuthors Info & Claims

ACM SIGMICRO Newsletter, Volume 15, Issue 4

Pages 246 - 255

https://doi.org/10.1145/384281.808233

Published: 01 December 1984 Publication History

PDF eReader

Abstract

This paper is a progress report on an experimental system, the state delta verification system (SDVS), for verifying microcode correctness. The goal of this project is to solve some of the problems, both theoretical and engineering, obstructing the realization of a usable and applicable program for checking proofs of microcode correctness. The ideal result would be a system that could be naturally incorporated into the specification-implementation cycle of, for example, microcoded machine instruction sets.

References

[1]

Leo Marcus and Jeff Cook, "SDVS User Manual," Tech. report ATR-84(8478)-1, The Aerospace Corporation, 1984.

Google Scholar

[2]

Leo Marcus, "Goals for SDVS: a usable proof checker for proofs of program correctness," Tech. report ATR-83(8478)-5, The Aerospace Corporation, 1984.

Google Scholar

[3]

Stephen D. Crocker, State Deltas: A Formalism for Representing Segments of Computation, PhD dissertation, University of California, Los Angeles, 1977.

Digital Library

Google Scholar

[4]

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.

Google Scholar

[5]

William T. Overman, "Verification of Concurrent Systems: Function and Timing." Tech. report CSD-810184, UCLA, August 1981.

Google Scholar

[6]

Eve Cohen, "ISPS for SDVS," Tech. report ATR-84(8478)-2, The Aerospace Corporation, 1984.

Google Scholar

[7]

Greg Nelson and Derek C. Oppen, "Fast Decision Procedures Based on Congruence Closure," Journal of the Association for Computing Machinery, Vol. 27, No. 2, April 1980,.

Digital Library

Google Scholar

[8]

Greg Nelson and Derek C. Oppen, "Simplification by cooperating decision procedures," ACM Transactions on Programming Languages and Systems, Vol. 1, No. 2, October 1979,.

Digital Library

Google Scholar

[9]

Martin Davis, "Hilbert's Tenth Problem is Unsolvable," American Mathematical Monthly, Vol. 80, No. 3, March 1973, pp. 233-269.

Crossref

Google Scholar

[10]

Leo Marcus, "Implementation Mapping between Programs," Tech. report ATR-84(8478)-3, The Aerospace Corporation, 1984.

Google Scholar

[11]

Beth Levy, "Microcode Verification Using SDVS—The Method and a Case Study," Tech. report ATM-83(3920-03)-2, The Aerospace Corporation, 1983.

Google Scholar

Cited By

View all

von Henke F(1991)Entwicklungstendenzen bei formalen Methoden im Bereich der ComputersicherheitSicherheitsaspekte in der Informationstechnik10.1007/978-3-322-83911-4_10(144-162)Online publication date: 1991
https://doi.org/10.1007/978-3-322-83911-4_10
Damm W(1988)A Microprogramming LogicIEEE Transactions on Software Engineering10.1109/32.613414:5(559-574)Online publication date: 1-May-1988
https://dl.acm.org/doi/10.1109/32.6134
Damm W(1988)A Microprogramming LogicIEEE Transactions on Software Engineering10.1109/32.613414:5(559-574)Online publication date: 1-May-1988
https://dl.acm.org/doi/10.1109/32.6134
Show More Cited By

Index Terms

Recommendations

SDVS: A system for verifying microcode correctness
MICRO 17: Proceedings of the 17th annual workshop on Microprogramming

This paper is a progress report on an experimental system, the state delta verification system (SDVS), for verifying microcode correctness. The goal of this project is to solve some of the problems, both theoretical and engineering, obstructing the ...
Microcode verification using SDVS-the method and a case study
MICRO 17: Proceedings of the Seventeenth Annual Microprogramming Workshop

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 ...
Microcode verification using SDVS-the method and a case study
MICRO 17: Proceedings of the 17th annual workshop on Microprogramming

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 ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

ACM SIGMICRO Newsletter Volume 15, Issue 4

MICRO 17: Proceedings of the Seventeenth Annual Microprogramming Workshop

Dec. 1984

302 pages

ISSN:1050-916X

DOI:10.1145/384281

Issue’s Table of Contents

MICRO 17: Proceedings of the 17th annual workshop on Microprogramming
December 1984
325 pages
Chairmen:
M. Carter,
R. A. Mueller

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

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

7
Total Citations
View Citations
181
Total Downloads

Downloads (Last 12 months)43
Downloads (Last 6 weeks)3

Reflects downloads up to 12 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

von Henke F(1991)Entwicklungstendenzen bei formalen Methoden im Bereich der ComputersicherheitSicherheitsaspekte in der Informationstechnik10.1007/978-3-322-83911-4_10(144-162)Online publication date: 1991
https://doi.org/10.1007/978-3-322-83911-4_10
Damm W(1988)A Microprogramming LogicIEEE Transactions on Software Engineering10.1109/32.613414:5(559-574)Online publication date: 1-May-1988
https://dl.acm.org/doi/10.1109/32.6134
Damm W(1988)A Microprogramming LogicIEEE Transactions on Software Engineering10.1109/32.613414:5(559-574)Online publication date: 1-May-1988
https://dl.acm.org/doi/10.1109/32.6134
Vegdahl SBelgard R(1985)The design of an interactive compiler for optimizing microprogramsProceedings of the 18th annual workshop on Microprogramming10.1145/18927.18919(129-136)Online publication date: 1-Dec-1985
https://dl.acm.org/doi/10.1145/18927.18919
Damm WDohmen GBelgard R(1985)Verification of microprogrammed computer architectures in the S*-system: a case studyProceedings of the 18th annual workshop on Microprogramming10.1145/18927.18913(61-73)Online publication date: 1-Dec-1985
https://dl.acm.org/doi/10.1145/18927.18913
Vegdahl S(1985)The design of an interactive compiler for optimizing microprogramsACM SIGMICRO Newsletter10.1145/18906.1891916:4(129-136)Online publication date: 1-Dec-1985
https://dl.acm.org/doi/10.1145/18906.18919
Damm WDohmen G(1985)Verification of microprogrammed computer architectures in the S*-system: a case studyACM SIGMICRO Newsletter10.1145/18906.1891316:4(61-73)Online publication date: 1-Dec-1985
https://dl.acm.org/doi/10.1145/18906.18913

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Abstract

References

Cited By

Index Terms

Recommendations