Formal Design of a Class of Computers

| its high stage: abstract microprogramming

Li-Guo Wang1

Department of Computer Science,
University of Edinburgh,

Michael Mendler2

Department of Computer Science,
Technical University of Denmark,

Abstract
We present a novel construction model of hardware and demonstrate how to use it in the entire process of formally designing a class of computers involving their specification, construction, and verification. In this paper we focus on the high stages of the design: the refinement from the behaviour specification at machine instruction level to the abstract microprogram at the term transition level. The concept of term transition introduced in this paper establishes a new generic high-level design stage which is common for computer architecture and design. Our approach is based on formal syntax and formal proof and constitutes a framework for the rigorous specification and verification of hardware synthesis systems.

1 Introduction

As formal methods are striving to be understood and accepted by industry the formalization of the design process itself | as opposed to mere post-design verification | receives more and more attention [1, 5, 13, 14, 29, 35]. In this paper we discuss the formal design of a class of computers. By formal design we mean an approach based on theorem-proving and by a class of computers we mean the specification scheme of an abstract computer characterizing each computer in the class.
We present a construction model of hardware which applies all the way from an abstract behaviour specification to an unknown structural implementation. It constitutes a new foundation for formal design where the traditional verificationoriented hardware model does not meet the goal. It admits finer-grained design descriptions in which aspects of hardware and software may coexist, and it

1The author is supported by a scholarship from Siemens AG Munich and scholarship from SERC GR/F 35890 U.K.
2The author is supported by a Human Capital and Mobility fellowship in the EuroForm network.