A Formal Definition of AMDL
Original Publication Date: 1979-Dec-31
Included in the Prior Art Database: 2005-Sep-16
Software Patent Institute
Peter W. Alfvin: AUTHOR [+2]
Since the introduction of ISP [Bell & Newell, 1971], the use of hardware description languages (HDLs) has increased dramatically. Used originally to describe at the programming level the instruction sets of digital computers, hardware descriptions are now being used in applications such as design automation, emulation, compiler generation, and program verification - to name only a few. This surge of activity has put the existing HDLs to a thorough test, with each application area making its own set of demands on the languages. One common demand, however, is for a precise definition of the HDI_s themselves. Before we discuss this problem of defining a hardware description language, let us look at a very small but very common example of its use. Consider a "push" instruction on a typical computer of the form PUSH reg, address. A prose description of this instruction might read: "The PUSH instruction increments the register reg and moves the contents of the word pointed to by address to the word pointed to by the new value of reg." While this definition might seem straightforward, there are a great number of possible difficulties. What if the registers were addressable memory locations and address points to reg? Is the original value or the incremented value of reg stored at reg + 1? Although it would be highly unlikely, what if the instruction PUSH reg, address were being executed out of reg? Would the instruction first be moved to an internal register, or would the address field of the instruction be modified during execution resulting in a reference to address + l? And what if reg pointed to reg - 1? Would the final value of reg be the contents of address plus one or simply the incremented contents of reg? There are,of course,other clarifications that might need to be made concerning what constitutes a legal address, how overflow conditions are handled, and other such matters. One could argue that such relatively minor details are not worth considering, for one should not be writing programs that depend on the machine's behavior in these unusual circumstances. This is a difficult argument in that it assumes that there could be an agreement upon what constitutes "unusual circumstances." One could also argue that there is nothing wrong with prose descriptions, and that this description simply needs to be expanded. While it is certainly true that the description could be more carefully worded, it is arguable that true precision could be obtained using this approach. Furthermore, there is no mechanism in English (or any natural language) which ensures that a definition is complete. It is sometimes not a simple matter to determine whether a prose definition has enumerated all possible situations. Finally, this kind of description is worthless to an application program requiring a computer description. If we are to reap the benefits of software such as compiler-compilers and general program verification systems,
THIS DOCUMENT IS AN APPROXIMATE REPRESENTATION OF THE ORIGINAL.
A Formal Definition of AMDL
Peter W. Alfvin
ISIIRR-79-78 October 1979 INFORMATION SCIENCES INSTITUTE
4676 Admiralty 1~aylMarinadel ReylCalifornia 90291 UNIVERSITY OF SOUTHERN CALIFORNIA ITT (213) 822-1511 This research was supported by the Rome Air Development Center under contracts f30602-78-C-o08 and t)AHC15-72-C-0308. Views and conclusions contained in this paper are the author's and should not be interpreted as representing the official opinion or policy of 11ADC, the U.S. Government a any person or agency connected with them.
First, I would like to thank my thesis adviser, David Martin, for his continued support during the preparation of this report. He introduced me to the subject of formal semantics, provided valuable guidance while I was formulating my ideas, and carefully reviewed the thesis in its final stages. He performed each of these tasks with a diligence, patience and spirit that made working with him an enjoyable and rewarding experience.
UCLA faculty members Emily Friedman and Milos Ercegovac completed the thesis committee and I am grateful for their participation.
'Ibis report was prepared while 1 was a staff member at the Information Sciences Institute of the University of Southern California. Steve Crocker, under whom I worked, deserves special thanks for providing the opportunity and the encouragement to pursue my thesis topic. Discussions with Steve and other 1SI members Leo Marcus and Dono VanMierop were also helpful.
This work was supported in part by the Rome Air Development Center under contracts F30602- 78-C-008 and DAHC15-72-C-0308. The views expressed here are those of the author and not necessarily those of the U.S. Government.
T1ie thesis was prepared using the substantial resources of ISI and Xerox, whose contribution I acknowledge.
AMDL is an abstract form of the hardware description language ISPS. This report presents a formal definition of AMDL, using the techniques of denotational semantics as developed by Scott and Strachey. AMDL includes some nonstandard control and data structures which are easily handled by this definitional method. This report assumes familiarity with descriptive denotational semantics.
AMDL is an abstract form of the hardware description language ISPS. This report presents a formal definition of AMDL, using the techniques of denotational semantics as developed by Scott and Strachey. AMDL includes some nonstandard control and data structures which are
University of Southern California Page 1 Dec 31, 1979
A Formal Definition of AMDL
easily handled by this definitional method. This report assumes familiarity with descriptive denotational semantics.
1, 0 Introduction
Since the introduction of ISP [Bell & Newell, 1971], the use of hardware description languages (HDLs) has increased dramatically. Used originally to describe at the programming level the instruction sets of di...