specification SYSTOLIC_CONVOLUTION_W2 [Y] : noexit behaviour
   hide X in
      (
      GENERATOR [X]
      |[X]|
      ARRAY [X, Y] (W1, W2, W3, W4, W5, W6, W7)
      )
where

   library BOOLEAN, NATURAL, EXP endlib

(*---------------------------------------------------------------------------*)

   process GENERATOR [X] : noexit :=
      X !X1;
         X !X2;
            X !X3;
               X !X4;
                  X !X5;
                     X !X6;
                        X !X7;
                           X !X8;
                              X !X9;
                               X !X10;
      X !X11;
         X !X12;
            X !X13;
               X !X14;
                  X !X15;
                     X !X16;
                        X !X17;
                           X !X18;
                              X !X19;
                                 X !X20;
       X !X21;
          X !X22;
             X !X23;
                X !X24;
                   X !X25;
                      X !X26;
                          stop
   endproc

(*---------------------------------------------------------------------------*)

   process ZERO [Y] : noexit :=
      Y !(0 of EXP);
         ZERO [Y]
   endproc

(*---------------------------------------------------------------------------*)

   process ARRAY [X0, Y7] (W1, W2, W3, W4, W5, W6, W7:EXP) : noexit :=
      hide X1, X2, X3, X4, X5, X6, X7, Y0, Y1, Y2, Y3, Y4, Y5, Y6 in
         (
         ZERO [Y0]
         |[Y0]|
         CELL [X0, Y0, X1, Y1] (W7, 7)
         |[X1, Y1]|
         CELL [X1, Y1, X2, Y2] (W6, 6)
         |[X2, Y2]|
         CELL [X2, Y2, X3, Y3] (W5, 5)
         |[X3, Y3]|
         CELL [X3, Y3, X4, Y4] (W4, 4)
         |[X4, Y4]|
         CELL [X4, Y4, X5, Y5] (W3, 3)
         |[X5, Y5]|
         CELL [X5, Y5, X6, Y6] (W2, 2)
         |[X6, Y6]|
         CELL [X6, Y6, X7, Y7] (W1, 1)
         )
   where

      (*---------------------------------------------------------------------*)

      process CELL [X_IN, Y_IN, X_OUT, Y_OUT] (W:EXP, K:NAT) : noexit :=
         [K gt 1] ->
            X_IN ?X:EXP;
               X_OUT !X;
                  CELL [X_IN, Y_IN, X_OUT, Y_OUT] (W, K - 1)
         []
         [K eq 1] ->
            X_IN ?X:EXP;
               Y_IN ?Y:EXP;
                  Y_OUT !(Y + (W * X));
                     X_OUT !X;
                        CELL [X_IN, Y_IN, X_OUT, Y_OUT] (W, 1)
      endproc

      (*---------------------------------------------------------------------*)

   endproc

endspec