PROC RegBank(CHAN OF INT WDec,ADec,BDec,Wbus,AbusO, BbusO, 
             CHAN OF ANY IAin, NoRead,  
             Wack,Valid,DAout,CHAN OF BOOL Ma, Memin)
  
  #USE "debug.lib"



  CHAN OF INT dItoWL, dItoAD,dItoBD,dWLtoWD,WDtoAf,WDtoMf,ADtoRdLk, BDtoRdLk, 
             ALkftoreg, MLkftoreg, AftoRdLk, MftoRdLk,Atord,Btord, ArgtoOL,
             BrgtoOL:
  
  CHAN OF ANY aWltoI, Lkdone,LkDn, NoRd, RdDone, Wdecen, RdDi, RdDonewd ,aLftoWl,
              NoLk,AAtoRdLk, MAtoRdLk, WrtdoneA,WrtdoneM ,Aack,Mack:


  CHAN OF BOOL LDMa:


  --**************************************************************
  PROC AMfmul(CHAN OF EVENT Aack, Mack, WLack, LkDn )
    BOOL any, any1:
    WHILE TRUE
      SEQ
        ALT
          Aack?any
            SKIP
          Mack?any
            SKIP
        PAR
          WLack!any
          LkDn!any1
  :

  ------------------------------------------------------------------
  PROC  Lkdnmul(CHAN OF ANY NoLk, Lkdn, Lkdone)
    BOOL any:

    WHILE TRUE
      SEQ
        ALT
          NoLk?any
            SKIP
          Lkdn?any
            SKIP
        Lkdone!any
  :
 
  --------------------------------------------------------------------
  PROC Rddnmul(CHAN OF ANY NoRd, RdDone, Wdecen)
    BOOL any:

    WHILE TRUE
      SEQ
        ALT
          NoRd?any
            SKIP
          RdDone?any
            SKIP
        Wdecen!any
  :
  -------------------------------------------------------------------
  PROC Rddnfork(CHAN OF ANY RdDone, RdDonei, RdDonewd)
    
    BOOL any, any1:
    WHILE TRUE
      SEQ
        RdDone?any
        PAR
          RdDonei!any
          RdDonewd!any1
  :


  --***************************************************************  
  PROC Input(CHAN OF RDATAST WDec,
             CHAN OF DATA ADec,BDec,
             CHAN OF DATAST toAdec,toBdec,toWlatch,
             CHAN OF EVENT IAin, NoReadi, NoReado,LkFin,ReadDone,WAin)
    
    INT aaddr, baddr:
    [MSGLENGTH]INT waddr:
    BOOL noread, end:
    SEQ
      
      noread:=FALSE
      end:=FALSE 
      PAR                           
        WDec?CASE 
          data; waddr
            SKIP
          stop
            end:=TRUE         
        ALT
          NoReadi?CASE signal
            noread:=TRUE
          ADec?aaddr
            BDec?baddr
                                     
  
      WHILE NOT end
        SEQ
          PAR
            toWlatch!data;waddr
            IF
              noread=FALSE
                PAR
                  toAdec!data;aaddr
                  toBdec!data;baddr
              TRUE
                SEQ
                  NoReado!signal                  
          PAR
            SEQ
              PAR
                IF
                  noread=FALSE      
                    ReadDone?CASE signal
                  TRUE
                    noread:=FALSE
                WAin?CASE signal
              IAin!signal
            LkFin?CASE signal
          PAR                           
            WDec?CASE 
              data; waddr
                SKIP
              stop
                end:=TRUE 
     
            ALT
              NoReadi?CASE signal
                noread:=TRUE
              ADec?aaddr
                BDec?baddr         
      PAR
        toWlatch!stop
        toAdec!stop
        toBdec!stop         

  :  

  --****************************************************************
  PROC WLatch(CHAN OF RDATAST Win,Wout, 
              CHAN OF EVENT Ain, Aout, NoLk,
              CHAN OF BOOL Mai,Mao)
    INT data:
    BOOL nolock, main,end:
    SEQ
      end:=FALSE
      PAR
        Win?CASE
          data;data
            SKIP
          stop
            end:=TRUE           
        Mai?main


      WHILE NOT end
        SEQ
          nolock:=FALSE
          PAR
            Ain!CASE signal
            IF
              data=#FFFF
                SEQ
                  PAR
                    NoLk!CASE signal
                    Wout!data;data
                  nolock:=TRUE
              TRUE
                PAR 
                  Wout!data
                  Mao!main
          PAR
            Mai?main
            Win?CASE
              data;data
                SKIP
              stop
                end:=TRUE
            IF
              nolock=FALSE
                Aout?CASE signal
              TRUE
                SKIP

      Wout!stop
                
  :

  --****************************************************************
  PROC OLatch(CHAN OF RDATAST DAin, DBin, DAout, DBout,
              CHAN OF EVENT Ain, Aout)
    INT adata, bdata:
    BOOL any:
    SEQ  
      PAR
        DAin?adata
        DBin?bdata
      WHILE TRUE
        SEQ
          PAR
            Ain ! any
            DAout!adata
            DBout!bdata

          PAR
            DAin?adata
            DBin?bdata
            Aout ? any
  :

  --****************************************************************
  PROC WDecoder(CHAN OF RDATAST  Din, DAout, DMout,
                CHAN OF BOOL Ma,
                CHAN OF EVENT ReadDone) 

    INT data:
    BOOL main, any, datrecv:
    SEQ
      end:=FALSE
      datrecv:=FALSE    
      Din?CASE
        data;data
          SKIP
        stop
          end:=TRUE    

      WHILE NOT end
        SEQ
          PAR
            IF 
              data <> #FFFF 
                SEQ          
                  Ma?main
                  datrecv:=TRUE
                TRUE 
                  datrecv:=FALSE
            ReadDone?CASE signal
          IF 
            datrecv = TRUE
              SEQ
                IF
                  main=TRUE
                    DMout!data;data
                  main=FALSE
                    DAout!data;data
            TRUE
              SKIP  
              
          Din?CASE
            data;data
              SKIP
            stop
              end:=TRUE
      PAR
        DAout!stop
        DMout!stop        
  
  :
  --****************************************************************
  PROC ADecoder(CHAN OF RDATAST Din, Dout)
    
    INT addr:
    BOOL end:
    SEQ
      end:=FALSE
      WHILE NOT end
        SEQ
          Din?CASE
            data;addr
              Dout!data;addr
            stop
              SEQ
                end:=TRUE
                Dout!stop

  :
  --****************************************************************
  PROC BDecoder(CHAN OF RDATAST Din, Dout)
    
    INT addr:
    BOOL end:
    SEQ
      end:=FALSE
      WHILE NOT end
        SEQ
          Din?CASE
            data;addr
              Dout!data;addr
            stop
              SEQ
                end:=TRUE
  :
  --****************************************************************

  PROC LkFifos(CHAN OF RDATAST ADin,ADout, ADtoRdLock,MDin, MDout,MDtoRdLock,
               CHAN OF EVENT AAin, AAout, AAtoRdLock,MAin, MAout, MAtoRdLock)


    PROC fifo.stage( CHAN OF RDATAST Din, Dout,
                       CHAN OF EVENT Ain, Aout)

      INT data:
      BOOL end:           
      SEQ
        end:=FALSE
        Din?CASE
          data;data
            SKIP
          stop
            end:=TRUE
           
        WHILE NOT end 
          SEQ
            PAR
              Ain !CASE signal
              Dout ! data;data
            PAR
              Din ?CASE
                data;data
                  SKIP
                stop
                  end:=TRUE
              Aout ? CASE signal
        Dout!stop
    :
    -----------------------------------------------------------------
    PROC first.stage(CHAN OF INT Din, Dout, toRdLock,
                   CHAN OF EVENT Ain, Aout)

      INT data: 
      BOOL any:          
      SEQ
        Din? CASE
          data;data
            SKIP
          stop
            end:=TRUE
                 
        WHILE TRUE
          SEQ
            toRdLock!data
            DEBUG.MESSAGE("NEW VALUE IN THE FIFO")
            PAR
              Ain ! signal
              Dout ! data;data
            PAR
              Din ?CASE
                data;data
                  SKIP
                stop
                  end:=TRUE
              Aout ? CASE signal
        Dout!stop     
    :
    ---------------------------------------------------------------------
    PROC last.stage( CHAN OF INT Din, Dout,
                       CHAN OF EVENT Ain, Aout, toRdlock)

      INT data: 
      BOOL any:          
      SEQ
        PAR
          Din? CASE
            data;data
              SKIP
            stop
              end:=TRUE         
        WHILE TRUE
          SEQ
            PAR
              Ain !signal
              Dout ! data;data
            PAR
              Din ? CASE
                data;data
                  SKIP
                stop
                  end:=TRUE
              SEQ
                Aout ? CASE signal
                toRdlock!signal
       Dout!stop
  
    :
    -----------------------------------------------------------------------
    PROC ALkFifo(CHAN OF RDATAST Din,Dout,DtoRdLock,
              CHAN OF EVENT AtoRdLock, Ain, Aout)

      VAL INT num.of.stages IS 3:
      [num.of.stages]CHAN OF RDATAST Data:
      [num.of.stages]CHAN OF EVENT Ack:
      INT i:
      PAR
        first.stage(Din, Data[0],DtoRdLock,Ain, Ack[0])
        PAR i=0 FOR num.of.stages-2
          fifo.stage(Data[i],Data[i+1],Ack[i], Ack[i+1])
        last.stage(Data[num.of.stages-2], Dout, Ack[num.of.stages-2],
                     Aout,AtoRdLock)
    :

    --------------------------------------------------------------------------
    PROC MLkFifo(CHAN OF RDATAST Din,Dout,DtoRdLock,
              CHAN OF EVENT AtoRdLock, Ain, Aout)

      VAL INT num.of.stages IS 4:
      [num.of.stages]CHAN OF RDATAST Data:
      [num.of.stages]CHAN OF EVENT Ack:
      INT i:
      PAR 
        first.stage(Din, Data[0],DtoRdLock,Ain, Ack[0])
        PAR i=0 FOR num.of.stages-2
          fifo.stage(Data[i],Data[i+1],Ack[i], Ack[i+1])
        last.stage(Data[num.of.stages-2], Dout, Ack[num.of.stages-2],
                     Aout,AtoRdLock)
    :
    -----------------main body of LkFifos------------------------------- 

    PAR
      ALkFifo( ADin,ADout, ADtoRdLock,AAtoRdLock, AAin,AAout )
      MLkFifo( MDin, MDout,MDtoRdLock,MAtoRdLock,MAin, MAout)
  :
  --*******************************************************************

  PROC ReadLock(CHAN OF RDATAST DfromAf, DfromMf, DfromAdec, DfromBdec, Atord, 
                                Btord, 
                CHAN OF EVENT AfromAf, AfromMf)

    VAL INT AfSize IS 3:
    VAL INT MfSize IS 4:
    [AfSize]INT Abuffer: 
    [MfSize]INT Mbuffer: 
    INT Atop, Abase, Mtop, Mbase, aaddr,baddr,i:
    BOOL awaits, bwaits, acango, bcango, any, end:
    
    SEQ
      Atop:=0
      Mtop:=0  
      Abase:=0
      Mbase:=0
      awaits:=FALSE
      bwaits:=FALSE 
      end:=FALSE
      WHILE NOT end
        PRI ALT
    
          AfromAf?CASE signal
            SEQ
              Abase:=(Abase+1) REM AfSize

              IF
                (awaits=TRUE)       
                  SEQ
                    acango:=TRUE

                    i:=Abase
                    WHILE (i<>Atop)                       
                      SEQ
                        IF
                          (Abuffer[i]=aaddr) 
                            acango:=FALSE
                          TRUE
                            SKIP 
                        i:=(i+1) REM AfSize 

                    i:=Mbase
                    WHILE (i<>Mtop)                    
                      SEQ
                        IF
                          (Mbuffer[i]=aaddr) 
                            acango:=FALSE
                          TRUE
                            SKIP 
                        i:=(i+1) REM MfSize
                TRUE
                  SKIP      

              IF
                (bwaits=TRUE)      
                  SEQ
                    bcango:=TRUE

                    i:=Abase
                    WHILE (i<>Atop)
                      SEQ
                        IF
                          (Abuffer[i]=baddr)  
                            bcango:=FALSE
                          TRUE
                            SKIP 
                        i:=(i+1) REM AfSize

                    i:=Mbase
                    WHILE (i<>Mtop)
                      SEQ
                        IF
                          (Mbuffer[i]=baddr)  
                            bcango:=FALSE
                          TRUE
                            SKIP   
                        i:=(i+1) REM MfSize
                TRUE
                  SKIP  
 
              PAR
                IF
                  (acango=TRUE) AND (awaits=TRUE)
                    SEQ
                      Atord!aaddr
                      awaits:=FALSE
                  TRUE
                    SKIP
    
                IF
                  (bcango=TRUE) AND (bwaits=TRUE)
                    SEQ
                      Btord!baddr
                      bwaits:=FALSE
                  TRUE
                    SKIP

   
          AfromMf?CASE signal
            SEQ
              Mbase:=(Mbase+1) REM MfSize

              IF
                (awaits=TRUE)     
                  SEQ
                    acango:=TRUE
                    i:=Mbase
                    WHILE (i<>Mtop)
                      SEQ
                        IF
                          (Mbuffer[i]=aaddr)  
                            acango:=FALSE
                          TRUE
                            SKIP
                        i:=(i+1) REM MfSize
  

                    i:=Abase
                    WHILE (i<>Atop)
                      SEQ
                        IF
                          (Abuffer[i]=aaddr)  
                            acango:=FALSE
                          TRUE
                            SKIP 
                        i:=(i+1) REM AfSize  
                TRUE
                  SKIP      

              IF
                (bwaits=TRUE)     
                  SEQ
                    bcango:=TRUE
                    i:=Mbase
                    WHILE (i<>Mtop)
                      SEQ
                        IF
                          (Mbuffer[i]=baddr) 
                            bcango:=FALSE
                          TRUE
                            SKIP 
                        i:=(i+1) REM MfSize

 
                    i:=Abase
                    WHILE (i<>Atop)
                      SEQ
                        IF
                          (Abuffer[i]=baddr) 
                            bcango:=FALSE
                          TRUE
                            SKIP  
                        i:=(i+1) REM AfSize 
                TRUE
                  SKIP  
 
              PAR
                IF
                  (acango=TRUE) AND (awaits=TRUE)
                    SEQ
                      Atord!aaddr
                      awaits:=FALSE
                  TRUE
                    SKIP
    
                IF
                  (bcango=TRUE) AND (bwaits=TRUE)
                    SEQ
                      Btord!baddr
                      bwaits:=FALSE
                  TRUE
                    SKIP
            

          DfromAf?Abuffer[Atop]
            Atop:=(Atop+1) REM AfSize

          DfromMf?Mbuffer[Mtop]
            Mtop:=(Mtop+1) REM MfSize

          DfromAdec?CASE
            data;aaddr          
              SEQ
                DfromBdec?baddr
                i:=Abase
                WHILE (i<>Atop)
                  SEQ
                    IF
                      (Abuffer[i]=aaddr) 
                        awaits:=TRUE
                      TRUE
                        SKIP
                    IF
                      (Abuffer[i]=baddr) 
                        bwaits:=TRUE
                      TRUE
                        SKIP
                    i:=(i+1) REM AfSize 


                i:=Mbase
                WHILE (i<>Mtop)
                  SEQ
                    IF
                      (Mbuffer[i]=aaddr) 
                        awaits:=TRUE
                      TRUE
                        SKIP
                    IF
                      (Mbuffer[i]=baddr) 
                        bwaits:=TRUE
                      TRUE
                        SKIP
                    i:=(i+1) REM MfSize 

          
                PAR
                  IF
                    awaits=FALSE
                      Atord!aaddr
                    TRUE
                      SKIP
                  IF
                    bwaits=FALSE
                      Btord!baddr
                    TRUE
                      SKIP
           stop
             SEQ
               end:=TRUE
               aaddr!stop
                
  :
  --***************************************************************************
  PROC Registers(CHAN OF RDATAST Abus, Bbus, Aaddr, Baddr, Wbus, fromAfifo, 
                                 fromMfifo, 
                 CHAN OF BOOL Memin,
                 CHAN OF EVENT Wack, WrtdoneA,WrtdoneM, Valid )
    
    VAL INT  num.of.reg IS 30:
    VAL INT BUSA IS 0:
    VAL INT BUSB IS 1:

    [num.of.reg]CHAN OF INT Rdenact,Wrtenact, CtoA, CtoB:
   

    ----------------------------------------------------------------------------
    PROC Multiplex([]CHAN OF INT CtoA, CtoB,  CHAN OF INT Abus, Bbus)

      INT adata, bdata,i,j:

      WHILE TRUE
        PAR
          ALT i = 0 FOR num.of.reg
            CtoA[i]?adata
              Abus!adata
          ALT j = 0 FOR num.of.reg
            CtoB[j]?bdata
              Bbus!bdata
    :
    ----------------------------------------------------------------------------
    PROC Read([]CHAN OF INT Rdenact, CHAN OF INT Aaddr, Baddr)
      INT addra, addrb:
      BOOL end:
      WHILE NOT end
        SEQ
          SEQ
            Aaddr?CASE
              data;addra 
                SEQ         
                  Baddr?data;addrb                                
                  Rdenact[addra] !BUSA
                  Rdenact[addrb]!BUSB

              stop
                
                end:=TRUE
                  
    :
    -------------------------------------------------------------------------
    PROC Write([]CHAN OF INT Wrtenact, CHAN OF RDATAST Wbus, fromAfifo,
                                                       fromMfifo, 
               CHAN OF EVENT Valid, Wack, WrtdoneA,WrtdoneM,
               CHAN OF BOOL Memin)
      BOOL mfifo,val:
      INT wdata,addr:
      BOOL any, any1:

      WHILE TRUE
        SEQ
          val:=FALSE
          PAR
            Memin?mfifo      
            ALT
              Valid?any
                val:=TRUE
              Wbus?wdata
                SKIP
          IF
            mfifo = TRUE
              fromMfifo?addr
            TRUE
              fromAfifo?addr
          IF
            val = FALSE
              Wrtenact[addr]!wdata
            TRUE
              SKIP 
          PAR
            Wack!any1
            IF
              mfifo=TRUE  
                WrtdoneM!any 
              TRUE  
                WrtdoneA!any               
    :
    -------------------------------------------------------------------------
    PROC Registercells ([]CHAN OF INT Rdenact, Wrtenact, Abus, Bbus)
              
      INT i:
      PROC Cell(CHAN OF INT fromrd, fromwrt, toabus, tobbus)
      
        INT enact, data:
        SEQ
          data:=0
          WHILE TRUE          
            ALT
              fromrd?enact
                IF
                  enact = BUSA
                    toabus!data
                  enact = BUSB
                    tobbus!data
              fromwrt?data
                SKIP
      :

      PAR i=0 FOR num.of.reg
        Cell(Rdenact[i], Wrtenact[i], Abus[i], Bbus[i]) 
     
    :
    ---------------Registers main body-----------------------------------

    PAR
      Read(Rdenact,Aaddr, Baddr)
      Write(Wrtenact,Wbus, fromAfifo, fromMfifo, Valid, Wack, WrtdoneA,WrtdoneM, 
            Memin)
      Registercells(Rdenact, Wrtenact, CtoA, CtoB)
      Multiplex(CtoA, CtoB,Abus, Bbus)

  :

  --------------------------------------------------------------------------
  
  PAR
   
    Input(WDec,ADec,BDec,dItoAD,dItoBD,dItoWL,
          IAin, NoRead, NoRd, Lkdone, RdDi, aWltoI)
   
    WLatch(dItoWL,dWLtoWD, aWltoI, aLftoWl, NoLk, Ma, LDMa)
   
    WDecoder(dWLtoWD, WDtoAf, WDtoMf, LDMa, Wdecen) 
   
    ADecoder(dItoAD, ADtoRdLk)
    
    BDecoder(dItoBD, BDtoRdLk)
 
   
    LkFifos(WDtoAf, ALkftoreg, AftoRdLk, WDtoMf, MLkftoreg,MftoRdLk,
            Aack, WrtdoneA, AAtoRdLk,Mack, WrtdoneM, MAtoRdLk)
   
    ReadLock(AftoRdLk, MftoRdLk, ADtoRdLk, BDtoRdLk, Atord, Btord, 
             AAtoRdLk, MAtoRdLk)
   
    Registers(ArgtoOL, BrgtoOL, Atord, Btord, Wbus, ALkftoreg, MLkftoreg, 
              Memin,Wack, WrtdoneA,WrtdoneM, Valid )

    OLatch(ArgtoOL, BrgtoOL, AbusO, BbusO,RdDone, DAout)

    AMfmul(Aack, Mack, aLftoWl, LkDn)
   
    Rddnmul(NoRd, RdDonewd, Wdecen)
   
    Rddnfork(RdDone, RdDi, RdDonewd)
  
    Lkdnmul(NoLk, LkDn, Lkdone)
:
    


    


  
          
            

    

 
