// ************************************************************************** // // // // eses eses // // eses eses // // eses eseses esesese eses Embedded Systems Group // // ese ese ese ese ese // // ese eseseses eseseses ese Department of Computer Science // // eses eses ese eses // // eses eseses eseseses eses University of Kaiserslautern // // eses eses // // // // ************************************************************************** // // -------------------------------------------------------------------------- // The following module derives a signal flow graph (SFG) from the observations // given in KuLL87a (and verified in file KuLL87a.qrz). Note that it is not // yet a systolic array, since the propagating variables c and r are immediately // broadcasted through the entire circuit. Moreover, we load the input matrix // in parallel to the array. The considered signal flow graph and the resulting // processor array as described below has still some spiral dependencies. // -------------------------------------------------------------------------- import ComputerArchitecture.SystolicArrays.TransitiveClosure.KuLL87aSpiralSFG.*; import ComputerArchitecture.SystolicArrays.TransitiveClosure.Warshall.WarshallB; package ComputerArchitecture.SystolicArrays.TransitiveClosure.KuLL87aSpiralSFG; macro N = 3; module KuLL87aSpiralSFG([N][N]bool ?a, t1, t2, event rdy) { weak abort { { WarshallB(a,t1); emit (rdy); } || SpiralArraySFG(a,t2); } when(rdy); } satisfies { s : assert A G (rdy -> forall(i=0..(N-1)) forall(j=0..(N-1)) (t1[i][j] <-> t2[i][j]) ); } // ---------------------------------------------------------------- // The reference is the following O(N) time version of Warshall's // algorithm (see WarshallAB.qrz for equivalent variants). // ----------------------------------------------------------------