Previous Contents Next

Gordon's Computer

Chapter 12: Gordon's Computer

In this chapter, we will look at another computer-based example: a 'made-up' machine called Gordon's Computer (after Prof. Mike Gordon, Cambridge Computer Laboratory, who first used it in 1983). The general layout is shown in fig 1.


Fig.1. Gordon's Computer Front Panel

Gordon's Computer is a commonly-used example which, unlike the previous two examples, includes inputs and outputs.

12.1. Gordon's Computer Programmer's Level: Informal Description

As it is usually described, Gordon's Computer is a box containing a simple computer, with a number of lights (representing outputs) and switches, a button and a dial (representing inputs). The computer has the following state elements.

Because we have 16-bit words and 13-bit memory addresses, we can fit a complete memory address into a word with three bits left over: we use these to specify one of eight instructions.

12.1.1. Inputs and Outputs

Programs are loaded into Gordons's Computer using, and execution is controlled by, a bank of 16 two-position switches; a push-button; and a four-position dial. The output is displayed by a bank of 16 lights; a bank of 13 lights; and two single lights.

The behaviour of the outputs is as follows.

The behaviour of the inputs is as follows.

By using the switches, dial and button it is possible to (tediously) program the machine, as well as start/stop execution.

12.2. Dealing with Input-Output

Before we get into the detail of the specification, we need to consider how to deal with inputs and outputs. It looks like we might be going back to our earlier way of dealing with hardware - using streams and stream transformers. To some degree this is true: however, there are some minor differences. Let us consider inputs first. As the machine executes instructions, and moves through a sequence of states, we might reasonably expect a stream of inputs to be continually arriving. We might wish to define a Maude operator something like this:


F : Int State InputStreams -> State .

This is (broadly) what we will do. The addition of outputs complicates matters a bit. Since an iterated map computes the state at a particular time, we should expect the output to be a set of output values - outputs at a given time - and not a set of output streams. Something like this:


F : Int State InputStreasm -> State OutputValues .

As we have already seen, we cannot define Maude modules that output multiple values: we need to define a tuple sort for that. In general, when dealing with inputs and outputs, you can expect to have to define a range of sorts representing various tuples, streams sorts, and so on - and Gordon's Computer is no different.

12.3. Gordon's Computer Programmer's Level: Formal Description

The complete description in Maude is here (minus the BINARY module). As usual, we will consider each module in turn.

12.3.1. MACHINE-WORD

The MACHINE-WORD module is as follows.


fmod MACHINE-WORD is
    protecting BINARY .

    sorts Address Word Opcode .

    subsort Address < Bits .
    subsort Word < Bits .
    subsort Opcode < Bits .

    ops zero one : -> Word .
    op opcode : Word -> Opcode .
    op addr : Word -> Address .
    op _+_ : Word Word -> Word [assoc comm] .
    op _-_ : Word Word -> Word .
    op _+_ : Address Address -> Address [assoc comm] .
    
    vars a b c d e f g h : Bit .
    vars i j k l m n o p : Bit .
    vars A B : Word .
    vars C D : Address .

    mb (a b c) : Opcode .
    mb (a b c d e f g h i j k l m) : Address .
    mb (a b c d e f g h i j k l m n o p ) : Word .

    eq one = (0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1) .
    eq zero = (0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0) .

    eq opcode(A) = bits(A,15,13) .
    eq addr(A) = bits(A,12,0) .

    eq A + B = bits(A ++ B, 15,0) .
    eq A - B = bits(A ++ (not B ++ one), 15, 0) .
    eq C + D = bits(C ++ D, 12, 0) .
endfm

This module is very similar to others you have seen: it defines a number of fixed-length bit strings, representing opcodes, memory addresses, and memory words. It also defines: some constants, some extraction operators (for opcodes and addresses) and some arithmetic operators.

12.3.2. MEM

The memory module is almost identical to those you have already seen and we will leave it out.

12.3.3. GORDON-STATE

Although broadly similar to other examples, the module defining the state is more complex than others because of the need to deal with inputs and outputs.


fmod GORDON-STATE is
    protecting MEM .

    *** The four position dial.
    sort Dial .

    *** Streams of: switch values, button pushes
    *** and dial positions.
    sorts SwitchStr BitStr DialStr .

    *** The state of the machine.
    sort GordonState .

    *** The output of the machine.
    sort GordonOut .

    *** The combined state and output
    sort GordonAll .

    *** Constants representing dial positions
    ops LoadPC LoadACC Store Run : -> Dial .

    *** Operators to evaluate streams,
    *** returning value on a stream at a given
    *** time.
    op _(_) : SwitchStr Int -> Word .
    op _(_) : BitStr Int -> Bit .
    op _(_) : DialStr Int -> Dial .

    *** Operator to make a machine state tuple.
    op _,_,_,_ : Mem Word Address Bit -> GordonState .

    *** Operator to make an output tuple.
    op _,_,_,_ : Word Address
        Bit Bit -> GordonOut .

    *** Operator to combine state and output.
    op _,_ : GordonState GordonOut -> GordonAll .
