On the verification of computer architectures using an architecture description language
Subrata Dasgupta · 1983
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 [email protected]@@@, 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 [email protected]@@@ to the formal proofs of correctness of architecture designs.