%
% implementation of a 2^k x N RAM
%

ram[k:nat, N:posnat]: THEORY 
BEGIN
  IMPORTING 
    ram_types[k,N]

% ram_next_conf computes the new state of the ram given the inputs
  ram_next_conf(ram     : ramt[k,N], 
                address : ram_addresst[k,N], 
                din     : ram_wordt[k,N], 
                we      : bit):
    [# next_conf : ramt[k,N], dout : ram_wordt[k,N] #] =
    (#
      next_conf :=
        IF we THEN
          ram WITH [address := din]
        ELSE
          ram
        ENDIF,
      dout := ram(address)
    #);
  
% ram2p_next_conf computes the new state of the ram given the inputs (2-port)
  ram2p_next_conf(ram       : ramt[k,N], 
                  radr,wadr : ram_addresst[k,N], 
                  din       : ram_wordt[k,N], 
                  we        : bit):
    [# next_conf : ramt[k,N], dout : ram_wordt[k,N] #] =
    (#
      next_conf :=
        IF we THEN
          ram WITH [wadr := din]
        ELSE
          ram
        ENDIF,
      dout := ram(radr)
    #);

% ram3p_next_conf computes the new state of the ram given the inputs (3-port)
  ram3p_next_conf(ram       : ramt[k,N], 
                  radr_A,
                  radr_B,
                  wadr      : ram_addresst[k,N], 
                  din       : ram_wordt[k,N], 
                  we        : bit):
    [# next_conf : ramt[k,N], dout_A, dout_B : ram_wordt[k,N] #] =
    (#
      next_conf :=
        IF we THEN
          ram WITH [wadr := din]
        ELSE
          ram
        ENDIF,
      dout_A := ram(radr_A),
      dout_B := ram(radr_B)
    #);

END ram