endfm

We introduce a sort Dial representing dial positions, together with four possible constant values. In addition, we introduce sorts representing streams of: 16-bit words, bits, and dial positions. The represent (respectively) streams of switch positions, button presses and dial positions. We also introduce the evaluation operators (_(_)) for determining the value on a stream at a given time. In previous examples, we have only needed one tuple sort representing the state of the machine. Here we need three.

12.3.4. GORDON-PM

The main functionality is defined in the module GORDON-PM. We will present it in full first, before looking at some of the component parts.


fmod GORDON-PM is
    protecting GORDON-STATE .

    *** The main iterated map function
    op GORDON : Int GordonState SwitchStr
        BitStr DialStr -> GordonAll .

    *** The state function
    op GORDON-STATE : Int GordonState SwitchStr
        BitStr DialStr -> GordonState .

    *** The output function
    op GORDON-OUT : Int GordonState SwitchStr
        BitStr DialStr -> GordonOut .

    *** The next-state function
    op next : GordonState Word Bit Dial -> GordonState .

    *** function to compute the output at a given time
    op out : GordonState -> GordonOut .
    
    *** function to execute one instruction
    op exec : GordonState -> GordonState .
    
    var M : Mem .
    var ACC : Word .
    var PC : Address .
    var IDLE : Bit .
    var SWstr : SwitchStr .
    var BUTTONstr : BitStr .
    var DIALstr : DialStr .
    var T : Int .
    var SW : Word .
    var BUTTON : Bit .
    var DIAL : Dial .

    *** The state and output of the machine at any given
    *** time is computed by the state and output functions
    eq GORDON(T,M,ACC,PC,IDLE,SWstr,BUTTONstr,DIALstr) =
        (GORDON-STATE(T,M,ACC,PC,IDLE,SWstr,BUTTONstr,DIALstr),
         GORDON-OUT(T,M,ACC,PC,IDLE,SWstr,BUTTONstr,DIALstr)) .

    *** At time zero, the state of the machine is just the
    *** initial state. Remember that GORDON computes the
    *** state *and* output, so to just get the state we
    *** need to apply the g1 function.
    eq GORDON-STATE(0,M,ACC,PC,IDLE,SWstr,BUTTONstr,DIALstr) =
        (M,ACC,PC,IDLE) .

    *** At other times, the state of the machine is the
    *** next state function applied to the state at the
    *** machine at the time before.
    ceq GORDON-STATE(T,M,ACC,PC,IDLE,SWstr,BUTTONstr,DIALstr) =
        next(GORDON-STATE(T - 1,M,ACC,PC,IDLE,
          SWstr,BUTTONstr,DIALstr),
          SWstr(T),BUTTONstr(T),DIALstr(T)) if T > 0 .

    *** At any time, the output of the machine is the out
    *** function applied to the state.
    eq GORDON-OUT(T,M,ACC,PC,IDLE,SWstr,BUTTONstr,DIALstr) =
     out(GORDON-STATE(T,M,ACC,PC,IDLE,SWstr,
         BUTTONstr,DIALstr)) .

    *** If the machine is idle, and the button pressed while
    *** the dial is in the 'LoadPC' position, we load the
    *** switches into the program counter.
    ceq next(M,ACC,PC,IDLE,SW,BUTTON,DIAL) =
        (M, ACC, bits(SW,12,0), 1) if (IDLE == 1) and
                                      (BUTTON == 1) and
                                      (DIAL == LoadPC) .
                      
    *** If the machine is idle, and the button pressed while
    *** the dial is in the 'LoadACC' position, we load the
    *** switches into the accumulator.
    ceq next(M,ACC,PC,IDLE,SW,BUTTON,DIAL) =
        (M, SW, PC, 1) if (IDLE == 1) and
                          (BUTTON == 1) and
                          (DIAL == LoadACC) .
              
    *** If the machine is idle, and the button pressed while
    *** the dial is in the 'Store' position, we store the
    *** accumulator in the memory at the address specified by
    *** the program counter.
    ceq next(M,ACC,PC,IDLE,SW,BUTTON,DIAL) =
        (M[ACC / PC], ACC, PC, 1) if (IDLE == 1) and
                               (BUTTON == 1) and
                               (DIAL == Store) .

    *** If the machine is idle and the button is not pressed,
    *** we remain idle; if the machine is running and the
    *** button is pressed, it stops.
    ceq next(M,ACC,PC,IDLE,SW,BUTTON,DIAL) =
        (M, ACC, PC, 1) if ((IDLE == 1) and
                             (BUTTON == 0)) or
                            ((IDLE == 0) and
                              (BUTTON == 1)) .
             
     *** If the machine is running and we do not press the
     *** button, it executes the next instruction; if it is
     *** idle and we press the button with the dial in the
     *** 'Run' position, we start execution.
     ceq next(M,ACC,PC,IDLE,SW,BUTTON,DIAL) =
        exec(M, ACC, PC, 0) if ((IDLE == 0) and
                                (BUTTON == 0)) or
                               ((IDLE == 1) and
                                (BUTTON == 1) and
                                (DIAL == Run)) .

    *** Stop the machine.
    ceq exec(M,ACC,PC,IDLE) =
        (M,ACC,PC,1) if opcode(M[PC]) == (0 0 0) .

    *** Jump unconditionally.
    ceq exec(M,ACC,PC,IDLE) =
        (M,ACC,addr(M[PC]),0)
                        if opcode(M[PC]) == (0 0 1) .
            
    *** A successful conditional jump (ACC == 0) .
    ceq exec(M,ACC,PC,IDLE) =
        (M,ACC,addr(M[PC]),0)
                        if opcode(M[PC]) == (0 1 0)
                           and (ACC == zero) .
               
    *** An unsuccessful conditional jump (ACC =/= 0)
    ceq exec(M,ACC,PC,IDLE) =
        (M,ACC,PC + one,0)
                        if opcode(M[PC]) == (0 1 0)
                           and (ACC =/= zero) .
               
    *** Addition.
    ceq exec(M,ACC,PC,IDLE) =
        (M,ACC + M[addr(M[PC])],PC + one,0)
                        if opcode(M[PC]) == (0 1 1) .

    *** Subtraction.
    ceq exec(M,ACC,PC,IDLE) =
        (M,ACC - M[addr(M[PC])],PC + one,0)
                        if opcode(M[PC]) == (1 0 0) .

    *** Load.
    ceq exec(M,ACC,PC,IDLE) =
        (M,M[addr(M[PC])],PC + one,0)
                        if opcode(M[PC]) == (1 0 1) .

    *** Store.
    ceq exec(M,ACC,PC,IDLE) =
        (M[ACC / addr(M[PC])],ACC,PC + one,0)
                        if opcode(M[PC]) == (1 1 0) .
            
    *** Skip (no-op).
    ceq exec(M,ACC,PC,IDLE) =
        (M,ACC,PC + one,0)
                        if opcode(M[PC]) == (1 1 1) .

    *** The output function
    eq out(M,ACC,PC,IDLE) = (ACC,PC,IDLE,1) .
