Previous Contents Next
In this chapter we will look at a simple example processor at the level of abstraction seen by an assembly language programmer. We will call this the Programmer's Model. It is often called other things (for example, the Architecture): unfortunately, the other commonly-used names are a bit vague on occasion (which is why we have our own). The complete file can be found here, though note that you will need to read the BINARY module defined earlier into Maude first. I strongly recommend running this example and making some experimental changes. (Note: ignore the warning about the __ operator and membership axioms.)
The first module, which imports BINARY, defines the various different length substrings we will need, along with various operators that extract bit strings and perform arithmetic. Our machine will have 10-bit memory addresses, and 16-bit words (memory will be word addressable). Instructions are 16 bits, with a 3-bit opcode field and either three 3-bit operand fields representing register addresses, or one 3-bit and one 10-bit operand field, representing a register and a memory address.
*** *** Module for dealing with machine words and instruction formats. *** fmod MACHINE-WORD is protecting BINARY . *** We import the BINARY module defined previously *** 3-bit OpField, 10-bit Address, 16-bit Word sorts OpField Address Word . subsort OpField < Bits . subsort Address < Bits . subsort Word < Bits . *** Instruction field extraction functions op opcode : Word -> OpField . *** The opcode field. ops rega regb regc : Word -> OpField . *** The three register address *** fields. ops address value : Word -> Address . *** Field used for addresses *** and constants. *** 16-bit addition. This is for the addition instruction. op _+_ : Word Word -> Word . *** 10-bit addition. This is for address arithmetic. op _+_ : Address Address -> Address . var Y : Bits . vars A1 A2 A3 A4 A5 A6 A7 A8 : Bits . vars A9 A10 A11 A12 A13 A14 A15 A16 : Bits . var V W : Word . var A B : Address . mb (A1 A2 A3) : OpField . mb (A1 A2 A3 A4 A5 A6 A7 A8 A9 A10) : Address . mb (A1 A2 A3 A4 A5 A6 A7 A8 A9 A10 A11 A12 A13 A14 A15 A16) : Word . *** EXPERIMENT: Try uncommenting the three [conditional] membership axioms *** below, and commenting out the three above. *** (You may want to change the reductions at the bottom to something *** much simpler!) ***cmb Y : OpField if | Y | = 3 . ***cmb Y : Address if | Y | = 10 . ***cmb Y : Word if | Y | = 16 . *** opcode and rega are always bits 15-13, 12-10 resp. eq opcode(V) = bits(V,15,13) . eq rega(V) = bits(V,12,10) . *** regb and regc are bits 9-7, 6-4 resp. (3-0 void) eq regb(V) = bits(V,9,7) . eq regc(V) = bits(V,6,4) . *** value (set instr only) and address are bits 9-0 *** Note that the defns. of these are the same, so we could omit one. eq value(V) = bits(V,9,0) . eq address(V) = bits(V,9,0) . *** We define 16 and 10 bit addition to be bitwise addition (from the *** module Bits above) truncated to 16 and 10 bits respectively *** Notice we need to truncate because n-bit addition generates an n+1 bit result eq V + W = bits(V ++ W,15,0) . eq A + B = bits(A ++ B,9,0) . endfm
Notice that if we had not used ++ for addition over arbitrary length bit strings, the final two equations would have led to a non-terminating system (Exercise: explain why).
The following modules deal with memory and registers. We treat memory (and registers) very much like arrays - which we saw in an earlier chapter. Note that memory and registers are very similar In retrospect, it may be better to use a different notation for registers, to avoid confusion. However, the risk is small.
*** *** Module for representing memory.. *** fmod MEM is protecting MACHINE-WORD . sorts Mem . *** New type representing memory op _[_] : Mem Address -> Word . *** Read op _[_/_] : Mem Word Address -> Mem . *** Write var M : Mem . vars A B : Address . var W : Word . eq M[W / A][A] = W . eq M[W / A][B] = M[B] [owise] . endfm *** *** Module for representing registers. *** fmod REG is protecting MACHINE-WORD . sorts Reg . *** New type representing registers. op _[_] : Reg OpField -> Word . *** Read op _[_/_] : Reg Word OpField -> Word . *** Write var R : Reg . var A B : OpField . var W : Word . eq R[W / A][A] = W . eq R[W / A][B] = R[B] [owise] . endfm
The following module represents the state tuple of the microprocessor - a program memory, a data memory, a program counter, and a set of registers.
*** *** State of SPM, together with tupling and *** projection functions *** fmod SPM-STATE is protecting MEM . protecting REG . sort SPMstate . op (_,_,_,_) : Mem Mem Word Reg -> SPMstate . *** Project out program and data memory ops mp_ md_ : SPMstate -> Mem . *** Project out program counter op pc_ : SPMstate -> Address . *** project out registers op reg_ : SPMstate -> Reg . var S : SPMstate . vars MP MD : Mem . var PC : Address . var REG : Reg . eq mp(MP,MD,PC,REG) = MP . eq md(MP,MD,PC,REG) = MD . eq pc(MP,MD,PC,REG) = PC . eq reg(MP,MD,PC,REG) = REG . endfm
This module describes the behaviour of the microprocessor. The state function generates a future state by repeatedly applying a next state function. There are five instructions: add, branch, load, store and set. Notice that we only use five of eight opcodes, and we really should have some 'exception' behaviour for the others in case a program accidentally includes them. However, we omit this here. Notice also that we must be careful to include the appropriate number of leading zeros when defining constants: the length of a bit string is used to determine its [sub] sort, so getting this wrong leads to errors.
*** *** SPM *** *** This is the "main" function, where we define the *** state funtion spm and the next-state function next. *** fmod SPM is protecting SPM-STATE . *** A few handy constants.. ops ADD, BR, LD, ST, SET : -> OpField . op ZERO : -> Word . op One : -> Address . *** State function op spm : Int SPMstate -> SPMstate . *** Next-state function op next : SPMstate -> SPMstate . *** Convert an address to a word op Address2Word : Address -> Word . var SPM : SPMstate . var T : Int . var MP MD : Mem . var PC : Address . var REG : Reg . var A : Address . *** Define opcodes etc. eq ADD = 0 0 0 . eq BR = 0 0 1 . eq LD = 0 1 0 . eq ST = 0 1 1 . eq SET = 1 0 0 . eq ZERO = 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 . eq One = 0 0 0 0 0 0 0 0 0 1 . *** Pad an address with leading zeros to become *** a word eq Address2Word(A) = 0 0 0 0 0 0 A . *** Formally, the state function is an Iterated Map *** Primitive recursive definition - repeatedly apply *** the state function eq spm(0,SPM) = SPM . eq spm(T,SPM) = next(spm(T - 1,SPM)) [owise] . *** Addition (opcode = 0) ceq next(MP,MD,PC,REG) = (MP, MD, PC + One, REG[REG[rega(MP[PC])] + REG[regb(MP[PC])] / regc(MP[PC])]) if opcode(MP[PC]) == ADD . *** [Taken] branch (opcode = 1, REG[0 0 0] = 0) ceq next(MP,MD,PC,REG) = (MP, MD, PC + address(MP[PC]), REG) if opcode(MP[PC]) == BR and REG[0 0 0] == ZERO . *** [Not-taken] branch (opcode = 1, REG[0 0 0] =/= 0) ceq next(MP,MD,PC,REG) = (MP, MD, PC + One, REG) if opcode(MP[PC]) == BR and REG[0 0 0] =/= ZERO . *** Load (opcode = 10) ceq next(MP,MD,PC,REG) = (MP, MD, PC + One, REG[MD[address(MP[PC])] / rega(MP[PC])]) if opcode(MP[PC]) == LD . *** Store (opcode = 11) ceq next(MP,MD,PC,REG) = (MP, MD[REG[rega(MP[PC])] / address(MP[PC])], PC + One, REG) if opcode(MP[PC]) == ST . *** Set (opcode = 100) ceq next(MP,MD,PC,REG) = (MP, MD, PC + One, REG[Address2Word(value(MP[PC])) / rega(MP[PC])]) if opcode(MP[PC]) == SET . endfm
Now we get to the final module, which defines a very simple program with two instructions. After the module, we actually run the program.
*** *** The final module is to define an actual program and *** run it. We will just define a two instruction *** program. *** fmod RUNPROGS is protecting SPM . ops Md Mp : -> Mem . *** Define memories as *** *constants*, *** NOT *variables* op Rg : -> Reg . *** Same for registers... op Pc : -> Word . *** ... and program counter *** Now specify a starting state... *** Notice that programming is a bit of a pain... *** Program counter will start at zero eq Pc = 0 0 0 0 0 0 0 0 0 0 . *** Register 1 contains 3 eq Rg[0 0 1] = 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 1 . *** Register 2 contains 6 eq Rg[0 1 0] = 0 0 0 0 0 0 0 0 0 0 0 0 0 1 1 0 . *** Add R1 to R2 storing in R3 eq Mp[0 0 0 0 0 0 0 0 0 0] = 0 0 0 0 0 1 0 1 0 0 1 1 0 0 0 0 . *** Store R3 in memory loc. 1 eq Mp[0 0 0 0 0 0 0 0 0 1] = 0 1 1 0 1 1 0 0 0 0 0 0 0 0 0 1 . endfm *** *** Now run the program *** *** First reduction shows state after running just *** one instruction (the add) reduce spm(1, (Mp,Md,Pc,Rg)) . *** Second reduction shows state after running both *** instructions (add and store) reduce spm(2, (Mp,Md,Pc,Rg)) .
The actual results of running this 'program' is shown below.
========================================== reduce in RUNPROGS : spm(1, Mp,Md,Pc,Rg) . rewrites: 353 in -10ms cpu (0ms real) (~ rewrites/second) result SPMstate: Mp,Md,0 0 0 0 0 0 0 0 0 1,(Rg[0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 1 / 0 1 1]) ========================================== reduce in RUNPROGS : spm(2, Mp,Md,Pc,Rg) . rewrites: 948 in -10ms cpu (0ms real) (~ rewrites/second) result SPMstate: Mp,Md[0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 1 / 0 0 0 0 0 0 0 0 0 1],0 0 0 0 0 0 0 0 1 0,(Rg[0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 1 / 0 1 1])
This says that after one cycle, and hence one instruction, the contents of the program and data memories are unchanged; the program counter is now 1; and register 3 (0 1 1) has been overwritten with value 9 (ie. 3 + 6). After the second cycle, and hence two instructions, the program memory is still unchanged, but now the data memory has had value 9 written to memory address 1; and the program counter is now 2.
Previous Contents Next