%
% implementaion of a direct mapped cache
% for a 2^a x 8*B memory
% with 2^l lines, 2^s sectors
%

dm_cache[a:posnat,
         t:subrange(1,a),
         l:upto(a-t),
         s:upto(a-l-t),
         B:posnat]: THEORY
BEGIN
  ASSUMING
    t_plus_l_plus_s_is_a : ASSUMPTION
      t+l+s=a;
  ENDASSUMING

  basics: LIBRARY = "../basics";
  IMPORTING 
    basics@basics,
    dm_cache_types[a,t,l,s,B]

% compute the valid, hit and dout signals
  dm_cache_hit_impl(tag     : cache_tagt[a,t,l,s,B], 
                    valid   : bit, 
                    adr_tag : cache_tagt[a,t,l,s,B]) : bool = 
    valid AND equal_impl[t](tag, adr_tag);

% compute next ``state´´
  dm_cache_next_config(cache:dm_cache_configt[a,t,l,s,B], 
                       input:cache_inputt[a,s,B]) : 
    [# config : dm_cache_configt[a,t,l,s,B],
       output : cache_outputt[a,s,B] #] =
  LET adr_line   = address_line[a,t,l,s,B](input`address),
      adr_tag    = address_tag[a,t,l,s,B](input`address),
      next_tag   = ram_next_conf[l,t](cache`dir`tag, 
                                      adr_line, 
                                      adr_tag, 
                                      input`tw),
      next_valid = ram_next_conf[l,1](cache`dir`valid, 
                                      adr_line, 
                                      fill[1](input`valid), 
                                      input`vw),
      next_dirty = ram_next_conf[l,1](cache`dir`dirty, 
                                      adr_line, 
                                      fill[1](input`dirty), 
                                      input`dw),
      next_data  = bw_ram_next_conf[l+s,B](cache`data, 
                                           address_linesect[a,t,l,s,B](input`address), 
                                           input`di, 
                                           input`cdwb) IN
  (# config :=
    (#
      data := next_data`next_conf,
      dir:=
      (#
        tag   := next_tag`next_conf,
        dirty := next_dirty`next_conf,
        valid := IF input`clear THEN
                   LAMBDA (line:linet) : fill[1](FALSE)
                 ELSE
                   next_valid`next_conf
                 ENDIF
      #)
    #),
    output :=
    (# 
      hit          := dm_cache_hit_impl[a,t,l,s,B](next_tag`dout, 
                                                   next_valid`dout(0),
                                                   adr_tag),
      dout         := next_data`dout,
      dirty        := next_dirty`dout(0) AND next_valid`dout(0),
      ev_address   := next_tag`dout o address_linesect[a,t,l,s,B](input`address)
    #)
  #);

  dm_cache_hit(cache:dm_cache_configt, address:addresst) : bool = 
    LET tag   = cache`dir`tag(address_line(address)),
        valid = cache`dir`valid(address_line(address))(0) IN
    dm_cache_hit_impl(tag, valid, address_tag(address));

  dm_cache_dirty(cache:dm_cache_configt, address:addresst) : bool = 
    cache`dir`dirty(address_line(address))(0) AND
    cache`dir`valid(address_line(address))(0);

  dm_cache_ev_address(cache:dm_cache_configt, address:addresst) : addresst = 
    cache`dir`tag(address_line(address)) o address_linesect(address);

  dm_cache_dout(cache:dm_cache_configt, address:addresst) : wordt =
    bw_ram_dout(cache`data, address_linesect(address));

% simple rewrites
  dm_cache_hit_impl_correct : LEMMA
    FORALL (cache : dm_cache_configt,
            input : cache_inputt) :
      dm_cache_next_config(cache,input)`output`hit =
        dm_cache_hit(cache,input`address);

  dm_cache_dout_impl_correct : LEMMA
    FORALL (cache : dm_cache_configt,
            input : cache_inputt) :
      dm_cache_next_config(cache,input)`output`dout =
        dm_cache_dout(cache,input`address);

% for arguments involving several cache cycles,
% a definition of the i-th state of a cache

  dm_cache_config(initial_dm_cache : dm_cache_configt,
                  n:nat, input:[nat->cache_inputt]) : 
    RECURSIVE dm_cache_configt =
    IF n=0 THEN
      initial_dm_cache
    ELSE
      dm_cache_next_config(dm_cache_config(initial_dm_cache,n-1,input),
                           input(n-1))`config
    ENDIF
    MEASURE n;

  dm_cache_output(initial_dm_cache : dm_cache_configt,
                  input            : [nat->cache_inputt]) : cache_output_funct =
    LAMBDA (n:nat, address:addresst): 
      (# hit          := dm_cache_hit(dm_cache_config(initial_dm_cache,n,input),address),
         dout         := dm_cache_dout(dm_cache_config(initial_dm_cache,n,input),address),
         dirty        := dm_cache_dirty(dm_cache_config(initial_dm_cache,n,input),address),
         ev_address   := dm_cache_ev_address(dm_cache_config(initial_dm_cache,n,input),address)
       #);

  dm_cache_out(initial_dm_cache : dm_cache_configt,
               input            : [nat->cache_inputt]) : 
    [ nat -> cache_outputt ] =
    LAMBDA (n:nat):
      dm_cache_next_config(dm_cache_config(initial_dm_cache,n,input),input(n))`output;

  dm_cache_out_is_output : LEMMA
    FORALL (initial_dm_cache : dm_cache_configt,
            input            : cache_input_funct):
    dm_cache_out(initial_dm_cache,input)=
    LAMBDA (n:nat): 
      dm_cache_output(initial_dm_cache,input)(n,input(n)`address);

END dm_cache