endfm

The Iterated Map Functions

We divide the computation of the state and output at time T into two parts: each of which is computed separately and then recombined:


    *** The main iterated map function
    op GORDON : Int GordonState SwitchStr
        BitStr DialStr -> GordonAll .

    *** The state and output of the machine at any given
    *** time is computed by the state and output functions
    eq GORDON(T,M,ACC,PC,IDLE,SWstr,BUTTONstr,DIALstr) =
        (GORDON-STATE(T,M,ACC,PC,IDLE,SWstr,BUTTONstr,DIALstr),
     GORDON-OUT(T,M,ACC,PC,IDLE,SWstr,BUTTONstr,DIALstr)) .

The state is defined in terms of a fairly conventional iterated map.


    *** The state function
    op GORDON-STATE : Int GordonState SwitchStr
        BitStr DialStr -> GordonState .

    *** At time zero, the state of the machine is just the
    *** initial state.
    eq GORDON-STATE(0,M,ACC,PC,IDLE,SWstr,BUTTONstr,DIALstr) =
        (M,ACC,PC,IDLE) .

    *** At other times, the state of the machine is the
    *** next state function applied to the state at the
    *** machine at the time before.
    ceq GORDON-STATE(T,M,ACC,PC,IDLE,SWstr,BUTTONstr,DIALstr) =
        next(GORDON-STATE(T - 1,M,ACC,PC,IDLE,
          SWstr,BUTTONstr,DIALstr),
          SWstr(T),BUTTONstr(T),DIALstr(T)) if T > 0 .

