% % implementaion of a set associative cache % for a 2^a x 8*B memory using LRU replacement % with 2^k direct mapped caches % with 2^l lines, 2^s sectors % sa_cache[K:upfrom(2), logK:posnat, 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; logK_is_logK: ASSUMPTION 2^(logK-1) < K AND K <= 2^logK; ENDASSUMING history : LIBRARY = "../history"; cache : LIBRARY = "../cache"; IMPORTING sa_cache_types[K,logK,a,t,l,s,B], cache@dm_cache[a,t,l,s,B], history@implementation[K,logK] % compute the valid, hit and dout signals sa_cache_hit_impl(hit_vector : hit_vectort[K,logK]) : bool = encoderf_impl[logK,K](hit_vector)`or_tree; sa_cache_dout_impl(hit_vector : hit_vectort[K,logK], way_dout : [ wayt[K,logK,a,t,l,s,B] -> wordt[a,B] ]) : wordt[a,B] = mux_tree_unary_select_impl[8*B,K](way_dout,hit_vector); sa_cache_forward_mux_impl(hist_reg : history_vectort[K,logK], history_out : history_vectort[K,logK], equal : bool) : history_vectort[K,logK] = LAMBDA (i:below(K)): IF equal THEN hist_reg(i) ELSE history_out(i) ENDIF; history_word_to_vector(word : bvec[K*logK]):history_vectort[K,logK]= LAMBDA (i:below(K)): word^(i*logK+logK-1,i*logK); history_vector_to_word(vector : history_vectort[K,logK]):bvec[K*logK]= LAMBDA (i:below(K*logK)): vector(div(i,logK))(mod(i,logK)); % inputs for the i-th direct mapped caches dm_cache_input(way_reg : way_regt[K,logK,a,t,l,s,B], input : cache_inputt[a, s, B], i : wayt[K,logK,a,t,l,s,B]) : cache_inputt[a, s, B] = input WITH [ dw := input`dw AND way_reg(i), vw := input`vw AND way_reg(i), tw := input`tw AND way_reg(i), cdwb := LAMBDA (ii:below(B)) : input`cdwb(ii) AND way_reg(i)]; % compute next ``state´´ sa_cache_next_config(cache : sa_cache_configt[K,logK,a,t,l,s,B], input : cache_inputt[a, s, B]) : [# config : sa_cache_configt[K,logK,a,t,l,s,B], output : cache_outputt[a,s,B] #] = LET adr_line =address_line[a, t, l, s, B](input`address), next_history=ram2p_next_conf[l,K*logK](cache`history, adr_line, cache`adr_reg, history_vector_to_word(cache`hist_reg), input`cache_rd), dm_next_conf =LAMBDA (i:wayt[K,logK,a,t,l,s,B]): dm_cache_next_config[a,t,l,s,B](cache`way(i), dm_cache_input[K,logK,a,t,l,s,B](cache`way_reg,input,i)), way_dout =LAMBDA (i:wayt[K,logK,a,t,l,s,B]) : dm_next_conf(i)`output`dout, dirty_out =LAMBDA (i:wayt[K,logK,a,t,l,s,B]) : fill[1](dm_next_conf(i)`output`dirty), ev_adr_out =LAMBDA (i:wayt[K,logK,a,t,l,s,B]) : dm_next_conf(i)`output`ev_address, hit_vector =LAMBDA (i:wayt[K,logK,a,t,l,s,B]) : dm_next_conf(i)`output`hit, hit_encf =encoderf_impl[logK,K](hit_vector), hit_signal =hit_encf`or_tree, forw_mux =sa_cache_forward_mux_impl[K,logK,a,t,l,s,B](cache`hist_reg, history_word_to_vector(next_history`dout), IF l=0 THEN TRUE ELSE equal_impl[l](adr_line,cache`adr_reg) ENDIF), next_way_reg =next_way_reg[K,logK](forw_mux,hit_vector,hit_signal) IN (# config := (# hist_reg := IF input`clear OR input`cache_rd THEN IF input`clear THEN initial_history_vector[K,logK] ELSE next_history_vector[K,logK](forw_mux, hit_vector, hit_encf`encf_out, hit_signal, input`linv) ENDIF ELSE cache`hist_reg ENDIF, way := LAMBDA (i:wayt): dm_next_conf(i)`config, way_reg := IF input`cache_rd THEN next_way_reg ELSE cache`way_reg ENDIF, adr_reg := IF input`cache_rd THEN adr_line ELSE cache`adr_reg ENDIF, history := IF input`clear THEN LAMBDA (x:linet) : history_vector_to_word(initial_history_vector[K,logK]) ELSE next_history`next_conf ENDIF #), output := (# dout := sa_cache_dout_impl[K,logK,a,t,l,s,B](hit_vector, way_dout), hit := hit_signal, dirty := mux_tree_unary_select_impl[1,K](dirty_out,next_way_reg)(0), ev_address := mux_tree_unary_select_impl[a,K](ev_adr_out,next_way_reg) #) #); sa_cache_hit_vector(cache:sa_cache_configt, address:addresst) : way_regt = LAMBDA (i:wayt) : dm_cache_hit(cache`way(i), address); sa_cache_hit(cache:sa_cache_configt, address:addresst) : bool = sa_cache_hit_impl(sa_cache_hit_vector(cache, address)); sa_cache_dout(cache:sa_cache_configt, address:addresst) : wordt = sa_cache_dout_impl(sa_cache_hit_vector(cache,address), LAMBDA (ii:wayt) : dm_cache_dout(cache`way(ii), address)); % data to be written into history-ram is forwarded iff addresses match % data is split into K ways sa_cache_forward_mux(cache : sa_cache_configt, address : addresst) : history_vectort[K,logK] = sa_cache_forward_mux_impl(cache`hist_reg, history_word_to_vector(cache`history(address_line(address))), address_line(address)=cache`adr_reg); sa_cache_dirty(cache:sa_cache_configt, address:addresst) : bool = mux_tree_unary_select_impl[1,K](LAMBDA (i:below(K)): fill[1](dm_cache_dirty(cache`way(i),address)), next_way_reg(sa_cache_forward_mux(cache,address), sa_cache_hit_vector(cache,address), sa_cache_hit(cache,address)))(0); sa_cache_ev_address(cache:sa_cache_configt, address:addresst) : addresst = mux_tree_unary_select_impl[a,K](LAMBDA (i:below(K)): dm_cache_ev_address(cache`way(i),address), next_way_reg(sa_cache_forward_mux(cache,address), sa_cache_hit_vector(cache,address), sa_cache_hit(cache,address))); % simple rewrites empty_line_equal : LEMMA FORALL (line,line2:linet): l=0 IMPLIES line=line2; sa_cache_hit_vector_impl_correct : LEMMA FORALL (cache : sa_cache_configt, input : cache_inputt): (LAMBDA (i:wayt) : dm_cache_next_config[a,t,l,s,B](cache`way(i), dm_cache_input[K,logK,a,t,l,s,B](cache`way_reg,input,i))`output`hit)= sa_cache_hit_vector(cache,input`address); sa_cache_hit_impl_correct : LEMMA FORALL (cache : sa_cache_configt, input : cache_inputt): sa_cache_next_config(cache,input)`output`hit= sa_cache_hit(cache,input`address); sa_cache_forward_mux_impl_correct : LEMMA FORALL (cache : sa_cache_configt, input : cache_inputt): sa_cache_forward_mux_impl(cache`hist_reg, history_word_to_vector(ram2p_next_conf[l,K*logK](cache`history, address_line(input`address), cache`adr_reg, history_vector_to_word(cache`hist_reg), input`cache_rd)`dout), IF l=0 THEN TRUE ELSE equal_impl[l](address_line(input`address),cache`adr_reg) ENDIF)= sa_cache_forward_mux(cache,input`address); sa_cache_dout_impl_correct : LEMMA FORALL (cache : sa_cache_configt, input : cache_inputt): sa_cache_next_config(cache,input)`output`dout= sa_cache_dout(cache,input`address); % for arguments involving several cache cycles, % a definition of the i-th state of a cache sa_cache_config(initial_sa_cache: sa_cache_configt, n:nat, input:cache_input_funct) : RECURSIVE sa_cache_configt = IF n=0 THEN initial_sa_cache ELSE sa_cache_next_config(sa_cache_config(initial_sa_cache,n-1,input),input(n-1))`config ENDIF MEASURE n; sa_cache_out(initial_sa_cache : sa_cache_configt, input : cache_input_funct) : [ nat -> cache_outputt ] = LAMBDA (n:nat): sa_cache_next_config(sa_cache_config(initial_sa_cache,n,input),input(n))`output; END sa_cache