Since the main coursework for this module will be to specify a microprocessor, we will 'get in the mood' with some simple hardware examples. However, we need to deal with some preliminary concepts first.
Hardware systems tend to deal with streams of data: that is, time-separated data send down some form of channel. This chanel is typically a wire, or a collection of wires, or some other physical (or wireless) communication path. And time-separated commonly means that data is controlled by a clock. A clock is essentially just a way of dividing up time - any given instant of time will be part of one particular clock cycle. In typical systems, clock cycles are defined by a signal that repeatedly alternates between true and false (or 0 and 1, or between two different voltages - it depends on your point of view). Hence a clock cycle begins (typically) when the signal changes from false to true, and ends when it next changes from false to true. There is hardware that works differently to this (and streams of data also appear as a concept in software). However, for our purposes, this is sufficient. We will be dealing with some simple hardware examples in this chapter that will accept one or more input streams as parameters, and generate one or more output streams as results. Time for both the hardware and the streams is controlled by some kind of global clock. Note that because our hardware examples take input streams and 'transform' them into output streams, we commonly call them stream transformers.
Before we actually write some examples down, we must decide how we are going to represent, or model, these various concepts: clocks, streams, and stream transformers.
It might seem that the obvious choice is a sequence of Booleans (true, false, true, false,...) - however, this is not convenient.
We need to be able to identify times - usually relative to the current time. That is, we want to be able to say things like 'the time before the current time'. We are sometimes interested in identifying a particular time: especially, the first time. The easiest way to do this is simply to use a copy of the natural numbers Nat, and label each clock cycle with one. So the first time is time zero, then time one, and so on. given some value t representing the current clock cycle, we can easily check if it is the first clock cycle (does t=0?), and we can easily compute relative times (for example, the 'time before' is just t-1).
Although convenient, there are two important differences with 'real' clock cycles. Firstly, real clock cycles do not have numbers - in practice, this does not concern us. Secondly, our clock cycles need not be as concrete as real clock cycles. The cycles in a real clock are almost always all the same length. Ours can be more abstract - we can make some longer than others if it is convenient (and it is - for the coursework). We will return to this when we start to deal with microprocessors.
Given we have decided to model time with the natural numbers, how do we model streams? There is much argument about this in general: for various good reasons, some people prefer quite complex mathematical models of streams. We do not however - for us a stream is a simple function from time to data. That is, suppose we wish to represent a particular stream b of Booleans. We do this with the function
b : Nat -> Bool .
Then b(0) is the Boolean on stream b at time 0; b(1) at time 1; and (in general) b(t) at time t.
Note that we said particular stream - if we wish to represent streams in general (and we do), then the notation is slightly more complex. First, we need to introduce a sort of streams - in fact, one for every sort of stream we need. For example:
sort BoolStr .
Then we need to introduce a function that will evaluate a stream. That is, given a stream b and a time t, it will tell us what is on the stream at the particular time.
op eval : BoolStr Int -> Bool .
There are a couple of fairly subtle and tricky points here.
We have changed the 'type' representing time from Nat to Int. We have done this for two reasons. First, because although Nat is available in Maude, it is simply notationally inconvenient - we would have to write 's(s(...s(0)...))' all the time (or introduce abbreviating constants - better but still irritating) instead of '1', '2' etc. Secondly, and more controversially, we will often wish to write things like
if f(T - 1) and (T > 0)
That is, check if some function of T - 1 holds but only when T > 0. In this case, if we used Nat and T = 0, we would run into possible problems because of course there is no 'minus one' in Nat. We could always rewrite our equations to avoid it, but it would be more complex and harder to read, so we will 'cheat' and use Int instead. The only problem is that we must be a bit careful to avoid 'negative times' (not a problem with Nat because they don't exist).
The second point is: why bother with eval, which means we must write eval(b,t) everytime we want to know what is on b at time t, instead of b(t)?
Actually, we don't need to write 'eval(b,t)' because we can define ourselves a mixfix operator which looks like our original version:
_(_) : BoolStr Int -> Bool .
So we can just write b(t) as before. Problem solved - except we must remember to define the _(_) operators.
Given we can define streams, stream transformers are just operators that take input streams and generate output streams. For example, consider a stream AND gate - which accepts two Booleans every clock cycle and outputs the AND of them every clock cycle:
op And-Stream : BoolStr BoolStr -> BoolStr .
But there is a problem: how do we define it using equations? You might at first thought think like this:
eq And-Stream(a,b) = a and b . ***WRONG!!!
But you would be wrong - because a and b are not Booleans but streams of Booleans. The built-in and operator only deals with Booleans, so this will not parse. What we need is a version of and that will work on streams - but that is just what And-Stream is supposed to be! Note that the intended meaning might seem 'obvious' - in fact I confidently predict that several of you will be so convinced of this that you will write something very similar in the exam - but remember that mis-interpreting things that are alledgedly 'obvious' is arguably where we came in, and why we are doing all this in the first place.
So what do we do? We could dream up and implement all sorts of clever (and hard to read) notation for 'stream operators' - but we won't. Instead of trying to define the whole output stream, we will try to define the output at a particular time:
eq And-Stream(a,b)(t) = a(t) and b(t) .
(Note there is a technical point here about operator precedence and parsing - but we will get back to that later.) What we have done is realised that And-Stream(a,b) is just a Boolean stream, and hence our _(_) evaluation operator can be applied to it: And-Stream(a,b)(t) is the value of And-Stream(a,b) at time t - which is just a Boolean. Hence all we need to do is work out the (Boolean) value of And-Stream(a,b)(t). To do that, we take the values on streams a and b at time t (a(t) and b(t) respectively) - which are both Booleans - and just 'and' them.
eq And-Stream(a,b)(t) = a(t) and b(t) .
Another issue is to do with delay. It is very common for hardware systems to take one (or more) complete clock cycles to compute results. That is, the results emerging at time t are the result of inputs that arrive at time t - 1 - which raises the question, what happens at time zero? There are two possibilities - either we care (and need to put in equations to say so), or (more likely) we don't. In that case, what do we output? One answer is nothing - that is, the output (and hence the function computing it) is undefined. This is mathematically fine (such functions are called partial) but complicated - we would prefer all our functions to be total, and hence we must output something. Generally, we define a special constant to represent unspecified. For example:
op U : -> Int .
There are two important points to make.
Now we are finally in a position to look at some examples.
A multiplexor (usually abreviated to MUX) is a simple piece of hardware that selects one of a number of inputs and directs it to a (single) output, depending on the value of a separate control input. The very simplest version uses a single Boolean stream to choose between two (Boolean) inputs. The source is here.
fmod MUX is protecting INT . sort BoolStr . op _(_) : BoolStr Int -> Bool . op mux : BoolStr BoolStr BoolStr -> BoolStr . vars X Y B : BoolStr . var T : Int . ceq mux(X,Y,B)(T) = X(T) if B(T) == true . ceq mux(X,Y,B)(T) = Y(T) if B(T) == false . endfm fmod MUX-RUN is protecting MUX . ops a b c : -> BoolStr . *** a and b are data streams eq a(0) = true . eq a(1) = false . eq a(2) = true . eq a(3) = false . eq b(0) = false . eq b(1) = true . eq b(2) = false . eq b(3) = true . *** c is the control stream eq c(0) = true . eq c(1) = true . eq c(2) = false . eq c(3) = false . endfm *** value at time 0 - should be true red mux(a,b,c)(0) . *** value at time 1 - should be false red mux(a,b,c)(1) . *** value at time 2 - should be false red mux(a,b,c)(2) . *** value at time 3 - should be true red mux(a,b,c)(3) .
The second module MUX-RUN simply defines a number of constant streams so we can do some example reductions. The first module MUX is the important one.
An inner product step processor (IPS) is commonly found in signal processing hardware. There will generally be many of them in either a one-dimensional or two-dimensional array, in various configurations: we will see a simple one-dimensional array in a later chapter on correctness. An IPS has three input streams A, B and C, and three output streams A', B' and C'. A' and B' are simply copies of A and B, delayed by one clock cycle. Stream C' is A*B+C, again delayed by one clock cycle. The actual datatypes involved vary from case to case - integers are common, which is what we will use.
There are two points to consider. First, we must use unspecified elements because of the delay. The second is that IPS is a function that takes three arguments and returns three results. We would like to write something like:
op ips : IntStr IntStr IntStr -> IntStr IntStr IntStr .
but we can't - Maude does not allow this syntax. Like most programming languages, only a single return value is permitted. So we must not only define streams of integers, but also streams of triples of integers. The code for IPS can be found here.
fmod IPS is protecting INT . sort IntStr . sort IPSTuple . sort IPSstr . op _(_) : IPSstr Int -> IPSTuple [prec 1] . op _(_) : IntStr Int -> Int [prec 1] . op U : -> Int . op _,_,_ : Int Int Int -> IPSTuple . op _,_,_ : IntStr IntStr IntStr -> IPSstr . op ips : IPSstr -> IPSstr . vars A B C : IntStr . var T : Int . eq ips(A,B,C)(0) = (U,U,U) . ***eq ips(A,B,C)(T + 1) = (A(T),B(T), *** A(T) * B(T) + C(T)) . eq ips(A,B,C)(T) = (A(T - 1),B(T - 1 ), A(T - 1) * B(T - 1) + C(T - 1)) [owise] . endfm fmod IPS-RUN is protecting IPS . op a : -> IntStr . op b : -> IntStr . op c : -> IntStr . eq a(0) = 1 . eq a(1) = 2 . eq a(2) = 3 . eq b(0) = 4 . eq b(1) = 5 . eq b(2) = 6 . eq c(0) = 6 . eq c(1) = 7 . eq c(2) = 8 . endfm red ips(a,b,c)(0) . red ips(a,b,c)(1) . red ips(a,b,c)(2) . red ips(a,b,c)(3) .
As with MUX the second module just defines some constant streams for the example reductions.
The shift register has two input streams: one data, and one control. The shift register reads in an element of the data stream whenever a true element appears on the control stream. When the control stream is false, the currently-stored value is retained (assuming there is one - until a true element appears on the control stream, the shift register outputs U). As with IPS, there is a one-cycle delay in computing the output of SR. The code can be found here.
fmod SR is protecting INT . sorts IntStr BoolStr . op U : -> Int . op _(_) : IntStr Int -> Int . op _(_) : BoolStr Int -> Bool . op SR : IntStr BoolStr -> IntStr . op delta : BoolStr Int -> Int . op beenTrue : BoolStr Int -> Bool . var D : IntStr . var C : BoolStr . var T : Int . eq SR(D,C)(0) = U . ceq SR(D,C)(T) = U if not beenTrue(C,T - 1) and (T > 0) . ceq SR(D,C)(T) = D(delta(C,T - 1)) if beenTrue(C,T - 1) and (T > 0) . eq beenTrue(C,0) = C(0) . ceq beenTrue(C,T) = true if (C(T) == true) and (T > 0) . ceq beenTrue(C,T) = beenTrue(C,T - 1) if (C(T) == false) and (T > 0) . ceq delta(C,0)= 0 if C(0) == true . ceq delta(C,T) = T if (C(T) == true) and (T > 0) . ceq delta(C,T) = delta(C, T - 1) if (C(T) == false) and (T > 0) . endfm fmod SR-RUN is protecting SR . op d : -> IntStr . op c : -> BoolStr . eq d(0) = 0 . eq d(1) = 1 . eq d(2) = 2 . eq d(3) = 3 . eq d(4) = 4 . eq c(0) = false . eq c(1) = false . eq c(2) = true . eq c(3) = false . eq c(4) = true . endfm red SR(d,c)(0) . red SR(d,c)(1) . red SR(d,c)(2) . red SR(d,c)(3) . red SR(d,c)(4) . red SR(d,c)(5) .
As before, the second module is purely for the example reductions.
As an aside, notice that because beenTrue and delta are so similar, we can actually use delta instead of beenTrue - provided we add an equation defining delta when C(0) is false. The complete code is here: below is the SR module.
fmod SR is protecting INT . sorts IntStr BoolStr . op U : -> Int . op _(_) : IntStr Int -> Int . op _(_) : BoolStr Int -> Bool . op SR : IntStr BoolStr -> IntStr . op delta : BoolStr Int -> Int . var D : IntStr . var C : BoolStr . var T : Int . eq SR(D,C)(0) = U . ceq SR(D,C)(T) = U if (delta(C,T - 1) == U) and (T > 0) . ceq SR(D,C)(T) = D(delta(C,T - 1)) if (delta(C,T - 1) =/= U) and (T > 0) . ceq delta(C,0) = U if C(0) == false . ceq delta(C,0)= 0 if C(0) == true . ceq delta(C,T) = T if (C(T) == true) and (T > 0) . ceq delta(C,T) = delta(C, T - 1) if (C(T) == false) and (T > 0) . endfm
(I'm not sure which version I prefer.) In the next chapter we will look at some more advanced features of Maude.