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

   library BOOLEAN, NATURAL, EXP endlib

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

   process GENERATOR [X] : noexit :=
      X !X1;
         X !X2;
            X !X3;
               X !X4;
                  X !X5;
                     X !X6;
                        stop
   endproc

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

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

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

   process ARRAY [X0, Y0] (W1, W2, W3, W4:EXP) : noexit :=
      hide X1, X2, X3, Y1, Y2, Y3 in
         (
         CELL [X0, Y0, X1, Y1] (W3, 3)
         |[X1, Y1]|
         CELL [X1, Y1, X2, Y2] (W2, 2)
         |[X2, Y2]|
         CELL [X2, Y2, X3, Y3] (W1, 1)
         |[Y3]|
         ZERO [Y3]
         )
   where

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

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

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

   endproc

endspec