article

Free access

On the verification of computer architectures using an architecture description language

Author:

Subrata DasguptaAuthors Info & Claims

ACM SIGARCH Computer Architecture News, Volume 11, Issue 3

Pages 32 - 38

https://doi.org/10.1145/1067651.801635

Published: 13 June 1983 Publication History

Abstract

In a previous paper [8], we had presented the notion of a family of languages for the multilevel design and description of computer architectures. Details of a particular language family, currently under development, was also described. One of the constituent members of this family is S@@@@, intended for the specifications of the outer (or exo-) and inner (or endo-) architectures of general purpose von Neumann style computers. In this paper we describe the formalization and application of S@@@@ to the formal proofs of correctness of architecture designs.

References

[1]

Alagic, S., and Arbib, M.A., The Design of Well Structured and Correct Programs, Springer Verlag, N.Y., 1978.]]

Digital Library

[2]

Baer, J-L., Computer Systems Architecture, Computer Science Press, Potomac, MD, 1980.]]

[3]

Barbacci, M.R., "A Comparison of register transfer languages for describing computers and digital systems," IEEE Trans. Comput., C-24, 2, 1975.]]

[4]

Barbacci, M.R., and Parker, A., "Using emulation to verify formal architecture descriptions," Computer, May 1978, pp. 51-56.]]

Digital Library

[5]

Barbacci, M.R., Barnes, G.E., Cattell, R.G., and Siewiorek, D.P., "The ISPS Computer description language," Dept. of Computer Science, Carnegie-Mellon Univ., Pittsburgh, PA., 1978.]]

[6]

Bell, C.G., and Newell, A., Computer Structures: Readings and Examples, McGraw-Hill, N.Y., 1971.]]

Digital Library

[7]

Dasgupta, S., "S@@@@: A language for describing computer architectures," in Computer Hardware Description Languages and Their Applications, M.A. Breuer & R. Hartenstein (Ed.), North-Holland, Amsterdam 1981, pp. 65-78.]]

[8]

Dasgupta, S., and Olafsson, M., "Towards a family of languages for the design and implementation of machine architectures," Proc. 9th Annual Symposium on Computer Architecture, IEEE Computer Society Press, 1982.]]

Digital Library

[9]

Dasgupta, S., "Computer Design and Description Languages" in Advances in Computers, M. Yovits (Editor), Vol. 21, Academic Press, 1982.]]

[10]

Dasgupta, S., The Design and Description of Computer Architectures, John Wiley & Sons (Wiley-Interscience), Forthcoming, 1983.]]

Digital Library

[11]

Dietmeyer, D.L., and Duley, J.R., "Register transfer languages and their translation" in Digital Systems Design Automation, M.A. Breuer (Ed.), Computer Science Press, 1975.]]

[12]

Fuller, S.H., Stone, H.S., Burr, W.E., "Initial selection and screening of the CFA candidate computer architectures," Proc. Natl. Comput. Conf., 1977, Vol. 46]]

[13]

Hoare, C.A.R., "An axiomatic basis for computer programming," Comm. ACM, 12, 10, 1974, pp. 549-557.]]

Digital Library

[14]

Hoare, C.A.R., "Notes on Data Structuring," in O-J Dahl, E.W. Dijkstra, & C.A.R. Hoare, Structured Programming, Academic Press, N.Y., 1972.]]

Digital Library

[15]

Jones, J.C., Design Methods: Seeds of Human Future, John Wiley & Sons, London, 1970.]]

[16]

Leung, C.K.C., "ADL: An Architecture Description Language for Packet Communication Systems," Proc. 4th Int. Symp. on Computer Hardware Description Languages, Palo Alto, CA, 1979.]]

[17]

Myers, G.J., Advances in Computer Architecture, John Wiley and Sons (Wiley-Interscience), N.Y., 1981, (2nd Edition).]]

Digital Library

[18]

Owicki, S., and Gries, D.G., "An axiomatic proof technique for parallel programs," Acta Informatica, 6, 1976, pp. 319-340.]]

Digital Library

[19]

Parker, A.C., and Wallace, J.J., "An I/O Hardware Description Language," IEEE Trans. Comput., C-30, 6, June 1981, pp. 423-428.]]

Digital Library

[20]

Patterson, D.A., "STRUM: structured programming system for correct firmware," IEEE Trans. Comput., C-25, 10, Oct. 1976, pp. 974-985.]]

Digital Library

Cited By

