So far, we have been exclusively concerned with specification - not that suprising since it is in the module title. However, in this chapter we will consider the following: What does it mean for an implementation of a specification to be correct? In order to answer that, we must first define what it means for something to be correct, and then build (some representation of) an implementation to compare with a specification. That is what we will do in this chapter - first we will write down the specification and implementation of a simple piece of hardware (a convolver). Next we will consider what it means for an implementation to be correct with respect to a specification. Finally we will formally define the correctness of the implementation with respect to the specification. We will not actually prove the implementation correct as that would be a bit beyond the scope of this module.
A convolver is a piece of hardware that computes the convolution function. This function is widely used in signal processing applications (for example, you might find convolution hardware in a mobile phone). A convolver reads an input stream of signals (we will assume they are integers) and operates on the last n elements of the stream. It multiplies each stream element with a (normally fixed) weight. The output is the sum of these products. Semi-formally:
conv(t+n+k) = w1.x(t) + w2.x(t+1) + ... + wn.x(t+n-1)
where w1,w2,...,wn are the fixed weights, and x(i), for i=t,...,t+n-1 are the elements of the input stream. Note that we need to wait at least n cycles for enough elements of input stream x to have been read in before an output can be produced. We also introduce an arbitrary positive constant k to recognize the fact that any hardware we build may require extra time to actually produce a result.
Here is the convolver specification in Maude for n=4 and k=0. You can download it here together with some sample values for the weights and the input streams, and some sample reductions.
*** Convolver specification with n=4 and k=0 fmod CONV-SPEC is protecting INT . sort IntStr . op _(_) : IntStr Int -> Int [prec 1] . op U : -> Int . ops W1 W2 W3 W4 : -> Int . *** n=4 in this example op convSpec : IntStr -> IntStr . vars X : IntStr . var T : Int . *** Output is U if we have not read in enough inputs ceq convSpec(X)(T) = U if T < 4 . *** Otherwise compute convolution eq convSpec(X)(T) = W1 * X(T - 3) + W2 * X(T - 2) + W3 * X(T - 1) + W4 * X(T) [owise] . endfm
If you want to get an idea about what the convolver does, consider the example reductions in the file containing the code. We have restricted the values of the integers for the weights and stream elements to be 1 or -1. The result of this is that the output of the convolver alternates between 4 and -4 (once the U elements have been output):
Weights: 1 -1 1 -1 Convolution = 4 Stream: 1 -1 1 -1 Weights: 1 -1 1 -1 Convolution = -4 Stream: -1 1 -1 1
That is, when the values of all the weights match the corresponding stream elements, then the output is 4, and when they all do not match, the output is -4. The convolver is pattern matching between the weights and the input stream. It is also possible for there to be partial matches:
*** Three matches Weights: 1 -1 1 -1 Convolution = 2 Stream: 1 1 1 -1 *** Two matches Weights: 1 -1 1 -1 Convolution = 0 Stream: 1 1 -1 -1 *** One match Weights: 1 -1 1 -1 Convolution = -2 Stream: 1 1 -1 1
Higher positive numbers indicate greater similarity between the input stream and the weights. It is usual in this case to use 1 and 0 instead of 1 and -1, and replace the multiplication operator with equality.
There are many ways we could choose to implement the convolver, but the usual way is to use an Inner Product Step Processor (IPS) which we have already seen. Recall that each IPS has three inputs A, B and C, and three outputs A', B' and C'. In the case of the convolver, the output A' is not needed:
To make a complete convolver, we need to chain together IPS processors, linking the B/B' and C/C' inputs and outputs.
To see how the convolver works in practice, consider the example shown in figure 3. This shows the operation of the convolver over four cycles. Notice that in order to get the convolver to work properly, we need to insert dummy don't care values between each input stream element, represented by '*'. Unknown output values are represented by '?'. (In practice, we could interleave two different convolution computations.)
In the example shown, the first convolution result emerges on the final cycle (W4.x(3)+W3.x(2)+W2.x(1)+W1.x(0)). This is followed by an unknown value, which in turn is followed by the next convolution result, which is in the process of being computed.
We are going to build a Maude representation of the IPS-based convolver. We are going to do this by composing together four IPS units. Note that there are, unfortunately, some complications.
You can download all of the code here. Here is the first module.
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 . *** Think of this as a next-state function op ips : IPSTuple -> IPSTuple . vars A B C : Int . var T : Int . *** Equations for the IPS next-state function ceq ips(A,B,C) = (U,U,U) if (A == U) or (B == U) or (C == U) . eq ips(A,B,C) = (A, B, A * B + C) [owise] . endfm
This is basically a simplified version of our previous ISP example.Here is the module defining the actual convolver.
fmod CONV-IMP is protecting IPS . sort ConvState . op _,_,_,_ : IPSTuple IPSTuple IPSTuple IPSTuple -> ConvState . op convImp : Int IntStr -> ConvState . ops conv1 conv2 conv3 conv4 : Int IntStr -> IPSTuple . ops W4 W3 W2 W1 : -> Int . op C : IPSTuple -> Int . var X : IntStr . var T : Int . vars I J K : Int . eq W1 = 1 . eq W2 = -1 . eq W3 = 1 . eq W4 = -1 . eq C(I,J,K) = K . eq convImp(T,X) = (conv1(T,X), conv2(T,X), conv3(T,X), conv4(T,X)) . eq conv1(T,X) = ips(W1,X(T - 3),0) . eq conv2(T,X) = ips(W2,X(T - 2), C(conv1(T - 1, X))) . eq conv3(T,X) = ips(W3,X(T - 1), C(conv2(T - 1, X))) . eq conv4(T,X) = ips(W4,X(T), C(conv3(T - 1, X))) . endfm
We have had to introduce a new sort representing the state of the whole convolver (ConvState). We have defined the implementation convImp in terms of four subfunctions conv1 to conv4, each representing one of the ISPs. Refering back to figure 3, conv1 is the right-most ISP, and conv4 is the left-most ISP (from which the result will emerge). The actual code file contains a further module defining a sample stream. Note it only makes sense to reduce convImp for even times. So
reduce convImp(8,x) .
makes sense but
reduce convImp(13,x) .
does not. This is because just as we must alternate don't care values on the inputs, so every other output value is meaningless. If we do a reduction (say reduce convImp(8,x) .) we get:
reduce in CONV-IMP-RUN : convImp(8, x) . rewrites: 182 in 0ms cpu (0ms real) (~ rewrites/second) result ConvState: U,U,U,-1,-1,2,U,U,U,-1,1,-4
The result is the twelve integers making up the state of the convolver: the first three are A, B and C from conv1 and so on. The value we are interested in is C from conv4 - conveniently this is the right-most value (i.e. 4).
We want to claim that convImp actually implements convSpec, but there are difficulties. First, the output of convSpec is a single integer not a tuple of 12; second, the timing behaviour is different in both cases. Although in this case it is pretty obvious what to do (for example, reduce convSpec(x)(4) should be -4 and luckily it is) we need to come up with some formal rules and principles if we are going to be able to do any proofs (note that we are not going to actually do any proofs here). The issue of the different data representation will be handled by a data abstraction map and the different time by a timing abstraction map. Having done that, we still need to model correctness.
Essentially, we need to construct a function that maps one state to the other. The first question to ask is: should the function map the implementation state to the specification state, or the other way around. For reasons that will (hopefully) become clearer later, we need to construct a function that maps the implementation state to the specification state.
op dataAbs : ImplementationState -> SpecificationState .
the next problem is how do we actually construct the function? Look at the implementation and specification of the convolver: the specification state value is also present in the implementation state (the last of the 12 integers). We just need to define a function that discards all the implementation state elements that are not present in the specification.
eq dataAbs(A1,A2,A3,A4,A5,A6,A7,A8,A9,A10,A11,A12) = (A12) .
In general, this is how most data abstraction functions are defined (they get a bit more complicated with pipelined and superscalar microprocessors).
For reasons we won't bother to go into here, data abstraction maps must be surjective: that is, at least one implementation state must map to every specification state.
Time abstraction is a little more complex - though many of the issues involved are similar. Each specification clock cycle lasts for one or more implementation clock cycles. (In our case, each specification clock cycle lasts for two implemenation clock cycles.) Like data abstraction functions, time abstraction functions must be surjective - if they are not, then clock cycles in the specification will be 'missed out' in the implementation. However, in addition, time abstraction functions must be monotonic. Formally, a function f is monotonic if:
if a >= b, then f(a) >= f(b)
We require time abstraction functions to be monotonic because otherwise the time in the specification could 'go backwards'.
The time abstraction functions we use are called Retimings: surjective and monotonic functions that map the implementation clock to the specification clock. We generally denote the set of all retimings (i.e. surjective and monotonic functions) from an implementation clock S to a specification clock T by
Ret(S,T)
In practice, retimings can depend not only on the implementation clock time, but also the actual initial state of the implementation. However, that is not the case here. An example retiming is shown in fig 4.
This diagram is typical of retimings: at least one ret arrow maps to each cycle of specification clock T (surjective); and the arrows do not cross (monotonic).
We can define retimings in a variety of ways - but we must ensure that they are always surjective and monotonic. In our case, the definition is trivial:
eq ret(S) = S quo 2 .
where quo is integer division. That is, time in the specification and implementation are related as follows:
Specification time: 0 1 2 3 4 5 ... Implementation time: 0 1 2 3 4 5 6 7 8 9 10 ...
So to find out what the implementation should be doing at time 4, look at specification time 2.
Having defined a data abstraction map and a retiming, we now need to actually build our correctness model. We also need to take care of the issue of mapping the input streams and outputs between specification and implementation
The simplest way to explain the correctness model is in terms of a commutative diagram - such as that shown in fig 5.
Suppose we start with some implementation state b that is 'legal' that we propose to run for some number s of implementation clock cycles (cycles of clock S). The commutative diagram says that for an implementation to be correct with respect to a specification, we should be able to follow both paths from the bottom left-hand corner of the diagram, and end up in the same state at the top right-hand corner. That is, we can choose to do one of the following.
If the implementation is correct, then the resulting specification state should be the same in both cases. There are just two issues to address.
Obviously we need to map the commutative diagram to Maude:
Specification(ret(s),dataAbs(b)) == dataAbs(Implemenation(s,b))
We will not undertake any verification in this chapter - it is too complex. In practice, the convolver is simple enough to be manually proved correct. However, realistic examples require machine proofs. This typically involves theorem proving software. Theorem provers partially automate the proof process. Maude is not actually a theorem prover, but one can be implemented in it using meta-level code (beyond the scope of this module).