Acta Informatica

, Volume 38, Issue 1, pp 45–88 | Cite as

Correctness of dataflow and systolic algorithms using algebras of streams

  • K. Meinke
  • L.J. Steggles
Original articles


We present two case studies which illustrate the use of second–order algebra as a formalism for specification and verification of hardware algorithms. In the first case study we specify a systolic algorithm for convolution and formally verify its correctness using second–order equational logic. The second case study demonstrates the expressive power of second–order algebraic specifications by presenting a non–constructive specification of the Hamming stream problem. A dataflow algorithm for computing the Hamming stream is then specified and the correctness of this algorithm is verified by semantical methods. Both case studies illustrate aspects of the metatheory of second-order equational logic.


Expressive Power Equational Logic Constructive Specification Semantical Method Algebraic Specification 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • K. Meinke
    • 1
  • L.J. Steggles
    • 2
  1. 1.Department of Numerical Analysis and Computer Science, KTH Stockholm, Sweden (e-mail: SE
  2. 2.Department of Computing Science, University of Newcastle, UK (e-mail: GB

Personalised recommendations