Nixon JSchach SWinner RHabib S(1986)A microarchitecture description language for retargeting firmware toolsProceedings of the 19th annual workshop on Microprogramming10.1145/19551.19535(34-43)Online publication date: 1-Dec-1986
https://dl.acm.org/doi/10.1145/19551.19535
Nixon JSchach SWinner R(1986)A microarchitecture description language for retargeting firmware toolsACM SIGMICRO Newsletter10.1145/19530.1953517:4(34-43)Online publication date: 1-Dec-1986
https://dl.acm.org/doi/10.1145/19530.19535
Nixon JSchach SWinner RHabib S(1986)A microarchitecture description language for retargeting firmware toolsProceedings of the 19th annual workshop on Microprogramming10.1145/19551.19535(34-43)Online publication date: 1-Dec-1986
https://dl.acm.org/doi/10.1145/19551.19535
Show More Cited By

Index Terms

On the verification of computer architectures using an architecture description language

Recommendations

On the verification of computer architectures using an architecture description language
ISCA '83: Proceedings of the 10th annual international symposium on Computer architecture

In a previous paper [8], we had presented the notion of a family of languages for the multilevel design and description of computer architectures. Details of a particular language family, currently under development, was also described. One of the ...
Teaching computer architecture using an architecture description language
WCAE '04: Proceedings of the 2004 workshop on Computer architecture education: held in conjunction with the 31st International Symposium on Computer Architecture

This paper presents the use of the ArchC Architecture Description Language (ADL) as a support tool for computer architecture courses. ArchC enables students to perform several experiments using its automatically generated SystemC simulators, covering ...
Domains of concern in software architectures and architecture description languages
DSL'97: Proceedings of the Conference on Domain-Specific Languages on Conference on Domain-Specific Languages (DSL), 1997

Software architectures shift the focus of developers from lines-of-code to coarser-grained elements and their interconnection structure. Architecture description languages (ADLs) have been proposed as domain-specific languages for the domain of software ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGARCH Computer Architecture News

ACM SIGARCH Computer Architecture News Volume 11, Issue 3

June 1983

413 pages

ISSN:0163-5964

DOI:10.1145/1067651

Issue’s Table of Contents

ISCA '83: Proceedings of the 10th annual international symposium on Computer architecture
June 1983
424 pages
ISBN:0897911016
DOI:10.1145/800046
Chairmen:
Harold W. Lawson,
Tilak Agerwala,
Hans H. Heilborn,
Hideo Aiso,
Lars-Erik Thorelli,
Jean Loup Baer,
Mario Tokoro

Copyright © 1983 Author.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 13 June 1983

Published in SIGARCH Volume 11, Issue 3

Check for updates

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

6
Total Citations
View Citations
332
Total Downloads

Downloads (Last 12 months)71
Downloads (Last 6 weeks)4

Reflects downloads up to 14 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Nixon JSchach SWinner RHabib S(1986)A microarchitecture description language for retargeting firmware toolsProceedings of the 19th annual workshop on Microprogramming10.1145/19551.19535(34-43)Online publication date: 1-Dec-1986
https://dl.acm.org/doi/10.1145/19551.19535
Nixon JSchach SWinner R(1986)A microarchitecture description language for retargeting firmware toolsACM SIGMICRO Newsletter10.1145/19530.1953517:4(34-43)Online publication date: 1-Dec-1986
https://dl.acm.org/doi/10.1145/19530.19535
Nixon JSchach SWinner RHabib S(1986)A microarchitecture description language for retargeting firmware toolsProceedings of the 19th annual workshop on Microprogramming10.1145/19551.19535(34-43)Online publication date: 1-Dec-1986
https://dl.acm.org/doi/10.1145/19551.19535
Nixon JSchach SWinner R(1986)A microarchitecture description language for retargeting firmware toolsACM SIGMICRO Newsletter10.1145/19530.1953517:4(34-43)Online publication date: 1-Dec-1986
https://dl.acm.org/doi/10.1145/19530.19535
Drongowski PWalker TDominick W(1985)Representation in CADProceedings of the 1985 ACM thirteenth annual conference on Computer Science10.1145/320599.320664(131-135)Online publication date: 1-Mar-1985
https://dl.acm.org/doi/10.1145/320599.320664
Dasgupta SWagner A(1984)The use of hoare logic in the verification of horizontal microprogramsInternational Journal of Computer & Information Sciences10.1007/BF0098582313:6(461-490)Online publication date: Dec-1984
https://doi.org/10.1007/BF00985823

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

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

Full Access

Get this Publication

Media

Figures

Other

Tables

View Issue’s Table of Contents