For the main coursework you will have to write a Maude description of a Microprocessor - so in this chapter, we will look at exactly how we go about doing that.
When we modelled simple hardware examples, we treated them as stream transformers - devices that map input streams to output streams: we did not consider their internal state at all. However, the usual approach to modelling microprocessors is different. While, in principle, we could do the same with microprocessors - they are just chips with inputs and outputs - we do not for a number of reasons.
The net result of these things is that it is usual to model microprocessor behaviour as state evolution over time. That is, a microprocessor has some starting state - which will include the representation of some program(s) and data - and that state changes over time, in response to the execution of the program(s) and the given data. (Real microprocessors may well have input as well as the initial state - we will not worry about that for now.).
Although it may be self-evident to you what state is, past experience tells me that not everyone thinks the same. So if you are not clear about state, here are some examples that hopefully will help.
We are going to be modelling the behaviour of microprocessors at the lowest level visible to a programmer - the machine language level. For us, state is going to be the collective contents of all the memory, registers and so on that are visible to the machine language programmer.
Clearly it is not enough to possess state - that state must change or evolve. It does this over time. Just as with the hardware examples, we must introduce some notion of time - and we will choose to use the same one. That is, we divide time up into clock cycles, and label each one with a natural number. How long should each clock cycle last? It depends on exactly what we are interested in modelling.
For instance, consider again the traffic light example. If we are simply interested in the cycle of changes, we might very well choose to make each clock cycle last as long as each light phase. That is, the first clock cycle might last for the R phase, the next for the RY phase, and so on. In all but the most unusual sets of traffic lights, this would mean that clock cycles would vary in length. We are quite happy to let that happen. Alternatively, you might actually be interested in how long each phase of the lights lasted. In that case, you are better off making each clock cycle last a fixed period of time (say, 1 second).
We are going to choose to make each clock cycle last for as long as it takes to execute a single machine instruction - which will generally be a variable period of time, since very few microprocessors possess instruction sets where every instruction lasts the same amount of time.
(There are quite interesting philosophical discussions to be had about this: Do events occur in time; or is time defined by the presence of events? I tend to prefer the latter, after I was convinced by my first PhD student.)
Before we get on to some small illustrative examples, we will explain how to model microprocessors. Typically, we will represent the state by some set A. The set A will, in realistic examples, be quite complex - a Cartesian product of individual state elements, each respresenting registers, memory and so on. When we look at actual examples, we will have to consider the structure of A - but for now, we will just assume it is some arbitrary set. We also need a set representing time. Strictly speaking, when we write specifications down mathematically, we define a special set T which is a copy of the natural numbers. However, as before we will 'cheat' and use the built-in Int sort.
We will model microprocessors as iterated maps: functions that take two arguments. The first is the number of clock cycles we wish to run the machine for; and the second is the initial state of the system. Iterated map functions are defined in terms of a next-state function that map the state of the system at one clock cycle to the state at the next clock cycle.
op F : Int A -> A . op next : A -> A . var t : Int . var a : A . eq F(0,a) = a . eq F(t + 1, a) = next(F(t, a)) .
That is, if we run a system F for zero clock cycles starting in initial state a, we remain in state a; if we run F for t+1 cycles starting in initial state a, then the final state will be equal to the result of the next-state function next applied to the state of F at the previous time t. For example, suppose we wish to calculate F(5,a):
F(5,a) = next(F(4,a)) = next(next(F(3,a))) = next(next(next(F(2,a)))) = next(next(next(next(F(1,a))))) = next(next(next(next(next(F(0,a)))))) = next(next(next(next(next(a)))))
Basically, we just apply the next-state function t times to the initial state a to calculate the state at time t. Unfortunately, as we saw before, Maude does not properly handle equations with t + 1 on the left hand side, so we have to rewrite them:
op F : Int A -> A . op next : A -> A . var t : Int . var a : A . eq F(0,a) = a . eq F(t, a) = next(F(t - 1, a)) if t > 0 [owise] .
The tricky part, of course, is deciding (1) exactly what is A; and (b) exactly how do we define next? Both depend on the actual example in question, and potentially can become very complex (particularly next). However, we will start off with a very simple example. The Fibonacci numbers are defined as follows.
fib(0) = fib(1) = 1 fib(n + 2) = fib(n + 1) + fib(n)
The simplest way to define the Fibonacci numbers in Maude is something like this:
fmod FIB is protecting INT . op fib : Int -> Int . var N : Int . eq fib(0) = 1 . eq fib(1) = 1 . eq fib(N) = fib(N - 1) + fib(N - 2) [owise] . endfm
However, we will - for the purpose of illustrating iterated maps - define it like this.
fmod FIB is protecting INT . sort Fib . op _,_ : Int Int -> Fib . op F : Int Fib -> Fib . op next : Fib -> Fib . vars T M N : Int . eq F(0,M,N) = (M,N) . eq F(T,M,N) = next(F(T - 1,M,N)) [owise] . eq next(M,N) = (N,M + N) . endfm
The state Fib in this case is a pair of Ints, and we define Fib as a tuple; the second two define the iterated map F. Look carefully at them and you can see that they are essentially the same as the ones we saw above. The final equation defines the next-state function next. Notice that the state at any one time consists of the last two Fibonacci numbers. As an exercise, try evaluating F with a variety of starting states and times. For example, try
*** Run for 1 cycle starting at 1,1 - should be 1,2 red F(1,1,1) . *** Run for 3 cycles starting at 1,1 - should be 3,5 red F(3,1,1) . *** Run for 3 cycles starting at 3,5 - should be 13,21 red F(3,3,5) .
One problem with our Fibonacci iterated map is that it only works properly if the initial state consists of a pair of consecutive Fibonacci numbers M and N, with M<N or M=N=1. We could change our definition of the value of an iterated map at time zero to:
eq F(0,a) = init(a) .
This is effectively what we do in an alternative version of FIB - by forcing M and N to both be one initially, regardless of what values the user set.
fmod FIB is protecting INT . sort Fib . op _,_ : Int Int -> Fib . op F : Int Fib -> Fib . op next : Fib -> Fib . vars T M N : Int . eq F(0,M,N) = (1,1) . eq F(T,M,N) = next(F(T - 1,M,N)) [owise] . eq next(M,N) = (N,M + N) . endfm
Of course the new version is arguably less flexible because it can only start with 1,1. It would be better to define an initialization function that first checked to see if the user-supplied arguments were a legal pair of Fibonacci numbers, and if so left them alone. Only if they were not should it set them to 1,1. As an exercise, modify F to do that - a module defining an operation that checks if two numbers are an appropriate pair of Fibonacci numbers can be found here.
The details and advantages of using initialization functions is beyond this module. However, carefully-chosen initialization functions that only make changes to initial states that are somehow 'wrong' are an important aspect of some automated verification techniques.
Since we mentioned traffic lights above, here is an example based on them.
fmod TRAFFIC is protecting INT . sort Light . op Red : -> Light . op Green : -> Light . op Yellow : -> Light . op RedYellow : -> Light . op TRAFFIC : Int Light -> Light . op next : Light -> Light . var t : Int . var l : Light . eq TRAFFIC(0, l) = l . ceq TRAFFIC(t, l) = next(TRAFFIC(t - 1, l)) if t > 0 . eq next(Green) = Yellow . eq next(Yellow) = Red . eq next(Red) = RedYellow . eq next(RedYellow) = Green . endfm
An example reduction would be
red TRAFFIC(4,Green) .
That is, what is the state of the light four light-changes after it is red? It should be Green again:
Green -> Yellow -> Red -> RedYellow -> Green
In the next chapter we will look at a simple microprocessor example. However, before that, we will outline the typical structure.