\begin{thebibliography}{99}

\bibitem{Armstrong}
James R. Armstrong,
Chip-Level Modelling with VHDL,
Prentice-Hall,
Englewood Cliffs, N.J.,
1989.

\bibitem{Anceau}
F. Anceau,
The Architecture of Microprocessors,
Addison-Wesley Publishing Company, Wokingham, 1986.

\bibitem{Barrow}
H. Barrow,
VERIFY:  A Program for Proving Correctness of Digital Hardware Designs,
Artificial Intelligence, Vol. 24, No. 1-3,
December 1984,
pp. 437-491.

\bibitem{Bevier87}
William R. Bevier, Warren A. Hunt, Jr., and William D. Young, in:
Towards Verified Execution Environments, in:
Procs. of the 1987 IEEE Symposium on Security and Privacy,
27-29 April 1987, Oakland, California
Computer Society Press, Washington, D.C., 1987
pp. 106-115.
Also Report No. 5, Computational Logic, Inc.,
Austin, Texas,
February 1987.

\bibitem{Bevier89}
W. Bevier, W. Hunt, J Moore, and W. Young,
An Approach to Systems Verification,
Journal of Automated Reasoning,
Vol. 5, No. 4, November 1989.

\bibitem{Bochman}
G. Bochman,
Hardware Specification with Temporal Logic,
IEEE Transactions on Computers,
Vol. C-31, No. 3,
March 1982,
pp. 223-231.

\bibitem{Bryant:thesis}
Randy Everitt Bryant,
A Switch-Level Simulation Model for Integrated Logic Circuits,
Ph.D. Thesis,
Dept. of Electrical Engineering and Computer Science,
Report No. MIT/LCS/TR-259,
Laboratory for Computer Science,
Massachusetts Institute of Technology,
March 1981.

\bibitem{Camilleri:thesis}
Albert John Camilleri,
Executing Behavioural Definitions in Higher Order Logic,
Ph.D. Thesis,
Report No. 140,
Computer Laboratory, Cambridge University,
February 1988.

\bibitem{Camilleri:pisa}
Albert John Camilleri,
Simulation as an Aid to Verification Using the HOL Theorem Prover, in:
D. Edwards, ed.,
Procs. of the IFIP TC10 Working Conf. on
Design Methodology in VLSI and Computer Architecture,
Pisa, Italy, 19-21 September 1988,
North-Holland, Amsterdam, 1989,
pp. 147-168.
Also Report No. 150,
Computer Laboratory, Cambridge University,
October 1988.

\bibitem{Camilleri:csp}
Albert John Camilleri,
Mechanizing CSP Trace Theory in Higher Order Logic,
(in preparation),
Hewlett-Packard Laboratories,
Bristol, England,
1989.

\bibitem{Camurati}
Paolo Camurati and Paolo Prinetto,
Formal Verification of Hardware Correctness,
IEEE Computer, Vol. 21, No. 7, July 1988,
pp. 8-19.

\bibitem{Cohn:calgary86}
Avra Cohn,
A Proof of Correctness of the Viper Microprocessor:  The First Level, in:
G. Birtwistle and P. Subrahmanyam, eds.,
VLSI Specification, Verification and Synthesis,
Kluwer Academic Publishers, Boston, 1988,
pp. 27-71.
Also Report No. 104, Computer Laboratory, Cambridge University,
January 1987.

\bibitem{Cohn:banff87}
Avra Cohn,
Correctness Properties of the Viper Block Model:  The Second Level, in:
G. Birtwistle and P. Subrahmanyam, eds.,
Current Trends in Hardware Verification and Automated Theorem Proving,
Springer-Verlag, New York, 1989,
pp. 1-91.
Also Report No. 134, Computer Laboratory, Cambridge University,
May 1988. 

\bibitem{Cohn:jar}
Avra Cohn,
The Notion of Proof in Hardware Verification,
Journal of Automated Reasoning,
Vol. 5,
May 1989,
pp. 127-139.

