Formal Methods: Why Should I Care? The Development of the T800 Transputer Floating−Point Unit
Jeremy Gibbons · 1993
The term `formal methods' is a general term for precise mathematically-based techniques used in the development of computer systems, both hardware and software. This paper discusses formal methods in general, and in particular describes their successful role in specifying, constructing and proving correct the floating-point unit of the Inmos T800 transputer chip. 1. Introduction The need for reliable computer systems is increasing rapidly, in step with our growing dependence on computers in daily life. This need can only be met by developing more rigorous methods for constructing these systems. The term `formal methods' is a blanket term for such precise, mathematically-based techniques for the development of computer systems. In this paper, we aim to give an introduction to formal methods in general, and to discuss how they helped in constructing the floating-point unit of the Inmos T800 transputer chip. The transputer [Inmos Ltd 1988b] is a microprocessor chip designed specificall...