Calculating a round-robin scheduler

Kropf has collected together a number of problems that can be used as benchmarks for hardware verification, one of which is a bus arbiter. The function of the bus arbiter is to assign the use of a shared resource on each clock cycle to one out of N subsystems that may want to use it, and in such a way that no subsystem is denied access forever. The most significant component in its implementation is a round-robin scheduler. Rather than verify the existing implementation of the scheduler, this paper shows how to construct a correct implementation from the given requirements. We make use of both point-free and pointwise relation algebra.