Proving Liveness and Termination of Systolic Arrays Using Communication Finite State Machines. - Mohamed G. Gouda; Hui-Seng Lee (IEEE Trans. Software Eng., 1985)