\bibitem{Cullyer:lncs331}
W.J. Cullyer,
High Integrity Computing, in:
M. Joseph, ed.,
Formal Techniques in Real-Time and Fault-Tolerant Systems,
Lecture Notes in Computer Science, No. 331,
Springer-Verlag, Berlin, 1988.
pp. 1-35.

\bibitem{Curzon:thesis}
Paul Curzon,
Ph.D. Thesis,
(in preparation),
Computer Laboratory,
Cambridge University,
1989.

\bibitem{Davie:thesis}
Bruce S. Davie,
A Formal, Hierarchical Design and Validation Methodology for VLSI,
Ph.D. Thesis,
Report CST-55-88,
Dept. of Computer Science,
University of Edinburgh,
October 1988.

\bibitem{Dhingra:thesis}
Inderpreet S. Dhingra,
Formalising an Integrated Circuit Design Style in Higher-Order Logic,
Ph.D. Thesis,
Report No. 151,
Computer Laboratory,
Cambridge University,
1989.

\bibitem{Clarke}
D. Dill and E. Clarke,
Automatic Verification of Asynchronous Circuits using
Temporal Logic,
IEE Procs., Vol. 133, Pt. E, No. 5,
September 1986,
pp. 276-282.

\bibitem{Eveking}
H. Eveking,
Formal Verification of Synchronous Systems, in:
G. Milne and P. Subrahmanyam, eds.,
Formal Aspects of VLSI Design,
Procs. of the 1985 Edinburgh Conference on VLSI,
North-Holland, Amsterdam, 1986,
pp. 137-152.

\bibitem{Eveking:glasgow}
H. Eveking,
How to Design Correct Hardware and Know It.
G. Milne, ed.,
The Fusion of Hardware Design and Verification,
Procs. of the IFIP WG 10.2 Intl. Working Conf.,
Glasgow, Scotland, 3-6 July 1988,
North-Holland, Amsterdam, 1988,
pp. 250-262.

\bibitem{Fujita}
M. Fujita, H. Tanaka and T. Moto-oka.,
Temporal Logic Based Hardware Description
and Its Verification with Prolog,
New Generation Computing, No. 1,
1983,
pp. 195-203.

\bibitem{Gordon81}
M. Gordon,
A Model of Register Transfer Systems with Applications to Microcode
and VLSI Correctness,
Internal Report CSR-82-81,
Department of Computer Science,
University of Edinburgh,
1981.

\bibitem{Gordon:tech41}
M. Gordon,
LCF\_LSM,
Report No. 41, Computer Laboratory, Cambridge University,
1983.

\bibitem{Gordon:tech42}
M. Gordon,
Proving a
Computer Correct using the LCF\_LSM Hardware Verification System,
Report No. 42, Computer Laboratory, Cambridge University,
1983.

\bibitem{Gordon:banff87}
Michael J. C. Gordon,
Mechanizing Programming Logics in Higher Order Logic, in:
G. Birtwistle and P. Subrahmanyam, eds.,
Current Trends in Hardware Verification and Automated Theorem Proving,
Springer-Verlag, New York, 1989,
pp. 387-439.
Also Report No. 145, Computer Laboratory, Cambridge University,
September 1988.

\bibitem{Hale:thesis}
Roger W. S. Hale,
Programming in Temporal Logic,
Ph.D. Thesis,
Report No. 173, Computer Laboratory, Cambridge University,
July 1989.

\bibitem{Herbert:thesis}
John M. J. Herbert,
Application of Formal Methods to Digital System Design,
Ph.D. Thesis,
Computer Laboratory,
Cambridge University,
1986.

\bibitem{Herbert:glasgow88}
John Herbert,
Temporal Abstraction of Digital Designs,
G. Milne, ed.,
The Fusion of Hardware Design and Verification,
Procs. of the IFIP WG 10.2 Intl. Working Conf.,
Glasgow, Scotland, 3-6 July 1988,
North-Holland, Amsterdam, 1988,
pp. 1-25.

\bibitem{Hunt:thesis}
Warren A. Hunt,
FM8501, A Verified Microprocessor,
Ph.D. Thesis,
Report No. 47,
Institute for Computing Science, University of Texas, Austin,
December 1985.

