[Next] [Up] [Previous]

A three-way arbiter

Now let's try to apply the same idea to a three-way bus arbiter. In this version, we will have one latched bit for each requester. This bit holds a one when the corresponding requester was granted the bus on the previous cycle. We'll still use a fixed priority scheme, but if a given request was granted on the previous cycle, we'll give it lowest priority on the current cycle. Thus, if the bit for a given requester is set, its request is served only if no others are requesting. Further, the requester with its bit set does not inhibit lower priority requesters. Here is one attempt at such an arbiter:

module main(req1,req2,req3,ack1,ack2,ack3)
{
  input req1,req2,req3 : boolean;
  output ack1,ack2,ack3 : boolean;
  
  bit1,bit2,bit3 : boolean;

  next(bit1) := ack1;
  ack1 := req1 & (bit1 ? ~(req2 | req3) : 1);

  next(bit2) := ack2;
  ack2 := req2 & (bit2 ? ~(req1 | req3) : ~(req1 & ~ bit1));

  next(bit3) := ack3;
  ack3 := req3 & (bit3 ? ~(req2 | req3) :
                            ~(req2 & ~bit2 | req1 & ~bit1));
}

The specifications for the three-way arbiter are as follows:

  mutex : assert G ~(ack1 & ack2 | ack1 & ack3 | ack2 & ack3);
  serve : assert G ((req1 | req2 | req3) -> (ack1 | ack2 | ack3));
  waste1 : assert G (ack1 -> req1);
  waste2 : assert G (ack2 -> req2);
  waste3 : assert G (ack3 -> req3);

  no_starve1 : assert G F (~req1 | ack1);
  no_starve2 : assert G F (~req2 | ack2);
  no_starve3 : assert G F (~req3 | ack3);

They are similar to the two-way case, but note that in mutex we consider all pairs. Also, we've specified non-starvation for all of the requesters, just in case. Save this program in a file (you can put the specifications anywhere inside the module declaration - statement order is irrelevant in SMV). Then open the file and choose ``Verify all''. You should get a false result for no_starve3. Click on no_starve3 and observe the counterexample trace. This is an example of a ``livelock''. The last two states in the counterexample repeat forever. Notice that requesters 1 and 2 are served alternately while requester 3 starves.

In fact, there is another error in the design. If you select the serve property and try to verify it, you'll find that serve can be false in the initial state. This occurs if more than one of the bits are true initially. We could rule this out by specifying initial values for these bits, as follows:

  init(bit1) := 0;
  init(bit2) := 0;
  init(bit3) := 0;

Alternatively, if we don't care if no one gets served in the initial state, we can change the specification. In temporal logic X p means that p is true at the ``next'' time. Thus, for example X G p means that p holds from the second state onward. Thus, we could change the specification to:

  serve : assert X G ((req1 | req2 | req3) -> (ack1 | ack2 | ack3));

As an exercise, you might want to try designing and verifying a three-way arbiter that satisfies all the specifications above.

[Next] [Up] [Previous]