The use of fixed point induction in verifying systolic array designs: an applicative approach

The paper presents our applicative approach of using fixed point induction principle to verify the correctness of systolic array designs. Fixed point induction exploits the repeatable, regular, and local attributes of systolic arrays in realizing recursive functions. The applicative language in denotational semantics improves proof efficiency by skipping the redundant search time and space that occurred in other techniques. Our approach, as well as an example of applying it to prove a systolic array for matrix inversion, are provided in the paper