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.
|Title of host publication||Mathematics of Program Construction (Proceedings 4th International Conference, MPC'98, Marstrand, Sweden, July 15-17, 1998)|
|Place of Publication||Berlin|
|Publication status||Published - 1998|
|Name||Lecture Notes in Computer Science|