Theory Sparc_State

(*
 * Copyright 2016, NTU
 *
 * This software may be distributed and modified according to the terms of
 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
 * See "LICENSE_BSD2.txt" for details.
 *
 * Author: Zhe Hou, David Sanan.
 *)

section ‹SPARC V8 state model›
theory Sparc_State
imports Main Sparc_Types  "../lib/wp/DetMonadLemmas" MMU
begin                                                                    
section ‹state as a function›

record cpu_cache = 
dcache:: cache_context
icache:: cache_context

text‹
The state @{term sparc_state} is defined as a tuple @{term cpu_context}, 
@{term user_context}, @{term mem_context}, defining the state of the CPU registers, 
user registers, memory, cache, and delayed write pool respectively. 
Additionally, a boolean indicates whether the state is 
undefined or not.
›

record (overloaded) ('a) sparc_state =
cpu_reg:: cpu_context
user_reg:: "('a) user_context"
sys_reg:: sys_context
mem:: mem_context
mmu:: MMU_state
cache:: cpu_cache
dwrite:: delayed_write_pool
state_var:: sparc_state_var
traps:: "Trap set"
undef:: bool

section‹functions for state member access›

definition cpu_reg_val:: "CPU_register ⇒ ('a) sparc_state ⇒ reg_type"
where
"cpu_reg_val reg state ≡ (cpu_reg state) reg"

definition cpu_reg_mod :: "word32 ⇒ CPU_register ⇒ ('a) sparc_state ⇒ 
                           ('a) sparc_state"
where "cpu_reg_mod data_w32 cpu state ≡ 
  state⦇cpu_reg := ((cpu_reg state)(cpu := data_w32))⦈"

text ‹r[0] = 0. Otherwise read the actual value.›
definition user_reg_val:: "('a) window_size ⇒ user_reg_type ⇒ ('a) sparc_state ⇒ reg_type"
where
"user_reg_val window ur state ≡ 
  if ur = 0 then 0
  else (user_reg state) window ur"

text ‹Write a global register. win should be initialised as NWINDOWS.›
fun (sequential) global_reg_mod :: "word32 ⇒ nat ⇒ user_reg_type ⇒ 
  ('a::len) sparc_state ⇒ ('a) sparc_state"
where
"global_reg_mod data_w32 0 ur state = state"
|
"global_reg_mod data_w32 win ur state = (
    let win_word = word_of_int (int (win-1));
        ns = state⦇user_reg := 
          (user_reg state)(win_word := ((user_reg state) win_word)(ur := data_w32))⦈ 
    in
    global_reg_mod data_w32 (win-1) ur ns
)"

text ‹Compute the next window.›
definition next_window :: "('a::len) window_size ⇒ ('a) window_size"
where
"next_window win ≡
  if (uint win) < (NWINDOWS - 1) then (win + 1)
  else 0
"

text ‹Compute the previous window.›
definition pre_window :: "('a::len) window_size ⇒ ('a::len) window_size"
where
"pre_window win ≡
  if (uint win) > 0 then (win - 1)
  else (word_of_int (NWINDOWS - 1))
"

text ‹write an output register. 
  Also write ur+16 of the previous window.›
definition out_reg_mod :: "word32 ⇒ ('a::len) window_size ⇒ user_reg_type ⇒ 
  ('a) sparc_state ⇒ ('a) sparc_state"
where
"out_reg_mod data_w32 win ur state ≡
  let state' = state⦇user_reg :=
        (user_reg state)(win := ((user_reg state) win)(ur := data_w32))⦈;
      win' = pre_window win;
      ur' = ur + 16
  in
  state'⦇user_reg := 
    (user_reg state')(win' := ((user_reg state') win')(ur' := data_w32))⦈
"

text ‹Write a input register.
  Also write ur-16 of the next window.›
definition in_reg_mod :: "word32 ⇒ ('a::len) window_size ⇒ user_reg_type ⇒
  ('a) sparc_state ⇒ ('a) sparc_state"
where
"in_reg_mod data_w32 win ur state ≡
  let state' = state⦇user_reg :=
    (user_reg state)(win := ((user_reg state) win)(ur := data_w32))⦈;
      win' = next_window win;
      ur' = ur - 16
  in
  state'⦇user_reg :=
    (user_reg state')(win' := ((user_reg state') win')(ur' := data_w32))⦈
"

text ‹Do not modify r[0].›
definition user_reg_mod :: "word32 ⇒ ('a::len) window_size ⇒ user_reg_type ⇒ 
 ('a) sparc_state ⇒ ('a) sparc_state"
where
"user_reg_mod data_w32 win ur state ≡
  if ur = 0 then state
  else if 0 < ur ∧ ur < 8 then
    global_reg_mod data_w32 (nat NWINDOWS) ur state
  else if 7 < ur ∧ ur < 16 then 
    out_reg_mod data_w32 win ur state
  else if 15 < ur ∧ ur < 24 then
    state⦇user_reg := 
      (user_reg state)(win := ((user_reg state) win)(ur := data_w32))⦈
  else ⌦‹if 23 < ur ∧ ur < 32 then›
    in_reg_mod data_w32 win ur state
  ⌦‹else state›
"

definition sys_reg_val :: "sys_reg ⇒ ('a) sparc_state ⇒ reg_type"
where
"sys_reg_val reg state ≡ (sys_reg state) reg"

definition sys_reg_mod :: "word32 ⇒ sys_reg ⇒ 
                          ('a) sparc_state ⇒ ('a) sparc_state"
where
"sys_reg_mod data_w32 sys state ≡ state⦇sys_reg := (sys_reg state)(sys := data_w32)⦈"

text ‹The following fucntions deal with physical memory. 
N.B. Physical memory address in SPARCv8 is 36-bit.›

text ‹LEON3 doesn't distinguish ASI 8 and 9; 10 and 11 for read access
  for both user and supervisor. 
We recently discovered that the compiled machine code by
the sparc-elf compiler often reads asi = 10 (user data) 
when the actual content is store in asi = 8 (user instruction).
For testing purposes, we don't distinguish asi = 8,9,10,11
for reading access.›

definition mem_val:: "asi_type ⇒ phys_address ⇒ 
                      ('a) sparc_state ⇒ mem_val_type option"
where
"mem_val asi add state ≡ 
  let asi8 = word_of_int 8;
      asi9 = word_of_int 9;
      asi10 = word_of_int 10;
      asi11 = word_of_int 11;
      r1 = (mem state) asi8 add
  in
  if r1 = None then
    let r2 = (mem state) asi9 add in
    if r2 = None then
      let r3 = (mem state) asi10 add in
      if r3 = None then 
        (mem state) asi11 add
      else r3
    else r2
  else r1
"

text ‹An alternative way to read values from memory. 
Some implementations may use this definition.›

definition mem_val_alt:: "asi_type ⇒ phys_address ⇒ 
                      ('a) sparc_state ⇒ mem_val_type option"
where
"mem_val_alt asi add state ≡ 
  let r1 = (mem state) asi add; 
      asi8 = word_of_int 8;
      asi9 = word_of_int 9;
      asi10 = word_of_int 10;
      asi11 = word_of_int 11
  in
  if r1 = None ∧ (uint asi) = 8 then
    let r2 = (mem state) asi9 add in
    r2
  else if r1 = None ∧ (uint asi) = 9 then
    let r2 = (mem state) asi8 add in
    r2
  else if r1 = None ∧ (uint asi) = 10 then
    let r2 = (mem state) asi11 add in
    if r2 = None then
      let r3 = (mem state) asi8 add in
      if r3 = None then
        (mem state) asi9 add        
      else r3
    else r2
  else if r1 = None ∧ (uint asi) = 11 then
    let r2 = (mem state) asi10 add in
    if r2 = None then
      let r3 = (mem state) asi8 add in
      if r3 = None then
        (mem state) asi9 add        
      else r3
    else r2
  else r1"

definition mem_mod :: "asi_type ⇒ phys_address ⇒ mem_val_type ⇒ 
                         ('a) sparc_state ⇒ ('a) sparc_state"
where
"mem_mod asi addr val state ≡
  let state1 = state⦇mem := (mem state)
    (asi := ((mem state) asi)(addr := Some val))⦈
  in ― ‹Only allow one of ‹asi› 8 and 9 (10 and 11) to have value.›
  if (uint asi) = 8 ∨ (uint asi) = 10 then
    let asi2 = word_of_int ((uint asi) + 1) in
    state1⦇mem := (mem state1)
      (asi2 := ((mem state1) asi2)(addr := None))⦈
  else if (uint asi) = 9 ∨ (uint asi) = 11 then
    let asi2 = word_of_int ((uint asi) - 1) in
    state1⦇mem := (mem state1)(asi2 := ((mem state1) asi2)(addr := None))⦈
  else state1
"

text ‹An alternative way to write memory. This method insists that 
for each address, it can only hold a value in one of ASI = 8,9,10,11.›

definition mem_mod_alt :: "asi_type ⇒ phys_address ⇒ mem_val_type ⇒ 
                         ('a) sparc_state ⇒ ('a) sparc_state"
where
"mem_mod_alt asi addr val state ≡
  let state1 = state⦇mem := (mem state)
    (asi := ((mem state) asi)(addr := Some val))⦈;
    asi8 = word_of_int 8;
    asi9 = word_of_int 9;
    asi10 = word_of_int 10;
    asi11 = word_of_int 11
  in 
  ― ‹Only allow one of ‹asi› 8, 9, 10, 11 to have value.›
  if (uint asi) = 8 then 
    let state2 = state1⦇mem := (mem state1)
      (asi9 := ((mem state1) asi9)(addr := None))⦈;
     state3 = state2⦇mem := (mem state2)
      (asi10 := ((mem state2) asi10)(addr := None))⦈;
     state4 = state3⦇mem := (mem state3)
      (asi11 := ((mem state3) asi11)(addr := None))⦈
    in
    state4
  else if (uint asi) = 9 then 
    let state2 = state1⦇mem := (mem state1)
      (asi8 := ((mem state1) asi8)(addr := None))⦈;  
     state3 = state2⦇mem := (mem state2)
      (asi10 := ((mem state2) asi10)(addr := None))⦈;
     state4 = state3⦇mem := (mem state3)
      (asi11 := ((mem state3) asi11)(addr := None))⦈
    in
    state4  
  else if (uint asi) = 10 then 
    let state2 = state1⦇mem := (mem state1)
      (asi9 := ((mem state1) asi9)(addr := None))⦈;
     state3 = state2⦇mem := (mem state2)
      (asi8 := ((mem state2) asi8)(addr := None))⦈;
     state4 = state3⦇mem := (mem state3)
      (asi11 := ((mem state3) asi11)(addr := None))⦈
    in
    state4
  else if (uint asi) = 11 then 
    let state2 = state1⦇mem := (mem state1)
      (asi9 := ((mem state1) asi9)(addr := None))⦈;
     state3 = state2⦇mem := (mem state2)
      (asi10 := ((mem state2) asi10)(addr := None))⦈;
     state4 = state3⦇mem := (mem state3)
      (asi8 := ((mem state3) asi8)(addr := None))⦈
    in
    state4
  else state1
"

context
  includes bit_operations_syntax
begin

text ‹Given an ASI (word8), an address (word32) addr, 
        read the 32bit value from the memory addresses 
        starting from address addr' where addr' = addr 
        exception that the last two bits are 0's. 
        That is, read the data from 
        addr', addr'+1, addr'+2, addr'+3.›
definition mem_val_w32 :: "asi_type ⇒ phys_address ⇒ 
                           ('a) sparc_state ⇒ word32 option"
where
"mem_val_w32 asi addr state ≡
  let addr' = (AND) addr 0b111111111111111111111111111111111100;
      addr0 = addr';
      addr1 = addr' + 1;
      addr2 = addr' + 2;
      addr3 = addr' + 3;
      r0 = mem_val_alt asi addr0 state;
      r1 = mem_val_alt asi addr1 state;
      r2 = mem_val_alt asi addr2 state;
      r3 = mem_val_alt asi addr3 state
  in
  if r0 = None ∨ r1 = None ∨ r2 = None ∨ r3 = None then
    None
  else
    let byte0 = case r0 of Some v ⇒ v;
        byte1 = case r1 of Some v ⇒ v;
        byte2 = case r2 of Some v ⇒ v;
        byte3 = case r3 of Some v ⇒ v 
    in
    Some ((OR) ((OR) ((OR) ((ucast(byte0)) << 24) 
                              ((ucast(byte1)) << 16)) 
                       ((ucast(byte2)) << 8)) 
                (ucast(byte3)))
"

text ‹
  Let ‹addr'› be ‹addr› with last two bits set to 0's.
  Write the 32bit data in the memory address ‹addr'›
  (and the following 3 addresses). 
  ‹byte_mask› decides which byte of the 32bits are written.
›
definition mem_mod_w32 :: "asi_type ⇒ phys_address ⇒ word4 ⇒ word32 ⇒ 
                           ('a) sparc_state ⇒ ('a) sparc_state"
where
"mem_mod_w32 asi addr byte_mask data_w32 state ≡
  let addr' = (AND) addr 0b111111111111111111111111111111111100;
      addr0 = (OR) addr' 0b000000000000000000000000000000000000;
      addr1 = (OR) addr' 0b000000000000000000000000000000000001;
      addr2 = (OR) addr' 0b000000000000000000000000000000000010;
      addr3 = (OR) addr' 0b000000000000000000000000000000000011;
      byte0 = (ucast (data_w32 >> 24))::mem_val_type;
      byte1 = (ucast (data_w32 >> 16))::mem_val_type;
      byte2 = (ucast (data_w32 >> 8))::mem_val_type;
      byte3 = (ucast data_w32)::mem_val_type;
      s0 = if (((AND) byte_mask (0b1000::word4)) >> 3) = 1 then
              mem_mod asi addr0 byte0 state 
           else state;
      s1 = if (((AND) byte_mask (0b0100::word4)) >> 2) = 1 then
              mem_mod asi addr1 byte1 s0 
           else s0;
      s2 = if (((AND) byte_mask (0b0010::word4)) >> 1) = 1 then
              mem_mod asi addr2 byte2 s1 
           else s1;
      s3 = if ((AND) byte_mask (0b0001::word4)) = 1 then
              mem_mod asi addr3 byte3 s2 
           else s2
  in
  s3
"

text ‹The following functions deal with virtual addresses. 
These are based on functions written by David Sanan.›

definition load_word_mem :: "('a) sparc_state ⇒ virtua_address ⇒ asi_type ⇒ 
                             machine_word option"
where "load_word_mem state va asi ≡ 
let pair = (virt_to_phys va (mmu state) (mem state)) in 
case pair of
  Some pair ⇒ ( 
    if mmu_readable (get_acc_flag (snd pair)) asi then 
      (mem_val_w32 asi (fst pair) state)
    else None)
  | None ⇒ None"

definition store_word_mem ::"('a) sparc_state ⇒ virtua_address ⇒ machine_word ⇒ 
                             word4 ⇒ asi_type ⇒ ('a) sparc_state option"
where "store_word_mem state va wd byte_mask asi ≡ 
let pair = (virt_to_phys va (mmu state) (mem state)) in 
case pair of
  Some pair ⇒ ( 
    if mmu_writable (get_acc_flag (snd pair)) asi then 
      Some (mem_mod_w32 asi (fst pair) byte_mask wd state)
    else None)
  | None ⇒ None"

definition icache_val:: "cache_type ⇒ ('a) sparc_state ⇒ mem_val_type option"
where "icache_val c state ≡ icache (cache state) c"

definition dcache_val:: "cache_type ⇒ ('a) sparc_state ⇒ mem_val_type option"
where "dcache_val c state ≡ dcache (cache state) c"

definition icache_mod :: "cache_type ⇒ mem_val_type ⇒ 
                           ('a) sparc_state ⇒ ('a) sparc_state"
where "icache_mod c val state ≡ 
  state⦇cache := ((cache state)
    ⦇icache := (icache (cache state))(c := Some val)⦈)⦈
"

definition dcache_mod :: "cache_type ⇒ mem_val_type ⇒ 
                           ('a) sparc_state ⇒ ('a) sparc_state"
where "dcache_mod c val state ≡ 
  state⦇cache := ((cache state)
    ⦇dcache := (dcache (cache state))(c := Some val)⦈)⦈
"

text ‹Check if the memory address is in the cache or not.›
definition icache_miss :: "virtua_address ⇒ ('a) sparc_state ⇒ bool"
where
"icache_miss addr state ≡
  let line_len = 12;
      tag = (ucast (addr >> line_len))::cache_tag;
      line = (ucast (0b0::word1))::cache_line_size 
  in
  if (icache_val (tag,line) state) = None then True 
  else False    
"

text ‹Check if the memory address is in the cache or not.›
definition dcache_miss :: "virtua_address ⇒ ('a) sparc_state ⇒ bool"
where
"dcache_miss addr state ≡
  let line_len = 12;
      tag = (ucast (addr >> line_len))::cache_tag;
      line = (ucast (0b0::word1))::cache_line_size 
  in
  if (dcache_val (tag,line) state) = None then True 
  else False    
"

definition read_data_cache:: "('a) sparc_state ⇒ virtua_address ⇒ machine_word option"
where "read_data_cache state va ≡
  let tag = (ucast (va >> 12))::word20;
       offset0 = (AND) ((ucast va)::word12) 0b111111111100;
       offset1 = (OR) offset0 0b000000000001;
       offset2 = (OR) offset0 0b000000000010;
       offset3 = (OR) offset0 0b000000000011;
       r0 = dcache_val (tag,offset0) state;
       r1 = dcache_val (tag,offset1) state;
       r2 = dcache_val (tag,offset2) state;
       r3 = dcache_val (tag,offset3) state
  in
  if r0 = None ∨ r1 = None ∨ r2 = None ∨ r3 = None then
    None
  else
    let byte0 = case r0 of Some v ⇒ v;
        byte1 = case r1 of Some v ⇒ v;
        byte2 = case r2 of Some v ⇒ v;
        byte3 = case r3 of Some v ⇒ v 
    in
    Some ((OR) ((OR) ((OR) ((ucast(byte0)) << 24) 
                              ((ucast(byte1)) << 16)) 
                       ((ucast(byte2)) << 8)) 
                (ucast(byte3)))
"

definition read_instr_cache:: "('a) sparc_state ⇒ virtua_address ⇒ machine_word option"
where "read_instr_cache state va ≡
  let tag = (ucast (va >> 12))::word20;
       offset0 = (AND) ((ucast va)::word12) 0b111111111100;
       offset1 = (OR) offset0 0b000000000001;
       offset2 = (OR) offset0 0b000000000010;
       offset3 = (OR) offset0 0b000000000011;
       r0 = icache_val (tag,offset0) state;
       r1 = icache_val (tag,offset1) state;
       r2 = icache_val (tag,offset2) state;
       r3 = icache_val (tag,offset3) state
  in
  if r0 = None ∨ r1 = None ∨ r2 = None ∨ r3 = None then
    None
  else
    let byte0 = case r0 of Some v ⇒ v;
        byte1 = case r1 of Some v ⇒ v;
        byte2 = case r2 of Some v ⇒ v;
        byte3 = case r3 of Some v ⇒ v 
    in
    Some ((OR) ((OR) ((OR) ((ucast(byte0)) << 24) 
                              ((ucast(byte1)) << 16)) 
                       ((ucast(byte2)) << 8)) 
                (ucast(byte3)))
"

definition add_data_cache :: "('a) sparc_state ⇒ virtua_address ⇒ machine_word ⇒ 
  word4 ⇒ ('a) sparc_state"
where 
 "add_data_cache state va word byte_mask ≡ 
   let tag = (ucast (va >> 12))::word20;
       offset0 = (AND) ((ucast va)::word12) 0b111111111100;
       offset1 = (OR) offset0 0b000000000001;
       offset2 = (OR) offset0 0b000000000010;
       offset3 = (OR) offset0 0b000000000011;
       byte0 = (ucast (word >> 24))::mem_val_type;
       byte1 = (ucast (word >> 16))::mem_val_type;
       byte2 = (ucast (word >> 8))::mem_val_type;
       byte3 = (ucast word)::mem_val_type;
       s0 = if (((AND) byte_mask (0b1000::word4)) >> 3) = 1 then
              dcache_mod (tag,offset0) byte0 state
            else state;
       s1 = if (((AND) byte_mask (0b0100::word4)) >> 2) = 1 then
              dcache_mod (tag,offset1) byte1 s0
            else s0;
       s2 = if (((AND) byte_mask (0b0010::word4)) >> 1) = 1 then
              dcache_mod (tag,offset2) byte2 s1
            else s1;
       s3 = if ((AND) byte_mask (0b0001::word4)) = 1 then
              dcache_mod (tag,offset3) byte3 s2
            else s2
   in s3
"

definition add_instr_cache :: "('a) sparc_state ⇒ virtua_address ⇒ machine_word ⇒ 
  word4 ⇒ ('a) sparc_state"
where 
 "add_instr_cache state va word byte_mask ≡ 
   let tag = (ucast (va >> 12))::word20;
       offset0 = (AND) ((ucast va)::word12) 0b111111111100;
       offset1 = (OR) offset0 0b000000000001;
       offset2 = (OR) offset0 0b000000000010;
       offset3 = (OR) offset0 0b000000000011;
       byte0 = (ucast (word >> 24))::mem_val_type;
       byte1 = (ucast (word >> 16))::mem_val_type;
       byte2 = (ucast (word >> 8))::mem_val_type;
       byte3 = (ucast word)::mem_val_type;
       s0 = if (((AND) byte_mask (0b1000::word4)) >> 3) = 1 then
              icache_mod (tag,offset0) byte0 state
            else state;
       s1 = if (((AND) byte_mask (0b0100::word4)) >> 2) = 1 then
              icache_mod (tag,offset1) byte1 s0
            else s0;
       s2 = if (((AND) byte_mask (0b0010::word4)) >> 1) = 1 then
              icache_mod (tag,offset2) byte2 s1
            else s1;
       s3 = if ((AND) byte_mask (0b0001::word4)) = 1 then
              icache_mod (tag,offset3) byte3 s2
            else s2
   in s3
"

definition empty_cache ::"cache_context" where "empty_cache c ≡ None"

definition flush_data_cache:: "('a) sparc_state ⇒ ('a) sparc_state" where
"flush_data_cache state ≡ state⦇cache := ((cache state)⦇dcache := empty_cache⦈)⦈"

definition flush_instr_cache:: "('a) sparc_state ⇒ ('a) sparc_state" where
"flush_instr_cache state ≡ state⦇cache := ((cache state)⦇icache := empty_cache⦈)⦈"

definition flush_cache_all:: "('a) sparc_state ⇒ ('a) sparc_state" where
"flush_cache_all state ≡ state⦇cache := ((cache state)⦇
  icache := empty_cache, dcache := empty_cache⦈)⦈"

text ‹Check if the FI or FD bit of CCR is 1. 
If FI is 1 then flush instruction cache. 
If FD is 1 then flush data cache.›
definition ccr_flush :: "('a) sparc_state ⇒ ('a) sparc_state"
where
"ccr_flush state ≡
  let ccr_val = sys_reg_val CCR state;
      ― ‹‹FI› is bit 21 of ‹CCR››
      fi_val = ((AND) ccr_val (0b00000000001000000000000000000000)) >> 21;
      fd_val = ((AND) ccr_val (0b00000000010000000000000000000000)) >> 22;
      state1 = (if fi_val = 1 then flush_instr_cache state else state)
  in
  if fd_val = 1 then flush_data_cache state1 else state1"

definition get_delayed_pool :: "('a) sparc_state ⇒ delayed_write_pool"
where "get_delayed_pool state ≡ dwrite state"

definition exe_pool :: "(int × reg_type × CPU_register) ⇒ (int × reg_type × CPU_register)"
where "exe_pool w ≡ case w of (n,v,c) ⇒ ((n-1),v,c)"

text ‹Minus 1 to the delayed count for all the members in the set. 
        Assuming all members have delay > 0.›
primrec delayed_pool_minus :: "delayed_write_pool ⇒ delayed_write_pool"
where
"delayed_pool_minus [] = []"
|
"delayed_pool_minus (x#xs) = (exe_pool x)#(delayed_pool_minus xs)"

text ‹Add a delayed-write to the pool.›
definition delayed_pool_add :: "(int × reg_type × CPU_register) ⇒ 
                                ('a) sparc_state ⇒ ('a) sparc_state"
where 
"delayed_pool_add dw s ≡
  let (i,v,cr) = dw in
  if i = 0 then ― ‹Write the value to the register immediately.›
    cpu_reg_mod v cr s
  else ― ‹Add to delayed write pool.›
    let curr_pool = get_delayed_pool s in
    s⦇dwrite := curr_pool@[dw]⦈"

text ‹Remove a delayed-write from the pool. 
        Assume that the delayed-write to be removed has delay 0.
        i.e., it has been executed.›
definition delayed_pool_rm :: "(int × reg_type × CPU_register) ⇒ 
                               ('a) sparc_state ⇒ ('a) sparc_state"
where
"delayed_pool_rm dw s ≡
  let curr_pool = get_delayed_pool s in
  case dw of (n,v,cr) ⇒ 
    (if n = 0 then
      s⦇dwrite := List.remove1 dw curr_pool⦈
     else s)
"

text ‹Remove all the entries with delay = 0, i.e., those that are written.›
primrec delayed_pool_rm_written :: "delayed_write_pool ⇒ delayed_write_pool"
where
"delayed_pool_rm_written [] = []"
|
"delayed_pool_rm_written (x#xs) = 
  (if fst x = 0 then delayed_pool_rm_written xs else x#(delayed_pool_rm_written xs))    
"

definition annul_val :: "('a) sparc_state ⇒ bool"
where "annul_val state ≡ get_annul (state_var state)"

definition annul_mod :: "bool ⇒ ('a) sparc_state ⇒ ('a) sparc_state"
where "annul_mod b s ≡ s⦇state_var := write_annul b (state_var s)⦈"

definition reset_trap_val :: "('a) sparc_state ⇒ bool"
where "reset_trap_val state ≡ get_reset_trap (state_var state)"

definition reset_trap_mod :: "bool ⇒ ('a) sparc_state ⇒ ('a) sparc_state"
where "reset_trap_mod b s ≡ s⦇state_var := write_reset_trap b (state_var s)⦈"

definition exe_mode_val :: "('a) sparc_state ⇒ bool"
where "exe_mode_val state ≡ get_exe_mode (state_var state)"

definition exe_mode_mod :: "bool ⇒ ('a) sparc_state ⇒ ('a) sparc_state"
where "exe_mode_mod b s ≡ s⦇state_var := write_exe_mode b (state_var s)⦈"

definition reset_mode_val :: "('a) sparc_state ⇒ bool"
where "reset_mode_val state ≡ get_reset_mode (state_var state)"

definition reset_mode_mod :: "bool ⇒ ('a) sparc_state ⇒ ('a) sparc_state"
where "reset_mode_mod b s ≡ s⦇state_var := write_reset_mode b (state_var s)⦈"

definition err_mode_val :: "('a) sparc_state ⇒ bool"
where "err_mode_val state ≡ get_err_mode (state_var state)"

definition err_mode_mod :: "bool ⇒ ('a) sparc_state ⇒ ('a) sparc_state"
where "err_mode_mod b s ≡ s⦇state_var := write_err_mode b (state_var s)⦈"

definition ticc_trap_type_val :: "('a) sparc_state ⇒ word7"
where "ticc_trap_type_val state ≡ get_ticc_trap_type (state_var state)"

definition ticc_trap_type_mod :: "word7 ⇒ ('a) sparc_state ⇒ ('a) sparc_state"
where "ticc_trap_type_mod w s ≡ s⦇state_var := write_ticc_trap_type w (state_var s)⦈"

definition interrupt_level_val :: "('a) sparc_state ⇒ word3"
where "interrupt_level_val state ≡ get_interrupt_level (state_var state)"

definition interrupt_level_mod :: "word3 ⇒ ('a) sparc_state ⇒ ('a) sparc_state"
where "interrupt_level_mod w s ≡ s⦇state_var := write_interrupt_level w (state_var s)⦈"

definition store_barrier_pending_val :: "('a) sparc_state ⇒ bool"
where "store_barrier_pending_val state ≡ 
  get_store_barrier_pending (state_var state)"

definition store_barrier_pending_mod :: "bool ⇒ 
  ('a) sparc_state ⇒ ('a) sparc_state"
where "store_barrier_pending_mod w s ≡
  s⦇state_var := write_store_barrier_pending w (state_var s)⦈"

definition pb_block_ldst_byte_val :: "virtua_address ⇒ ('a) sparc_state
  ⇒ bool"
where "pb_block_ldst_byte_val add state ≡
  (atm_ldst_byte (state_var state)) add"

definition pb_block_ldst_byte_mod :: "virtua_address ⇒ bool ⇒ 
  ('a) sparc_state ⇒ ('a) sparc_state"
where "pb_block_ldst_byte_mod add b s ≡
  s⦇state_var := ((state_var s)
    ⦇atm_ldst_byte := (atm_ldst_byte (state_var s))(add := b)⦈)⦈"

text ‹We only read the address such that add mod 4 = 0. 
  add mod 4 represents the current word.›
definition pb_block_ldst_word_val :: "virtua_address ⇒ ('a) sparc_state
  ⇒ bool"
where "pb_block_ldst_word_val add state ≡
  let add0 = ((AND) add (0b11111111111111111111111111111100::word32)) in
  (atm_ldst_word (state_var state)) add0"

text ‹We only write the address such that add mod 4 = 0.
  add mod 4 represents the current word.›
definition pb_block_ldst_word_mod :: "virtua_address ⇒ bool ⇒ 
  ('a) sparc_state ⇒ ('a) sparc_state"
where "pb_block_ldst_word_mod add b s ≡
  let add0 = ((AND) add (0b11111111111111111111111111111100::word32)) in
  s⦇state_var := ((state_var s)
    ⦇atm_ldst_word := (atm_ldst_word (state_var s))(add0 := b)⦈)⦈"

definition get_trap_set :: "('a) sparc_state ⇒ Trap set"
where "get_trap_set state ≡ (traps state)"

definition add_trap_set :: "Trap ⇒ ('a) sparc_state ⇒ ('a) sparc_state"
where "add_trap_set t s ≡ s⦇traps := (traps s) ∪ {t}⦈"

definition emp_trap_set :: "('a) sparc_state ⇒ ('a) sparc_state"
where "emp_trap_set s ≡ s⦇traps := {}⦈"

definition state_undef:: "('a) sparc_state ⇒ bool"
where "state_undef state ≡ (undef state)"

text ‹The ‹memory_read› interface that conforms with the SPARCv8 manual.›
definition memory_read :: "asi_type ⇒ virtua_address ⇒ 
                           ('a) sparc_state ⇒ 
                           ((word32 option) × ('a) sparc_state)"
where "memory_read asi addr state ≡
  let asi_int = uint asi in ― ‹See Page 25 and 35 for ASI usage in LEON 3FT.›
  if asi_int = 1 then ― ‹Forced cache miss.›
    ― ‹Directly read from memory.›
    let r1 = load_word_mem state addr (word_of_int 8) in
    if r1 = None then
      let r2 = load_word_mem state addr (word_of_int 10) in
      if r2 = None then
        (None,state)
      else (r2,state)
    else (r1,state)
  else if asi_int = 2 then ― ‹System registers.›
    ― ‹See Table 19, Page 34 for System Register address map in LEON 3FT.›
    if uint addr = 0 then ― ‹Cache control register.›
      ((Some (sys_reg_val CCR state)), state)
    else if uint addr = 8 then ― ‹Instruction cache configuration register.›
      ((Some (sys_reg_val ICCR state)), state)
    else if uint addr = 12 then ― ‹Data cache configuration register.›
      ((Some (sys_reg_val DCCR state)), state)
    else ― ‹Invalid address.›
      (None, state)
  else if asi_int ∈ {8,9} then ― ‹Access instruction memory.›
    let ccr_val = (sys_reg state) CCR in
    if ccr_val AND 1 ≠ 0 then ― ‹Cache is enabled. Update cache.›
    ― ‹We don't go through the tradition, i.e., read from cache first,›
    ― ‹if the address is not cached, then read from memory,›
    ― ‹because performance is not an issue here.›
    ― ‹Thus we directly read from memory and update the cache.›
      let data = load_word_mem state addr asi in
      case data of
      Some w ⇒ (Some w,(add_instr_cache state addr w (0b1111::word4)))
      |None ⇒ (None, state)
    else ― ‹Cache is disabled. Just read from memory.›
      ((load_word_mem state addr asi),state)
  else if asi_int ∈ {10,11} then ― ‹Access data memory.›
    let ccr_val = (sys_reg state) CCR in
    if ccr_val AND 1 ≠ 0 then ― ‹Cache is enabled. Update cache.›
    ― ‹We don't go through the tradition, i.e., read from cache first,›
    ― ‹if the address is not cached, then read from memory,›
    ― ‹because performance is not an issue here.›
    ― ‹Thus we directly read from memory and update the cache.›
      let data = load_word_mem state addr asi in
      case data of
      Some w ⇒ (Some w,(add_data_cache state addr w (0b1111::word4)))
      |None ⇒ (None, state)
    else ― ‹Cache is disabled. Just read from memory.›
      ((load_word_mem state addr asi),state)
  ― ‹We don't access instruction cache tag. i.e., ‹asi = 12›.›
  else if asi_int = 13 then ― ‹Read instruction cache data.›
    let cache_result = read_instr_cache state addr in
    case cache_result of
    Some w ⇒ (Some w, state)
    |None ⇒ (None, state)
  ― ‹We don't access data cache tag. i.e., ‹asi = 14›.›
  else if asi_int = 15 then ― ‹Read data cache data.›
    let cache_result = read_data_cache state addr in
    case cache_result of
    Some w ⇒ (Some w, state)
    |None ⇒ (None, state)
  else if asi_int ∈ {16,17} then ― ‹Flush entire instruction/data cache.›
    (None, state) ― ‹Has no effect for memory read.›
  else if asi_int ∈ {20,21} then ― ‹MMU diagnostic cache access.›
    (None, state) ― ‹Not considered in this model.›
  else if asi_int = 24 then ― ‹Flush cache and TLB in LEON3.›
    ― ‹But is not used for memory read.›
    (None, state)
  else if asi_int = 25 then ― ‹MMU registers.›
    ― ‹Treat MMU registers as memory addresses that are not in the main memory.›
    ((mmu_reg_val (mmu state) addr), state) 
  else if asi_int = 28 then ― ‹MMU bypass.›
    ― ‹Directly use addr as a physical address.›
    ― ‹Append 0000 in the front of addr.›
    ― ‹In this case, (ucast addr) suffices.›
    ((mem_val_w32 asi (ucast addr) state), state)
  else if asi_int = 29 then ― ‹MMU diagnostic access.›
    (None, state) ― ‹Not considered in this model.›
  else ― ‹Not considered in this model.›
    (None, state)
"

text ‹Get the value of a memory address and an ASI.›
definition mem_val_asi:: "asi_type ⇒ phys_address ⇒ 
                      ('a) sparc_state ⇒ mem_val_type option"
where "mem_val_asi asi add state ≡ (mem state) asi add"

text ‹Check if an address is used in ASI 9 or 11.›
definition sup_addr :: "phys_address ⇒ ('a) sparc_state ⇒ bool"
where
"sup_addr addr state ≡
  let addr' = (AND) addr 0b111111111111111111111111111111111100;
      addr0 = (OR) addr' 0b000000000000000000000000000000000000;
      addr1 = (OR) addr' 0b000000000000000000000000000000000001;
      addr2 = (OR) addr' 0b000000000000000000000000000000000010;
      addr3 = (OR) addr' 0b000000000000000000000000000000000011;
      r0 = mem_val_asi 9 addr0 state;
      r1 = mem_val_asi 9 addr1 state;
      r2 = mem_val_asi 9 addr2 state;
      r3 = mem_val_asi 9 addr3 state;
      r4 = mem_val_asi 11 addr0 state;
      r5 = mem_val_asi 11 addr1 state;
      r6 = mem_val_asi 11 addr2 state;
      r7 = mem_val_asi 11 addr3 state
  in
  if r0 = None ∧ r1 = None ∧ r2 = None ∧ r3 = None ∧
     r4 = None ∧ r5 = None ∧ r6 = None ∧ r7 = None
  then False
  else True
"

text ‹The ‹memory_write› interface that conforms with SPARCv8 manual.›
text ‹LEON3 forbids user to write an address in ASI 9 and 11.›
definition memory_write_asi :: "asi_type ⇒ virtua_address ⇒ word4 ⇒ word32 ⇒ 
                            ('a) sparc_state ⇒ 
                            ('a) sparc_state option"
where
"memory_write_asi asi addr byte_mask data_w32 state ≡ 
  let asi_int = uint asi; ― ‹See Page 25 and 35 for ASI usage in LEON 3FT.›
      psr_val = cpu_reg_val PSR state;
      s_val = get_S psr_val
  in 
  if asi_int = 1 then ― ‹Forced cache miss.›
    ― ‹Directly write to memory.›
    ― ‹Assuming writing into ‹asi = 10›.›
    store_word_mem state addr data_w32 byte_mask (word_of_int 10) 
  else if asi_int = 2 then ― ‹System registers.›
    ― ‹See Table 19, Page 34 for System Register address map in LEON 3FT.›
    if uint addr = 0 then ― ‹Cache control register.›
      let s1 = (sys_reg_mod data_w32 CCR state) in
      ― ‹Flush the instruction cache if FI of CCR is 1;›
      ― ‹flush the data cache if FD of CCR is 1.›
      Some (ccr_flush s1)
    else if uint addr = 8 then ― ‹Instruction cache configuration register.›
      Some (sys_reg_mod data_w32 ICCR state)
    else if uint addr = 12 then ― ‹Data cache configuration register.›
      Some (sys_reg_mod data_w32 DCCR state)
    else ― ‹Invalid address.›
      None
  else if asi_int ∈ {8,9} then ― ‹Access instruction memory.›
    ― ‹Write to memory. LEON3 does write-through. Both cache and the memory are updated.›
    let ns = add_instr_cache state addr data_w32 byte_mask in
    store_word_mem ns addr data_w32 byte_mask asi
  else if asi_int ∈ {10,11} then ― ‹Access data memory.›
    ― ‹Write to memory. LEON3 does write-through. Both cache and the memory are updated.›
    let ns = add_data_cache state addr data_w32 byte_mask in
    store_word_mem ns addr data_w32 byte_mask asi
  ― ‹We don't access instruction cache tag. i.e., ‹asi = 12›.›
  else if asi_int = 13 then ― ‹Write instruction cache data.›
    Some (add_instr_cache state addr data_w32 (0b1111::word4))
  ― ‹We don't access data cache tag. i.e., asi = 14.›
  else if asi_int = 15 then ― ‹Write data cache data.›
    Some (add_data_cache state addr data_w32 (0b1111::word4))
  else if asi_int = 16 then ― ‹Flush instruction cache.›
    Some (flush_instr_cache state)
  else if asi_int = 17 then ― ‹Flush data cache.›
    Some (flush_data_cache state)
  else if asi_int ∈ {20,21} then ― ‹MMU diagnostic cache access.›
    None ― ‹Not considered in this model.›
  else if asi_int = 24 then ― ‹Flush TLB and cache in LEON3.›
    ― ‹We don't consider TLB here.›
    Some (flush_cache_all state)
  else if asi_int = 25 then ― ‹MMU registers.›
    ― ‹Treat MMU registers as memory addresses that are not in the main memory.›
    let mmu_state' = mmu_reg_mod (mmu state) addr data_w32 in
    case mmu_state' of
    Some mmus ⇒ Some (state⦇mmu := mmus⦈)
    |None ⇒ None 
  else if asi_int = 28 then ― ‹MMU bypass.›
    ― ‹Write to virtual address as physical address.›
    ― ‹Append 0000 in front of addr.›
    Some (mem_mod_w32 asi (ucast addr) byte_mask data_w32 state)
  else if asi_int = 29 then ― ‹MMU diagnostic access.›
    None ― ‹Not considered in this model.›
  else ― ‹Not considered in this model.›
    None
"

definition memory_write :: "asi_type ⇒ virtua_address ⇒ word4 ⇒ word32 ⇒ 
                            ('a) sparc_state ⇒ 
                            ('a) sparc_state option"
where
"memory_write asi addr byte_mask data_w32 state ≡ 
  let result = memory_write_asi asi addr byte_mask data_w32 state in
  case result of 
  None ⇒ None
  | Some s1 ⇒ Some (store_barrier_pending_mod False s1)"

text ‹monad for sequential operations over the register representation›
type_synonym ('a,'e) sparc_state_monad = "(('a) sparc_state,'e) det_monad" 

text ‹Given a word32 value, a cpu register, 
        write the value in the cpu register.›
definition write_cpu :: "word32 ⇒ CPU_register ⇒ ('a,unit) sparc_state_monad"
where "write_cpu w cr ≡
  do
    modify (λs. (cpu_reg_mod w cr s));
    return ()
  od"

definition write_cpu_tt :: "word8 ⇒ ('a,unit) sparc_state_monad"
where "write_cpu_tt w ≡
  do
    tbr_val ← gets (λs. (cpu_reg_val TBR s));
    new_tbr_val ← gets (λs. (write_tt w tbr_val));
    write_cpu new_tbr_val TBR;
    return ()
  od"

text ‹Given a word32 value, a word4 window, a user register, 
        write the value in the user register. 
        N.B. CWP is a 5 bit value, but we only use the last 4 bits,
        since there are only 16 windows.›
definition write_reg :: "word32 ⇒ ('a::len) word ⇒ user_reg_type ⇒ 
  ('a,unit) sparc_state_monad"
where "write_reg w win ur ≡
  do
    modify (λs.(user_reg_mod w win ur s));
    return ()
  od"

definition set_annul :: "bool ⇒ ('a,unit) sparc_state_monad"
where "set_annul b ≡
  do
    modify (λs. (annul_mod b s));
    return ()
  od"

definition set_reset_trap :: "bool ⇒ ('a,unit) sparc_state_monad"
where "set_reset_trap b ≡
  do
    modify (λs. (reset_trap_mod b s));
    return ()
  od"

definition set_exe_mode :: "bool ⇒ ('a,unit) sparc_state_monad"
where "set_exe_mode b ≡
  do
    modify (λs. (exe_mode_mod b s));
    return ()
  od"

definition set_reset_mode :: "bool ⇒ ('a,unit) sparc_state_monad"
where "set_reset_mode b ≡
  do
    modify (λs. (reset_mode_mod b s));
    return ()
  od" 

definition set_err_mode :: "bool ⇒ ('a,unit) sparc_state_monad"
where "set_err_mode b ≡
  do
    modify (λs. (err_mode_mod b s));
    return ()
  od"

fun get_delayed_0 :: "(int × reg_type × CPU_register) list ⇒ 
  (int × reg_type × CPU_register) list"
where
"get_delayed_0 [] = []"
|
"get_delayed_0 (x # xs) = 
  (if fst x = 0 then x # (get_delayed_0 xs)
  else get_delayed_0 xs)"

text ‹Get a list of delayed-writes with delay 0.›
definition get_delayed_write :: "delayed_write_pool ⇒ (int × reg_type × CPU_register) list"
where
"get_delayed_write dwp ≡ get_delayed_0 dwp"

definition delayed_write :: "(int × reg_type × CPU_register) ⇒ ('a) sparc_state ⇒
  ('a) sparc_state"
where "delayed_write dw s ≡
  let (n,v,r) = dw in
  if n = 0 then
    cpu_reg_mod v r s
  else s"

primrec delayed_write_all :: "(int × reg_type × CPU_register) list ⇒
  ('a) sparc_state ⇒ ('a) sparc_state"
where "delayed_write_all [] s = s"
|"delayed_write_all (x # xs) s =
  delayed_write_all xs (delayed_write x s)"

primrec delayed_pool_rm_list :: "(int × reg_type × CPU_register) list⇒ 
  ('a) sparc_state ⇒ ('a) sparc_state"
where "delayed_pool_rm_list [] s = s"
|"delayed_pool_rm_list (x # xs) s =
  delayed_pool_rm_list xs (delayed_pool_rm x s)"

definition delayed_pool_write :: "('a) sparc_state ⇒ ('a) sparc_state"
where "delayed_pool_write s ≡
  let dwp0 = get_delayed_pool s;
      dwp1 = delayed_pool_minus dwp0;
      wl = get_delayed_write dwp1;
      s1 = delayed_write_all wl s;
      s2 = delayed_pool_rm_list wl s1 
  in s2"

definition raise_trap :: "Trap ⇒ ('a,unit) sparc_state_monad"
where "raise_trap t ≡
  do
    modify (λs. (add_trap_set t s));
    return ()
  od"

end

end