specification SYSTOLIC_CONVOLUTION_B1 [Y] : noexit behaviour
   hide X in
      (
      GENERATOR [X]
      |[X]|
      ARRAY [X, Y] (W1, W2, W3)
      )
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;
                              stop
   endproc

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

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

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

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

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

      process BROADCAST [IN0, OUT1, OUT2, OUT3] : noexit :=
         IN0 ?X:EXP;
            OUT3 !X;
                OUT2 !X;
                    OUT1 !X;
                        BROADCAST [IN0, OUT1, OUT2, OUT3]
      endproc

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

   endproc
   
endspec