This paper presents a theoretical framework to reason about 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.