Design and performance analysis of buffers: a constructive approach

This paper presents a theoretical framework to analyse the correctness of VLSI programs for buffers and to compare the performance of the corresponding circuits. A very simple calculus consisting of only two operators is presented that suffices to establish the functional correctness of complicated buffer designs. Furthermore, sequence functions are presented both as a formalism to show absence of deadlock and as a vehicle for performance analysis. It is shown that the class of square FIFOs is optimal in the sense that no buffer of the same capacity and I/O-distance can accommodate a larger range of occupancies, when run at its minimum cycle time. Moreover, the theory accurately predicts the size of the range of occupancies that has been found experimentally.