The main difference from previous examples is that GORDON-STATE takes as arguments both the initial state of the machine and the input streams.

The output is computed by a separate function.


    *** The output function
    op GORDON-OUT : Int GordonState SwitchStr
        BitStr DialStr -> GordonOut .

    *** At any time, the output of the machine is the out
    *** function applied to the state.
    eq GORDON-OUT(T,M,ACC,PC,IDLE,SWstr,BUTTONstr,DIALstr) =
     out(GORDON-STATE(T,M,ACC,PC,IDLE,SWstr,
         BUTTONstr,DIALstr)) .

The actual output will be computed by the out function. However, notice that basically the output at time T is just a function of the state at time T. This is usually the case. It is also usual for the actual function of the state to be quite simple.

Next-State Function

Unlike previous next-state functions, the one for Gordon's Computer does not actually execute instructions - that is left for a sub-function called exect. Instead, the next-state function deals with inputs.

If the button is pushed when the machine is not running and the dial is in the LoadPC position, we load the least-significant 13 switch values into PC.


    *** If the machine is idle, and the button pressed while
    *** the dial is in the 'LoadPC' position, we load the
    *** switches into the program counter.
    ceq next(M,ACC,PC,IDLE,SW,BUTTON,DIAL) =
        (M, ACC, bits(SW,12,0), 1) if (IDLE == 1) and
                                      (BUTTON == 1) and
                                      (DIAL == LoadPC) .

If the button is pushed when the machine is not running and the dial is in the LoadACC position, we load the switch values into ACC.


    *** If the machine is idle, and the button pressed while
    *** the dial is in the 'LoadACC' position, we load the
    *** switches into the accumulator.
    ceq next(M,ACC,PC,IDLE,SW,BUTTON,DIAL) =
        (M, SW, PC, 1) if (IDLE == 1) and
                          (BUTTON == 1) and
                          (DIAL == LoadACC) .

Similarly, the Store position controls storing values into memory.


    *** If the machine is idle, and the button pressed while
    *** the dial is in the 'Store' position, we store the
    *** accumulator in the memory at the address specified by
    *** the program counter.
    ceq next(M,ACC,PC,IDLE,SW,BUTTON,DIAL) =
        (M[ACC / PC], ACC, PC, 1) if (IDLE == 1) and
                                     (BUTTON == 1) and
                                     (DIAL == Store) .

If the machine is not currently running, and we do not do anything (i.e. we do not push the button), then the machine will remain idle. However, if it was running and we do push the button, it stops.


    *** If the machine is idle and the button is not pressed,
    *** we remain idle; if the machine is running and the
    *** button is pressed, it stops.
    ceq next(M,ACC,PC,IDLE,SW,BUTTON,DIAL) =
        (M, ACC, PC, 1) if ((IDLE == 1) and
                            (BUTTON == 0)) or
                           ((IDLE == 0) and
                            (BUTTON == 1)) .

Finally, if the machine is currently running and we do not push the button, it keeps running and we call the exec function to compute an instruction. Similarly, if the machine is not running and we do push the button, it starts running and again we call the exec function to compute an instruction.


    *** If the machine is running and we do not press the
    *** button, it executes the next instruction; if it is
    *** idle and we press the button with the dial in the
    *** 'Run' position, we start execution.
    ceq next(M,ACC,PC,IDLE,SW,BUTTON,DIAL) =
        exec(M, ACC, PC, 1) if ((IDLE == 0) and
                                (BUTTON == 0)) or
                               ((IDLE == 1) and
                                (BUTTON == 1) and
                                (DIAL == Run)) .

Exec Function

We will not consider the exec function in detail - it is very similar to other next-state functions you have already seen. There is one case for each instruction except for the conditional jump which has two (one each for a successful and an unsuccessful jump).

Output Function

The last function to consider is out, which is very simple.


    *** The output function
    eq out(M,ACC,PC,IDLE) = (ACC,PC,IDLE,1) .

This essentially says that: the value of the 16-light bank is the same as ACC; the value of the 13-light bank; the value of the first single light is the same as the IDLE bit; and the second single light is always on.

Why is the second light, which tells us when the machine can be interrupted, always on? The answer is to do with the level of temporal abstraction we have chosen - that is, the length of each clock cycle. We have picked a clock in which each cycle lasts for one instruction. Effectively this means we only observe the state and output of the machine ('look at' it, if you like) at the start/end of machine instructions. That is, between instructions - at precisely those times that the machine can be interrupted. So we only observe the machine at those times when the light is on. If we wish to observe it at other times, we will need to use a lower level of temporal abstraction, which we will not do in this module.

Previous Contents Next