Stream transformers are a formalism to specify and reason about stream processing systems. Many application specific circuits, e.g. in the area of signal processing, classify as such systems. This paper presents a two- operator calculus to reason about a specific class of stream operators, viz.
the periodic stream samplers. The calculus is sound and complete and an algorithm using only a few rules is given to bring each operator sequence in canonical form. The calculus can be used to show functional correctness of any permutation circuit. It is shown how the basic building blocks of these circuits are specified using the operators, and as an example of the calculus the correctness of a non-trivial buffer is proven. In addition it is argued that this calculus can be a valuable ingredient of any larger calculus that deals with circuit components that have more complicated functionality.
Name | Computer science reports |
---|
Volume | 0502 |
---|
ISSN (Print) | 0926-4515 |
---|