// ************************************************************************** //
//                                                                            //
//    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).
// ----------------------------------------------------------------