Equivalence relations of synchronous schemes

Cirovic, Branislav (2000) Equivalence relations of synchronous schemes. Doctoral (PhD) thesis, Memorial University of Newfoundland.

[English] PDF (Migrated (PDF/A Conversion) from original format: (application/pdf)) - Accepted Version Available under License - The author retains copyright ownership and moral rights in this thesis. Neither the thesis nor substantial extracts from it may be printed or otherwise reproduced without the author's permission. Download (9MB) [English] PDF - Accepted Version Available under License - The author retains copyright ownership and moral rights in this thesis. Neither the thesis nor substantial extracts from it may be printed or otherwise reproduced without the author's permission. (Original Version)

Abstract

Synchronous systems are single purpose multiprocessor computing machines, which provide a realistic model of computation capturing the concepts of pipelining, parallelism and interconnection. The syntax of a synchronous system is specified by the synchronous scheme, which is in fact a directed, labelled, edge-weighted multi-graph. The vertices and their labels represent functional elements (the combinational logic) with some operation symbols associated with them, while the edges represent interconnections between functional elements. Each edge is weighted and the non- negative integer weight (register count) is the number of registers (clocked memory) placed along the interconnection between two functional elements. These notions allowed the introduction of transformations useful for the design and optimization of synchronous systems: retiming and slowdown. -- Two synchronous systems are strongly equivalent if they have the same stepwise behavior under all interpretations. Retiming a functional element in a synchronous system means shifting one layer of registers from one side of the functional element to the other. Retiming equivalence is obtained as the reflexive and transitive closure of this primitive retiming relation. Slowdown is defined as follows: for any system G = (V,E,w) and any positive integer c, the c-slow system cG = (V,E,w') is the one obtained by multiplying all the register counts in G by c. Slowdown equivalence is obtained as the symmetric and transitive closure of this primitive slowdown relation. Strong retiming equivalence is the join of two basic equivalence relations on synchronous systems, namely strong equivalence and retiming equivalence. Slowdown retiming equivalence is the join of retiming and slowdown equivalence. Strong slowdown retiming equivalence is the join of strong, slowdown and retiming equivalence. It is proved that both slowdown retiming and strong slowdown retiming equivalence of synchronous systems (schemes), are decidable. -- According to [Leiserson and Saxe, 1983a, 1983b], synchronous systems S and S' are equivalent if for every sufficiently old configuration c of S, there exists a configuration c' of S' such that when S started in configuration c and S' started in configuration c' the two systems exhibit the same behavior. It is proved that two synchronous systems (schemes) are Leiserson equivalent if and only if they are strong retiming equivalent. -- The semantics of synchronous systems can be specified by algebraic structures called feedback theories. Synchronous schemes and feedback theories have been ax-iomatized equationally in [Bartha, 1987]. Here we extend the existing set of axioms in order to capture strong retiming equivalence. -- One of the fundamental features of synchronous systems is synchrony, that is, the computation of the network is synchronized by a global (basic) clock. Other, slower clocks can be defined in terms of boolean-valued flows. In order to describe the behavior of schemes with multiple regular clocks, we extend the existing algebra of schemes to include multiclocked schemes, and study the general idea of Leiserson equivalence in the framework of this algebra.

Actions (login required)

View Item