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

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 `bit`s 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.