***
*** PDP 8
***
*** This group of modules represents a simplified specification of the DEC PDP-8.
***

*** 
*** NOTE: you must import the BINARY module first.
*** some unnecessary stuff from here.
***

*** This module defines the operators that extract bit fields from instructions,
*** as well as the words themselves
fmod PDP8-WORD is

    protecting BINARY .
    
    sorts MachineWord OpCode Address .
    
    subsort MachineWord < Bits .
    subsort OpCode < Bits .
    subsort Address < Bits .

    *** Operators to extract the various
    *** instruction fields
    op opcode : MachineWord -> OpCode .
    op addr : MachineWord -> Address .
    op pagebit : MachineWord -> Bool .
    op indir : MachineWord -> Bool .

    *** Operators for 12-bit addition, 
    *** and the 13th bit of 12-bit addition
    op _+_ : MachineWord MachineWord -> MachineWord .
    op _+13_ : MachineWord MachineWord -> Bit .
    
    *** AND operator - note we have only *declared*
    *** this operator, not *defined* it. (If you
    *** have done the exercises from Chapter 8, you
    *** will have defined an AND operator that you
    *** can use.)
    op _AND_ : MachineWord MachineWord -> MachineWord .

    vars X Y : MachineWord .
    vars a b c d e f g h i j k l : Bit .
    
    mb (a b c d e f g h i
        j k l) : MachineWord .       *** 12 bits
    mb (a b c) : OpCode .            *** 3 bits
    mb (a b c d e f g) : Address  .  *** 7 bits

    *** Opcode is always most significant 3 bits
    eq opcode(Y) = bits(Y,11,9) .

    *** Address is always least significant 7 bits
    eq addr(Y) = bits(Y,6,0) .

    *** extract page bit
    ceq pagebit(Y) = true if bits(Y,8,8) == 1 .
    ceq pagebit(Y) = false if bits(Y,8,8) == 0 .

    *** extract indirection bit
    ceq indir(Y) = true if bits(Y,7,7) == 1 .
    ceq indir(Y) = false if bits(Y,7,7) == 0 .

    *** 12-bit addition
    eq X + Y = bits(X ++ Y, 11, 0) .

    *** 13th bit of addition - used to set L flag
    eq X +13 Y = bits(X ++ Y, 12, 12) .
endfm

*** This module defines memory
fmod MEM is

    protecting PDP8-WORD .

    sort Mem .

    op _[_] : Mem MachineWord -> MachineWord .
    op _[_/_] : Mem MachineWord MachineWord -> Mem .

    var M : Mem .
    vars A I J : MachineWord .

    eq M[A / I][I] = A .
    eq M[A / I][J] = M[J] [owise] .
endfm

*** This module defines memory addressing, reading and writing
fmod MEM-OP is

    protecting MEM .

    *** Operators for memory addressing,
    *** reading and writing
    op maddr : Mem MachineWord -> MachineWord .
    op mval : Mem MachineWord -> MachineWord .
    op Mw : Mem MachineWord MachineWord -> Mem .

    var M : Mem .
    vars PC VAL : MachineWord .
    
    ceq maddr(M,PC) = (0 0 0 0 0 addr(M[PC]))
        if pagebit(M[PC]) == false and
                         indir(M[PC]) == false .
    ceq maddr(M,PC) = (bits(PC,11,7) addr(M[PC]))
        if pagebit(M[PC]) == true and
                         indir(M[PC]) == false .
    ceq maddr(M,PC) = M[(0 0 0 0 0 addr(M[PC]))]
        if pagebit(M[PC]) == false and
                         indir(M[PC]) == true .
    ceq maddr(M,PC) = M[(bits(PC,11,7) addr(M[PC]))]
        if pagebit(M[PC]) == true and
                         indir(M[PC]) == true .
                                       
    eq mval(M,PC) = M[maddr(M,PC)] .
    eq Mw(M,PC,VAL) = M[VAL / maddr(M,PC)] .
endfm

*** This module defines the state of the PDP-8
fmod PDP8-STATE is

    protecting MEM-OP .
    
    sorts PDP8State .

    *** operator to construct a PDP-8 state from
    *** component parts
    op (_,_,_,_) : MachineWord MachineWord Bit
        Mem -> PDP8State .

    *** operators to extract fields from a
    *** PDP-8 state
    op a_ : PDP8State -> MachineWord .
    op pc_ : PDP8State -> MachineWord .
    op l_ : PDP8State -> Bit .
    op mem_ : PDP8State -> Mem .
    
    var M : Mem .
    vars A PC : MachineWord .
    var L : Bit .
    
    eq a(A,PC,L,M) = A .
    eq pc(A,PC,L,M) = PC .
    eq l(A,PC,L,M) = L .
    eq mem(A,PC,L,M) = M .
endfm

*** This module defines the PDP-8 State and Next-State functions
fmod PDP8 is

    protecting PDP8-STATE .

    *** State and Next-State functions
    op PDP8 : Int PDP8State -> PDP8State .
    op next : PDP8State -> PDP8State .

    *** Constants
    ops ONE TWO : -> MachineWord .

    *** Ancilliary function used in conditional
    *** instruction
    op skip : Mem MachineWord -> MachineWord .

    vars A PC : MachineWord .
    var L : Bit .
    var M : Mem .
    var T : Int .
            
    *** Define constants
    eq ONE = (0 0 0 0 0 0 0 0 0 0 0 1) .
    eq TWO = (0 0 0 0 0 0 0 0 0 0 1 0) .


    *** Define the State function
    eq PDP8(0,(A,PC,L,M)) = (A,PC,L,M) .
    eq PDP8(T,(A,PC,L,M)) =
        next(PDP8(T - 1,(A,PC,L,M))) [owise] .

    *** Define the ancilliary skip function
    eq skip(M,PC) = if mval(M,PC) ==
                      (1 1 1 1 1 1 1 1 1 1 1 1) then
                     PC + TWO else PC + ONE fi .

    ***
    *** Now we do the various cases of the Next-State
    *** function
    ***

    *** AND
    ceq next((A,PC,L,M)) =
            (A AND mval(M,PC),PC + ONE,L,M)
        if opcode(M[PC]) == 0 0 0 .

    *** TAD
    ceq next((A,PC,L,M)) =
            (A + mval(M,PC),PC + ONE, A +13 mval(M,PC),M)
        if opcode(M[PC]) == 0 0 1 .

    *** ISZ
    ceq next((A,PC,L,M)) =
            (A, skip(M,PC), L, Mw(M,PC,mval(M,PC) + ONE))
        if opcode(M[PC]) == 0 1 0 .

    *** DCA
    ceq next((A,PC,L,M)) =
            (0 0 0 0 0 0 0 0 0 0 0 0,PC + ONE, L,
            Mw(M,PC,A))
        if opcode(M[PC]) == 0 1 1 .
        
    *** JSR
    ceq next((A,PC,L,M)) =
            (A, mval(M,PC) + 1, L, Mw(M,PC,PC + ONE))
        if opcode(M[PC]) == 1 0 0 .
        
    *** JMP
    ceq next((A,PC,L,M)) = (A, mval(M,PC), L, M)
        if opcode(M[PC]) == 1 0 1 .
endfm