%
% implemetation of the computation of the next hit-vector
%
% $Id: implementation.pvs,v 1.6 2001/07/09 13:35:08 sbeyer Exp $
%
% $Log: implementation.pvs,v $
% Revision 1.6  2001/07/09 13:35:08  sbeyer
% * simplified import-chain
%
% Revision 1.5  2001/07/09 09:09:48  sbeyer
% * now using arrays for history_vector (since it is supported by pvs2hdl)
%
% Revision 1.4  2001/05/29 12:30:50  sbeyer
% * removed EXPORTING declaration
%
% Revision 1.3  2001/05/22 09:46:27  sbeyer
% - imported types instantiated
% - removed "orphaned proofs" in types
%
% Revision 1.2  2001/05/21 12:56:33  sbeyer
% added lemma way_moves_lte_1_positions_backward and fixed some unexplainable (non-existent?) errors
%
% Revision 1.1  2001/03/09 13:31:32  sbeyer
% *** empty log message ***
%

implementation[K:upfrom(2),
               logK:posnat]: THEORY
BEGIN
  ASSUMING
    logK_is_logK: ASSUMPTION 
      2^(logK-1) < K AND K <= 2^logK;
  ENDASSUMING

  IMPORTING 
      history_types[K,logK]

% initial history vector
  initial_history_vector : history_vectort[K,logK] =
    LAMBDA (i:below(K)) : nat2bv[logK](i);

% ev computes address of the way that is to be evicted
  ev(history_vector:history_vectort[K,logK]):history_datat[K,logK] = 
    history_vector(K-1);

% hsel_input
  hsel_input(history_vector   :history_vectort[K,logK], 
             hit_vector_binary:history_datat[K,logK],
             hit              :bit):hit_vectort[K,logK] = 
  pp_impl[K](LAMBDA (i:history_indext[K,logK]) : 
    LET eq=equal_impl[logK](history_vector(i), hit_vector_binary) IN
      eq AND hit);

% a-mux in hsel
  hsel_a_mux(ev_element       :history_datat[K,logK], 
             hit_vector_binary:history_datat[K,logK],
             hit              :bit): history_datat[K,logK] =
    IF hit THEN
      hit_vector_binary
    ELSE
      ev_element
    ENDIF;

% b-mux in hsel
  hsel_b_mux(pp_out         : hit_vectort[K,logK], 
             history_vector : history_vectort[K,logK]) :
    [below(K-1) -> bvec[logK]] =
    LAMBDA (i:below(K-1)):
      IF pp_out(i) THEN
        history_vector(i+1)
      ELSE
        history_vector(i)
      ENDIF;

% put the a- and b-mux output together for next history
  next_history_vector(history_vector    : history_vectort[K,logK], 
                      hit_vector        : hit_vectort[K,logK], 
                      hit_vector_binary : history_datat[K,logK],
                      hit               : bit,
                      linv              : bit) : history_vectort[K,logK] =
    
    LET pp_output  = hsel_input[K,logK](history_vector,
                                        hit_vector_binary,
                                        hit),
        ev_element = ev[K,logK](history_vector),
        a_mux      = hsel_a_mux[K,logK](ev_element,
                                        hit_vector_binary,
                                        hit),
        b_mux      = hsel_b_mux[K,logK](pp_output,history_vector) IN
      LAMBDA (i:below(K)):
        IF linv THEN
          IF i=K-1 THEN
            a_mux
          ELSE
            b_mux(i)
          ENDIF
        ELSE
          IF i=0 THEN
            a_mux
          ELSE
            b_mux(i-1)
          ENDIF
        ENDIF;

% next wayreg
  next_way_reg(history_vector : history_vectort[K,logK], 
               hit_vector     : hit_vectort[K,logK],
               hit            : bit) : hit_vectort[K,logK] =
    LET dec=decoder_impl[logK,2^logK](ev[K,logK](history_vector)) IN
    LAMBDA (i:history_indext[K,logK]) : 
      (dec(i) AND NOT hit) OR hit_vector(i);

END implementation