\bibitem{Joyce:tech100}
Joyce, J., G. Birtwistle and M. Gordon,
Proving a Computer Correct in Higher Order Logic,
Report No. 100, Computer Laboratory,
Cambridge University,
1986.

\bibitem{Joyce:calgary86}
Jeffrey J. Joyce,
Formal Verification and Implementation of a Microprocessor, in:
G. Birtwistle and P. Subrahmanyam, eds.,
VLSI Specification, Verification and Synthesis,
Procs. of a Workshop,
12-16 January 1987,
Kluwer Academic Publishers, Boston, 1988,
pp. 129-157.

\bibitem{Joyce:firstyear}
Jeffrey J. Joyce,
Multi-Level Verification of a Simple Microprocessor,
First Year Ph.D. Progress Report and Research Proposal,
Computer Laboratory,
Cambridge University,
December 1987.

\bibitem{Joyce:glasgow}
Jeffrey J. Joyce,
Generic Structures in the Formal Specification and
Verification of Digital Circuits, in:
G. Milne, ed.,
The Fusion of Hardware Design and Verification,
Procs. of the IFIP WG 10.2 Intl. Working Conf.,
Glasgow, Scotland, 3-6 July 1988,
North-Holland, Amsterdam, 1988,
pp. 50-74.

\bibitem{Joyce:stirling}
Jeffery J. Joyce,
Formal Specification and Verification of Asynchronous Processes
in Higher-Order Logic, in:
C. Rattray, ed.,
BCS-FACS Workshop on Specification and Verification of Concurrent Processes,
Stirling, Scotland, 6-8 July 1988,
(to be published by Springer Verlag).
Also Report No. 136, Computer Laboratory, Cambridge University,
June 1988.

\bibitem{Joyce:pisa}
Jeffery J. Joyce,
Using Higher-Order Logic to Specify Computer Hardware and Architecture, in:
D. Edwards, ed.,
Design Methodologies for VLSI and Computer Architecture,
Procs. of the IFIP TC10 Working Conf. on
Design Methodology in VLSI and Computer Architecture,
Pisa, Italy, 19-21 September 1988,
North-Holland, Amsterdam, 1989,
pp. 129-146.

\bibitem{Joyce:tech167}
Jeffrey J. Joyce,
A Verified Compiler for a Verified Microprocessor,
Report No. 167, Computer Laboratory, Cambridge University,
March 1989.

\bibitem{Joyce:cornell}
Jeffrey J. Joyce,
Totally Verified Systems: Linking Verified Software to Verified Hardware, in:
M. Leeser and G. Brown, eds.,
Specification, Verification and Synthesis:
Mathematical Aspects,
Procs. of a Workshop, 5-7 July 1989,
Ithaca, N.Y.,
Springer-Verlag,
1989.
Also Report No. 178, Computer Laboratory, Cambridge University,
September 1989.

\bibitem{Joyce:vlsi89}
Jeffrey J. Joyce,
Formal Specification and Verification of Synthesized MOS Structures, in:
G. Musgrave and U. Lauther, eds.,
VLSI 89,
Procs. of the IFIP TC10/WG 10.5 Intl. Conf. on Very Large Scale Integration,
Munich, Germany, 16-18 August 1989,
(to be published by Elsevier Science Publishers).

\bibitem{Joyce:integration}
Jeffrey J. Joyce,
Formal Specification and Verification of Microprocessor Systems,
Integration, the VLSI journal, Vol. 7,
September 1989,
pp. 247-266.

\bibitem{Joyce:thesis}
Jeffrey J. Joyce,
Ph.D. Thesis,
(in preparation),
Computer Laboratory, Cambridge University,
1989.

\bibitem{SRI}
J. Joyce, E. Liu, J. Rushby, N. Shankar, R. Suaya, F. von Henke:
From Hardware Verification to Silicon Compilation,
(in preparation)
SRI International, Menlo Park,
1990.

