Verification of a systolic algorithm in process algebra
W. P. Weijland · Cambridge University Press eBooks · 1990
In designing VLSI-circuits it is very useful, if not necessary, to construct the specific circuit by placing simple components in regular configurations. Systolic systems are circuits built up from arrays of cells and therefore very suitable for formal analysis and induction methods. In the case of a palindrome recognizer a correctness proof is given using bisimulation semantics with asynchronous cooperation. The proof is carried out in the formal setting of the Algebra of Communicating Processes (see Bergstra & Klop [1986]), which provides us with an algebraical theory and a convenient proof system. An extensive introduction to this theory is included in this paper. The palindrome recognizer has also been studied by Hennessy [1986] in a setting of failure semantics with synchronous cooperation. INTRODUCTION In the current research on (hardware) verification one of the main goals is to find strong proof systems and tools to verify the designs of algorithms and architectures. For instance, in the development of integrated circuits the important stage of testing a prototype (to save the high costs of producing defective processors) can be dealt with much more efficiently, when a strong verification tool is available. Therefore, developing a verification theory has very high priority and is subject of study at many universities and scientific institutions. However, working on detailed verification theories is not the only approach to this problem. Once having a basic theory, the development of case studies is of utmost importance to provide us with new ideas.