Assertion based Verification of a Round Robin Arbiter

Description: A common problem with any design is access to a shared resource by multiple agents. An arbiter design is used to ensure that only one agent has access to the shared resource at any given time. A common example of the need of arbiter is in a multiprocessor memory design where multiple processors needs to access memory using a shared bus. There are different arbitration techniques used in design of arbiter based on different requirements and round robin arbiter is one of the commonly used arbitration mechanism that ensures fairness.
A round robin arbitration policy is a token passing scheme where fairness among the multiple requesting agents is ensured with no starvation. In each cycle, one of the master has the highest priority to get access to the shared resource. This is then rotated in a round robin order. If any master does not need access to the resource in the cycle, then the next master in round robin order gets the priority.
Following diagram shows the block diagram of an arbiter that controls 4 requesting agents and generates 4 grants to each of the agent in a round robin order.

 

Design Specification: Assume that each of the requesting agent can assert the request signal (Req 0/1/2/3) independently and will hold it asserted until the arbiter gives them grant for a pulse. The arbitration order is Req0 followed by 1 and then 2 and then 3 in a round robin fashion. Given that there are 4 requesting agents, each of them should get a grant at least one in 4 cycles. This also means that if a request is asserted, the grant signal for that agent should be assigned in a maximum of 4 cycles.

Verification

Assertion Based Verification Details:

Based on above design specifications, think through the possible assertions that you can implement to check for correct design behaviour.

Here is a list of reference assertions that should match your list:

1) In any cycle, there can be only one grant signal that can be asserted.

2) Each requesting agent should get a grant signal in a maximum 4 cycle window.

3) If one requesting agent gets a grant, it cannot receive another grant unless no other agent is requesting.

4) If there are no requests, there cannot be any grants asserted