An Engineering Approach to Formal Digital System Design

. This paper describes a first attempt at building design tools that amalgamate theorem proving and engineering methods. To gain acceptance such a tool must focus on the engineering task and proof steps must be hidden. From these ideas a prototype system based on the HOL proof assistant has been designed. The key features of this system are threefold. First, we use window reasoning for modelling the design process; Second, we have defined a set of application specific derived inference rules that implement common design tasks; Third, we have extended the design representation in logic with annotations to support efficient algorithmic reasoning. 1 Introduction As production technology has continued to improve during the last decades, the complexity of digital systems has increased accordingly. This ever increasing complexity has led to digital systems having shorter life cycles and to the design task growing more difficult. At the same time, the use of digital systems in safety critica..