Browse Prior Art Database

Using Emulation to Verify Formal Architecture Descriptions

IP.com Disclosure Number: IPCOM000131417D
Original Publication Date: 1978-May-01
Included in the Prior Art Database: 2005-Nov-10
Document File: 9 page(s) / 36K

Publishing Venue

Software Patent Institute

Related People

Mario R. Barbacci: AUTHOR [+4]

Abstract

Does the reference manual actually describe the real computer? Not entirely, but the authors, starting with a simulation based on the written word, worked out the remaining errors using the machine diagnostics as the last word.

This text was extracted from a PDF file.
This is the abbreviated version, containing approximately 11% of the total text.

Page 1 of 9

THIS DOCUMENT IS AN APPROXIMATE REPRESENTATION OF THE ORIGINAL.

This record contains textual material that is copyright ©; 1978 by the Institute of Electrical and Electronics Engineers, Inc. All rights reserved. Contact the IEEE Computer Society http://www.computer.org/ (714-821-8380) for copies of the complete work that was the source of this textual material and for all use beyond that as a record from the SPI Database.

Using Emulation to Verify Formal Architecture Descriptions

Mario R. Barbacci

Carnegie-Mellon University*

Alan Parker

Naval Research Laboratory

Does the reference manual actually describe the real computer? Not entirely, but the authors, starting with a simulation based on the written word, worked out the remaining errors using the machine diagnostics as the last word.

Formal descriptions of digital systems have been used mainly for academic purposes.' A recently completed project, however, illustrates that such descriptions are highly useful in the evaluation of commercially available computer architectures. A formal description can serve as the specification of a family of architectures. Such a specification, to be of value, must accurately reflect the actual architecture. Verification of this relationship, therefore, is central to the description's usefulness as a specification. Once verified, the description can generate machine- and implementation-independent diagnostics to be used in the evaluation of any architecture claiming family membership.

The Computer Family Architecture Project2 evaluated a set of commercially available architectures in order to select a standard family of tactical military computers. Three of these architectures /IBM S/370, Interdata 8/32, and DEC PDP- 11) were selected for a detailed comparison via test programs executed under an instrumented simulator. The results of the experiment, together with an evaluation of the existing software bases, were used to select the PDP-11 as the preferred architecture.

A simulator and associated tools were used to verify the description of the selected architecture. Although the PDP- 11 is the only architecture used in this article, the method is general and can be applied to other Inot necessarily existing) computer architectures.

1

Since formal descriptions have been used mostly for academic purposes,2 the use of ISP34s in the CFA Project was, to our knowledge, the first time descriptions of real, commercially available architectures were used for evaluation and verification. Other projects show a range of applications of formal descriptions well beyond what will be described in this articled 7 A

The architecture research facility

The architecture research facility used in the CFA Project and later in the verification of the PDP-11 description is depicted in Figure 1. The ISP compiler produces code for a hypothetical machine, dubbed the "Register Transfer Machine." The "object code" produced by the compiler

1 *Currently on leave at Digital Equip...