\bibitem{Leeser:thesis}
Miriam E. Leeser.
Reasoning about the Function and Timing of Integrated Circuits
with Prolog and Temporal Logic,
Ph.D. Thesis, Computer Laboratory,
Report No. 132, Computer Laboratory, Cambridge University,
April 1988.

\bibitem{Loewenstein:cornell}
Paul Loewenstein,
Reasoning about State Machines in Higher-Order Logic, in:
M. Leeser and G. Brown, eds.,
Specification, Verification and Synthesis:
Mathematical Aspects,
Procs. of a Workshop, 5-7 July 1989,
Ithaca, N.Y.,
Springer-Verlag,
1989.

\bibitem{Melham:calgary86}
Thomas F. Melham,
Abstraction Mechanisms for Hardware Verification, in:
G. Birtwistle and P. Subrahmanyam, eds.,
VLSI Specification, Verification and Synthesis,
Kluwer Academic Publishers, Boston, 1988,
pp. 267-291.
Also Report No. 103, Computer Laboratory, Cambridge University,
January 1987.

\bibitem{Melham:thesis}
Thomas F. Melham,
Formalizing Abstraction Mechanisms for Hardware Verification in
Higher Order Logic,
Ph.D. Thesis,
Computer Laboratory, Cambridge University,
1989.

\bibitem{Moszkowski:thesis}
Benjamin C. Moszkowski,
Reasoning about Digital Circuits,
Ph.D. Thesis,
Report CS-83-970,
Dept. of Computer Science,
Stanford University,
1983.

\bibitem{Moszkowski:journal}
Benjamin Moszkowski,
A Temporal Logic for Multilevel Reasoning about Hardware,
IEEE Computer Vol. 18, No. 2,
February 1985,
pp. 10-19.

\bibitem{Pygott84}
C. Pygott,
Electrical, Environmental and Timing Specification of the Viper
Microprocessor,
Memorandum No. 3753,
RSRE,
British Ministry of Defense,
December 1984.

\bibitem{Richards:tech84}
Martin Richards,
BSPL: A Language for Describing the Behaviour of Synchronous Hardware,
Report No. 84, Computer Laboratory,
Cambridge University,
July 1986.

\bibitem{Seitz}
C. Seitz,
Chapter 7: System Timing, in:
C. Mead and L. Conway,
Introduction to VLSI Systems,
Addison-Wesley,
Reading, Massachusetts, 1980,
pp. 218-262.

\bibitem{Subra:calgary86}
P. A. Subrahmanyam,
Toward a Framework for Dealing with System Timing in
Very High Level Silicon Compilers, in:
G. Birtwistle and P. Subrahmanyam, eds.,
VLSI Specification, Verification and Synthesis,
Kluwer Academic Publishers, Boston, 1988,
pp. 159-215.

\bibitem{Subra:cornell}
P. A. Subrahmanyam,
What's in a Timing Discipline ?:
Considerations in the Specification and Synthesis of Systems with
Interacting Asynchronous and Synchronous Components, in:
M. Leeser and G. Brown, eds.,
Specification, Verification and Synthesis:
Mathematical Aspects,
Procs. of a Workshop, 5-7 July 1989,
Ithaca, N.Y.,
Springer-Verlag,
1989.

\bibitem{VanTassel:thesis}
John P. Van Tassel,
The Semantics of VHDL with VAL and HOL:
Towards Practical Verification Tools,
M.Sc. Thesis,
Dept. of Computer Science and Engineering,
Wright State University,
1989.

\bibitem{EHDM}
F. W. von Henke, J. S. Crow, R. Lee, J. M. Rushby and R. A. Whitehurst,
The EHDM Verification Environment: An Overview,
Proceedings of the 11th National Computer Security Conference,
Baltimore, October 1988,
pp. 147-155.

\bibitem{Weise:thesis}
Daniel Weise,
Formal Multilevel Hierarchical Verification of Synchronous
MOS VLSI Circuits,
Ph.D Thesis,
Report No. 978,
Artificial Intelligence Laboratory,
Massachusetts Institute of Technology,
1987.

\end{thebibliography}