% % Implementation of DLX Memory % cache_mem_impl_sven: THEORY BEGIN dlxif : LIBRARY = "../dlxif"; basics: LIBRARY = "../basics"; lib : LIBRARY = "../lib"; pipe_control : LIBRARY = "../pipe_control"; IMPORTING cache_mem_impl_types, dlxif@isa, basics@basicadder, basics@sext, basics@equal, lib@exp_lems, pipe_control@ext_pipe_control_nc[29,sa_cache,2,1,20,7,sa_cache,4,2,20,7,2,3]; % compute the effective address compute_EA(address:registert, imm :registert):registert = basicadder_impl[32](address,imm,FALSE)^(31,0); tommem_step(mem : mem_reg, input : tommem_inputt): tommem_stept= LET imal = input`PC(1) OR input`PC(0), imr = NOT imal, imm = sext_impl[16,32](input`inputs`f^(15,0)), EA = compute_EA(input`inputs`op(0),imm), dmal = I_misa(EA, input`inputs`f), % stall = mem`inst`dmal OR stall_in, mw = mem`inst`valid AND mem`inst`I_s AND NOT mem`inst`dmal AND NOT mem`inst`stalled AND mem`inst`storing, mr = mem`inst`valid AND NOT mem`inst`I_s AND NOT mem`inst`dmal AND NOT mem`inst`stalled, mwb = gen_bw8(EA, I_s(input`inputs`f), I_w(input`inputs`f), I_h(input`inputs`f), I_f(input`inputs`f)), sh4s = shift4store_imp(EA,input`inputs`op(2)), % we stall in a valid instruction if % - stall_in is active (then inst`valid cannot become inactive % in the following cycle) % on inactive stall_in, we do not stall if % - either stalled is active (the instuction terminates after stall in this cycle) % - or the memory instrucion terminates regularly % (this includes "fast" exception termination) mif_in = (# memory_output := input`bp_in, ext_memory_interface_output := (# data := (# mr := mr OR mem`inst`rollback AND NOT mem`inst`I_s, mw := mw OR mem`inst`rollback AND mem`inst`I_s, address := mem`inst`EA^(31,3), dout := mem`inst`data, mbw := mem`inst`mwb #), data2 := input`ext_in, inst := (# mr := imr OR mem`istalled, address := IF mem`istalled THEN mem`mPC ELSE input`PC^(31,3) ENDIF #), clear := input`ext_reset #) #), mif_next = ext_pipe_impl_next_conf_nc[29,sa_cache,2,1,20,7,sa_cache,4,2,20,7,2,3](mem`mif,mif_in), stallout = mem`inst`valid OR mem`inst`rollback, din = IF I_f(input`inputs`f) THEN input`inputs`op(3) o input`inputs`op(2) ELSE sh4s o sh4s ENDIF, dout = IF NOT mem`inst`I_s AND NOT mem`inst`stalled AND NOT mem`inst`dmal AND NOT mif_next`output`ext_memory_interface_input`data`busy THEN mif_next`output`ext_memory_interface_input`data`din ELSE mem`inst`data ENDIF, cdb_dout=IF mem`inst`stalled THEN mem`inst`data ELSE mif_next`output`ext_memory_interface_input`data`din ENDIF, sh4ldi= IF mem`inst`EA(2) THEN cdb_dout^(63,32) ELSE cdb_dout^(31,0) ENDIF, sh4l= shift4load_imp(mem`inst`EA, sh4ldi, mem`inst`I_b,mem`inst`I_h,mem`inst`I_w,mem`inst`I_u) IN (# reg := (# mif :=mif_next`next_conf, istalled := (imr OR mem`istalled) AND mif_next`output`ext_memory_interface_input`inst`busy AND NOT input`ext_reset, mPC := IF mif_next`output`ext_memory_interface_input`inst`busy AND NOT mem`istalled THEN input`PC^(31,3) ELSE mem`mPC ENDIF, inst :=IF input`ext_reset THEN mem`inst WITH [valid := FALSE, rollback := FALSE ] ELSIF NOT stallout THEN (# tag := input`inputs`tag, valid := input`inputs`valid AND NOT input`clear, stalled := FALSE, EA := EA, data := din, mwb := mwb, I_b := I_b(input`inputs`f), I_h := I_h(input`inputs`f), I_w := I_w(input`inputs`f), I_u := I_u(input`inputs`f), I_f := I_f(input`inputs`f), I_s := I_s(input`inputs`f), dmal := dmal, dpf := FALSE, rollback := FALSE, storing := FALSE #) ELSIF input`clear OR mem`inst`rollback THEN mem`inst WITH [valid := mem`inst`valid AND NOT input`clear, rollback := (mw OR mr OR mem`inst`rollback) AND mif_next`output`ext_memory_interface_input`data`busy] ELSE % this is the stallout case (i.e. % mem`inst`valid % holds mem`inst WITH [stalled := IF NOT mif_next`output`ext_memory_interface_input`data`busy AND NOT (mem`inst`I_s AND NOT mem`inst`storing) OR mem`inst`dmal OR input`stall_in AND mem`inst`stalled THEN % we now have: mem`inst`valid AND (stall_in OR NOT mem`inst`stalled) OR mem`inst`valid input`stall_in ELSE mem`inst`stalled ENDIF, valid := input`stall_in OR NOT mem`inst`dmal AND NOT mem`inst`stalled AND (mem`inst`I_s AND NOT mem`inst`storing OR mif_next`output`ext_memory_interface_input`data`busy), data := dout, storing := equal_impl[tag_width](input`ROBtail,mem`inst`tag) AND NOT mem`inst`stalled AND NOT mem`inst`dmal AND mem`inst`I_s AND NOT mem`inst`storing OR mem`inst`storing AND mif_next`output`ext_memory_interface_input`data`busy ] ENDIF % stalled is set when a data memory acces is in fact stalled % (mem`mif`arb(1) AND mem`mif`automaton`done AND stall_in) % and it is cleared when NOT stall_in % on a reset, it is obviously cleared.. #), imem_out := IF imal THEN r0 ELSIF input`PC(2) THEN mif_next`output`ext_memory_interface_input`inst`din^(63,32) ELSE mif_next`output`ext_memory_interface_input`inst`din^(31,0) ENDIF, imem_busy:= mif_next`output`ext_memory_interface_input`inst`busy OR mem`istalled AND NOT equal_impl[29](mem`mPC,input`PC^(31,3)), imal := imal, ipf := FALSE, ext_out := mif_next`output`ext_memory_interface_input`data2, bp_out := mif_next`output`memory_input, out := (# tag := mem`inst`tag, valid := NOT input`stall_in AND mem`inst`valid AND (mem`inst`dmal OR mem`inst`stalled OR NOT (mem`inst`I_s AND NOT mem`inst`storing) AND NOT mif_next`output`ext_memory_interface_input`data`busy), data := LAMBDA (i:below(2)): % the 'dont-care' result has to reflect specification... IF mem`inst`dmal OR mem`inst`dpf OR mem`inst`I_s THEN r0 ELSIF i=0 THEN IF mem`inst`I_f THEN cdb_dout^(31,0) ELSE sh4l ENDIF ELSE IF mem`inst`I_f THEN cdb_dout^(63,32) ELSE sh4l ENDIF ENDIF, CA:=LAMBDA (i: below(32)): COND i=2 -> mem`inst`dmal, i=4 -> mem`inst`dpf, ELSE -> FALSE ENDCOND, EData := mem`inst`EA #) #); compute_EA_correct : LEMMA FORALL (Iw, op0 : registert): compute_EA(op0,sext_impl[16,32](Iw^(15,0)))= op0+sign_extend(32)(Iw^(15,0)); END cache_mem_impl_sven