%
% control for an arbitrary cache
% (direct mapped, set associative, fully associative)
% with a-bit-addresses, 8*2^b-byte words
% and 2^s words per cache line


interface_types[a:above(1), s:subrange(1,a-1), b:nat]: THEORY
BEGIN
  IMPORTING
    control_types[a,s,b]

  interface_configt : TYPE+ = [# scnt     : sectt[a,s,2^b],
                                 fwd_word : wordt[a,2^b] #];

  interface_inputt : TYPE+ = 
  [# address       : addresst[a,2^b], % output of the dlx
     mwb           : bvec[2^b],       % output of the dlx
     din           : wordt[a,2^b],    %
     scntce        : bit,  %
     scntclr       : bit,  %
     cache_w       : bit,  % outputs of the control
     snoop_access  : bit,  %
     sw            : bit,  %
     lfill         : bit,  %
     snoop_address : addresst[a,2^b], % snnop address
%     cache_dout    : wordt[a,2^b], % output of the cache
     mdat          : wordt[a,2^b] #];  %output of the memory

  interface_outputt : TYPE+ = 
  [# cdwb        : bvec[2^b],       % 
     address     : addresst[a,2^b], % inputs for the cache
     di          : wordt[a,2^b],    %
     dout        : wordt[a,2^b],      % input for the data forwarding circuit 
     madr        : addresst[a,2^b] #];  % input for the memory

  interface_input_funct  : TYPE+ = [ nat -> interface_inputt  ];

  interface_output_funct : TYPE+ = [ nat -> interface_outputt ];

END interface_types