Hardware

Abstract

In Sect. 3.1 we introduce the classical model of digital circuits. This includes the classical definition of the depth d(g) of a gate g in a circuit as the length of a longest path from an input of the circuit to the gate. For the purpose of timing analysis in a later section, we also introduce the function sp(g) measuring the length of a shortest path from an input of the circuit to gate g. We present the classical proof by pigeon hole principle that the depth of gates is well defined. By induction on the depth of gates we then conclude the classical result that the semantics of switching circuits is well defined.

A few basic digital circuits are presented for later use in Sect. 3.2. This is basically the same collection of circuits as presented in [12].

In Sect. 3.3 we introduce two hardware models: i) the usual digital model consisting of digital circuits and 1-bit registers as presented in [12, 11] and ii) a detailed model involving propagation delays, set up and hold times as presented, e.g., in [14, 10]. Working out the proof sketch from [10], we formalize timing analysis and show by induction on depth that, with proper timing analysis, the detailed model is simulated by the digital model. This justifies the use of the digital model as long as we use only gates and registers.

In the very simple Sect. 3.4 we define n-bit registers which are composed of 1-bit registers in order to use them as single components h.R of hardware configurations h.

As we aim at the construction of memory systems, we extend in Sect. 3.5 both circuit models with open collector drivers, tristate drivers, buses, and a model of main memory. As new parameters we have to consider in the detailed model the enable and disable times of drivers. Also – as main memory is quite slow – we have to postulate that, during accesses to main memory, its input signals should be stable in the detailed model, i.e., there should be no glitches on the input signals to the memory. We proceed to construct digital interface circuitry for controlling buses and main memory and show in the detailed model that, with that circuitry, buses and main memory are properly operated. These results permit to abstract buses, main memory and their interface circuitry to the digital model. So in later constructions, we only have to worry about proper operation of the interface circuitry in the digital world, and we do not have to reconsider the detailed model.

For readers who suspect that we might be paranoid, we also prove that the proof obligations for the interface circuitry which we impose on the digital model cannot be derived from the digital model itself. Indeed, we construct a bus control that i) is provably free of contention in the digital model and which ii) has – for common technology parameters – bus contention for about 1/3 of the time. As “bus contention” translates in the real world to “short circuit”, such circuits destroy themselves.

Thus, the introduction of the detailed hardware model solves a very real problem which is usually ignored in previous work, such as [12]. One would suspect that the absence of such an argument leads to constructions that malfunction in one way or another. In [12], buses are replaced by multiplexers, so bus control is not an issue. But the processor constructed there has caches for data and instructions, which are backed up by a main memory. Moreover, the interface circuitry for the instruction cache as presented in [12] might produce glitches. On the other hand, the (digital) design in [12] was formally verified in subsequent work [1, 3]; it was also put on a field programmable gate array (FPGA) and ran correctly immediately after the first power up without ever producing an error. If there are no malfunctions where one would worry about them in view of later insights, one looks for explanations. It turned out that the hardware engineer who transferred the design to the FPGA had made a single change to the design (without telling anybody about it): he had put a register stage in front of the main memory. In the physical design, this register served as interface circuitry to the main memory and happened to conform to all conditions presented in Sect. 3.5. Thus, although the digital portion of the processor was completely verified, the design in the book still contained a bug, which is only visible in the detailed model. The bug was fixed without proof (indeed without being recognized) by the introduction of the register stage in front of the memory. In retrospect, in 2001 the design was not completely verified; that it ran immediately after power up involved luck.

A few constructions for control automata are presented for later use in Sect. 3.6. This is basically the same collection of automata as presented in [12].