matita/matita/contribs/ng_assembly/emulator/read_write/IP2022_read_write.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* ********************************************************************** *)
  16 (*                          Progetto FreeScale                            *)
  17 (*                                                                        *)
  18 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
  19 (*   Sviluppo: 2008-2010                                                  *)
  20 (*                                                                        *)
  21 (* ********************************************************************** *)
  22
  23 include "emulator/status/status_setter.ma".
  24 include "emulator/read_write/read_write_base.ma".
  25
  26 ndefinition IP2022_ADDRSEL_loc ≝ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,x2〉〉〉.
  27 ndefinition IP2022_ADDRX_loc   ≝ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,x3〉〉〉.
  28 ndefinition IP2022_IPH_loc     ≝ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,x4〉〉〉.
  29 ndefinition IP2022_IPL_loc     ≝ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,x5〉〉〉.
  30 ndefinition IP2022_SPH_loc     ≝ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,x6〉〉〉.
  31 ndefinition IP2022_SPL_loc     ≝ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,x7〉〉〉.
  32 ndefinition IP2022_PCH_loc     ≝ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,x8〉〉〉.
  33 ndefinition IP2022_PCL_loc     ≝ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,x9〉〉〉.
  34 ndefinition IP2022_W_loc       ≝ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,xA〉〉〉.
  35 ndefinition IP2022_STATUS_loc  ≝ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,xB〉〉〉.
  36 ndefinition IP2022_DPH_loc     ≝ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,xC〉〉〉.
  37 ndefinition IP2022_DPL_loc     ≝ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,xD〉〉〉.
  38 ndefinition IP2022_SPEED_loc   ≝ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,xE〉〉〉.
  39 ndefinition IP2022_MULH_loc    ≝ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,xF〉〉〉.
  40 ndefinition IP2022_ADDRH_loc   ≝ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x1,x0〉〉〉.
  41 ndefinition IP2022_ADDRL_loc   ≝ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x1,x1〉〉〉.
  42 ndefinition IP2022_DATAH_loc   ≝ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x1,x2〉〉〉.
  43 ndefinition IP2022_DATAL_loc   ≝ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x1,x3〉〉〉.
  44 ndefinition IP2022_CALLH_loc   ≝ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x1,x4〉〉〉.
  45 ndefinition IP2022_CALLL_loc   ≝ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x1,x5〉〉〉.
  46
  47 (* **** *)
  48 (* READ *)
  49 (* **** *)
  50
  51 (* NB: non ci sono strane indirezioni,
  52        solo registri memory mapped da intercettare *)
  53 ndefinition IP2022_memory_filter_read_aux ≝
  54 λt:memory_impl.λs:any_status IP2022 t.λaddr:word32.
  55 λT:Type.λfREG:byte8 → option T.λfMEM:aux_mem_type t → aux_chk_type t → word32 → option T.
  56 (* intercettare le locazioni memory mapped *)
  57  match eq_w32 addr IP2022_ADDRSEL_loc with
  58   [ true ⇒ fREG (addrsel_reg_IP2022 (alu … s))
  59   | false ⇒
  60  match eq_w32 addr IP2022_ADDRX_loc with
  61   [ true ⇒ fREG (w24x (get_addrarray (addrsel_reg_IP2022 (alu … s))
  62                                      (addr_array_IP2022 (alu … s))))
  63   | false ⇒
  64  match eq_w32 addr IP2022_IPH_loc with
  65   [ true ⇒ fREG (cnH ? (ip_reg_IP2022 (alu … s)))
  66   | false ⇒
  67  match eq_w32 addr IP2022_IPL_loc with
  68   [ true ⇒ fREG (cnL ? (ip_reg_IP2022 (alu … s)))
  69   | false ⇒
  70  match eq_w32 addr IP2022_SPH_loc with
  71   [ true ⇒ fREG (cnH ? (sp_reg_IP2022 (alu … s)))
  72   | false ⇒
  73  match eq_w32 addr IP2022_SPL_loc with
  74   [ true ⇒ fREG (cnL ? (sp_reg_IP2022 (alu … s)))
  75   | false ⇒
  76  match eq_w32 addr IP2022_PCH_loc with
  77   [ true ⇒ fREG (cnH ? (pc_reg_IP2022 (alu … s)))
  78   | false ⇒
  79  match eq_w32 addr IP2022_PCL_loc with
  80   [ true ⇒ fREG (cnL ? (pc_reg_IP2022 (alu … s)))
  81   | false ⇒
  82  match eq_w32 addr IP2022_W_loc with
  83   [ true ⇒ fREG (acc_low_reg_IP2022 (alu … s))
  84   | false ⇒
  85  (* PAGE[7:5] Z[2] H[1] C [0] *)
  86  match eq_w32 addr IP2022_STATUS_loc with
  87   [ true ⇒ fREG 〈(rol_ex (ex_of_oct (page_reg_IP2022 (alu … s)))),
  88                  (or_ex (or_ex (match z_flag_IP2022 (alu … s) with
  89                                  [ true ⇒ x4 | false ⇒ x0 ])
  90                                (match h_flag_IP2022 (alu … s) with
  91                                  [ true ⇒ x2 | false ⇒ x0 ]))
  92                         (match c_flag_IP2022 (alu … s) with
  93                           [ true ⇒ x1 | false ⇒ x0 ]))〉
  94   | false ⇒
  95  match eq_w32 addr IP2022_DPH_loc with
  96   [ true ⇒ fREG (cnH ? (dp_reg_IP2022 (alu … s)))
  97   | false ⇒
  98  match eq_w32 addr IP2022_DPL_loc with
  99   [ true ⇒ fREG (cnL ? (dp_reg_IP2022 (alu … s)))
 100   | false ⇒
 101  (* SPEED[3:0] *)
 102  match eq_w32 addr IP2022_SPEED_loc with
 103   [ true ⇒ fREG 〈x0,(speed_reg_IP2022 (alu … s))〉
 104   | false ⇒
 105  match eq_w32 addr IP2022_MULH_loc with
 106   [ true ⇒ fREG (mulh_reg_IP2022 (alu … s))
 107   | false ⇒
 108  match eq_w32 addr IP2022_ADDRH_loc with
 109   [ true ⇒ fREG (w24h (get_addrarray (addrsel_reg_IP2022 (alu … s))
 110                                      (addr_array_IP2022 (alu … s))))
 111   | false ⇒
 112  match eq_w32 addr IP2022_ADDRL_loc with
 113   [ true ⇒ fREG (w24l (get_addrarray (addrsel_reg_IP2022 (alu … s))
 114                                      (addr_array_IP2022 (alu … s))))
 115   | false ⇒
 116  match eq_w32 addr IP2022_DATAH_loc with
 117   [ true ⇒ fREG (cnH ? (data_reg_IP2022 (alu … s)))
 118   | false ⇒
 119  match eq_w32 addr IP2022_DATAL_loc with
 120   [ true ⇒ fREG (cnL ? (data_reg_IP2022 (alu … s)))
 121   | false ⇒
 122  match eq_w32 addr IP2022_CALLH_loc with
 123   [ true ⇒ fREG (cnH ? (getn_array16T x0 ? (call_stack_IP2022 (alu … s))))
 124   | false ⇒
 125  match eq_w32 addr IP2022_CALLL_loc with
 126   [ true ⇒ fREG (cnL ? (getn_array16T x0 ? (call_stack_IP2022 (alu … s))))
 127 (* accesso normale *)
 128   | false ⇒ fMEM (mem_desc … s) (chk_desc … s) addr
 129   ]]]]]]]]]]]]]]]]]]]].
 130
 131 (* lettura IP2022 di un byte *)
 132 ndefinition IP2022_memory_filter_read ≝
 133 λt:memory_impl.λs:any_status IP2022 t.λaddr:word32.
 134  IP2022_memory_filter_read_aux t s addr byte8
 135   (λb.Some byte8 b)
 136   (λm:aux_mem_type t.λc:aux_chk_type t.λa:word32.mem_read t m c a).
 137
 138 (* lettura IP2022 di un bit *)
 139 ndefinition IP2022_memory_filter_read_bit ≝
 140 λt:memory_impl.λs:any_status IP2022 t.λaddr:word32.λsub:oct.
 141  IP2022_memory_filter_read_aux t s addr bool
 142   (λb.Some bool (getn_array8T sub bool (bits_of_byte8 b)))
 143   (λm:aux_mem_type t.λc:aux_chk_type t.λa:word32.mem_read_bit t m c a sub).
 144
 145 (* ***** *)
 146 (* WRITE *)
 147 (* ***** *)
 148
 149 ndefinition high_write_aux_w16 ≝
 150 λf:byte8 → byte8.λw:word16.〈(f (cnH ? w)):(cnL ? w)〉.
 151
 152 ndefinition lowc_write_aux_w16 ≝
 153 λf:byte8 → byte8.λw:word16.λflag:aux_mod_type.
 154  〈((match flag with
 155     [ auxMode_ok ⇒ λx.x
 156     | auxMode_inc ⇒ succ_b8
 157     | auxMode_dec ⇒ pred_b8 ]) (cnH ? w)):
 158   (f (cnL ? w))〉.
 159
 160 ndefinition lownc_write_aux_w16 ≝
 161 λf:byte8 → byte8.λw:word16.〈(cnH ? w):(f (cnL ? w))〉.
 162
 163 ndefinition ext_write_aux_w24 ≝
 164 λf:byte8 → byte8.λw:word24.〈(f (w24x w));(w24h w);(w24l w)〉.
 165
 166 ndefinition high_write_aux_w24 ≝
 167 λf:byte8 → byte8.λw:word24.〈(w24x w);(f (w24h w));(w24l w)〉.
 168
 169 ndefinition low_write_aux_w24 ≝
 170 λf:byte8 → byte8.λw:word24.λflag:aux_mod_type.
 171  match (match flag with
 172          [ auxMode_ok ⇒ λx.x
 173          | auxMode_inc ⇒ succ_w16
 174          | auxMode_dec ⇒ pred_w16 ]) 〈(w24x w):(w24h w)〉 with
 175   [ mk_comp_num wx' wh' ⇒ 〈wx';wh';(w24l w)〉 ].
 176
 177 (* flag di carry: riportare il carry al byte logicamente superiore *)
 178 (* modifica di pc: non inserita nella stato ma postposta *)
 179 ndefinition IP2022_memory_filter_write_aux ≝
 180 λt:memory_impl.λs:any_status IP2022 t.λaddr:word32.λflag:aux_mod_type.
 181 λfREG:byte8 → byte8.λfMEM:aux_mem_type t → aux_chk_type t → word32 → option (aux_mem_type t).
 182 (* intercettare le locazioni memory mapped *)
 183  match eq_w32 addr IP2022_ADDRSEL_loc with
 184   [ true ⇒ set_addrsel_reg … s (fREG (addrsel_reg_IP2022 (alu … s)))
 185   | false ⇒
 186  match eq_w32 addr IP2022_ADDRX_loc with
 187   [ true ⇒ set_addr_reg … s (ext_write_aux_w24 fREG (get_addrarray (addrsel_reg_IP2022 (alu … s))
 188                                                                    (addr_array_IP2022 (alu … s))))
 189   | false ⇒
 190  match eq_w32 addr IP2022_IPH_loc with
 191   [ true ⇒ set_ip_reg … s (high_write_aux_w16 fREG (ip_reg_IP2022 (alu … s)))
 192   | false ⇒
 193  match eq_w32 addr IP2022_IPL_loc with
 194   [ true ⇒ set_ip_reg … s (lowc_write_aux_w16 fREG (ip_reg_IP2022 (alu … s)) flag)
 195   | false ⇒
 196  match eq_w32 addr IP2022_SPH_loc with
 197   [ true ⇒ set_sp_reg … s (high_write_aux_w16 fREG (sp_reg_IP2022 (alu … s)))
 198   | false ⇒
 199  match eq_w32 addr IP2022_SPL_loc with
 200   [ true ⇒ set_sp_reg … s (lowc_write_aux_w16 fREG (sp_reg_IP2022 (alu … s)) flag)
 201   | false ⇒
 202  match eq_w32 addr IP2022_PCL_loc with
 203   [ true ⇒ Some ? (set_pc_reg … s (lowc_write_aux_w16 fREG (pc_reg_IP2022 (alu … s)) flag))
 204   | false ⇒
 205  match eq_w32 addr IP2022_W_loc with
 206   [ true ⇒ Some ? (set_acc_8_low_reg … s (fREG (acc_low_reg_IP2022 (alu … s))))
 207   | false ⇒
 208  match eq_w32 addr IP2022_DPH_loc with
 209   [ true ⇒ set_dp_reg … s (high_write_aux_w16 fREG (dp_reg_IP2022 (alu … s)))
 210   | false ⇒
 211  match eq_w32 addr IP2022_DPL_loc with
 212   [ true ⇒ set_dp_reg … s (lowc_write_aux_w16 fREG (dp_reg_IP2022 (alu … s)) flag)
 213   | false ⇒
 214  match eq_w32 addr IP2022_MULH_loc with
 215   [ true ⇒ set_mulh_reg … s (fREG (mulh_reg_IP2022 (alu … s)))
 216   | false ⇒
 217  match eq_w32 addr IP2022_ADDRH_loc with
 218   [ true ⇒ set_addr_reg … s (high_write_aux_w24 fREG (get_addrarray (addrsel_reg_IP2022 (alu … s))
 219                                                                     (addr_array_IP2022 (alu … s))))
 220   | false ⇒
 221  match eq_w32 addr IP2022_ADDRL_loc with
 222   [ true ⇒ set_addr_reg … s (low_write_aux_w24 fREG (get_addrarray (addrsel_reg_IP2022 (alu … s))
 223                                                                    (addr_array_IP2022 (alu … s))) flag)
 224   | false ⇒
 225  match eq_w32 addr IP2022_DATAH_loc with
 226   [ true ⇒ set_data_reg … s (high_write_aux_w16 fREG (data_reg_IP2022 (alu … s)))
 227   | false ⇒
 228 (* nessun riporto automatico *)
 229  match eq_w32 addr IP2022_DATAL_loc with
 230   [ true ⇒ set_data_reg … s (lownc_write_aux_w16 fREG (data_reg_IP2022 (alu … s)))
 231   | false ⇒
 232  match eq_w32 addr IP2022_CALLH_loc with
 233   [ true ⇒ set_call_reg … s (high_write_aux_w16 fREG (getn_array16T x0 ? (call_stack_IP2022 (alu … s))))
 234   | false ⇒
 235 (* nessun riporto automatico *)
 236  match eq_w32 addr IP2022_CALLL_loc with
 237   [ true ⇒ set_call_reg … s (lownc_write_aux_w16 fREG (getn_array16T x0 ? (call_stack_IP2022 (alu … s))))
 238 (* accesso normale *)
 239   | false ⇒ opt_map … (fMEM (mem_desc … s) (chk_desc … s) addr)
 240              (λmem'.Some ? (set_mem_desc … s mem'))
 241   ]]]]]]]]]]]]]]]]].
 242
 243 (* scrittura IP2022 di un byte *)
 244 ndefinition IP2022_memory_filter_write ≝
 245 λt:memory_impl.λs:any_status IP2022 t.
 246 λaddr:word32.λflag:aux_mod_type.λval:byte8.
 247  (* PAGE[7:5] Z[2] H[1] C [0] *)
 248  match eq_w32 addr IP2022_STATUS_loc with
 249   [ true ⇒ Some ?
 250             (set_alu … s
 251              (set_page_reg_IP2022
 252               (set_z_flag_IP2022
 253                (set_h_flag_IP2022
 254                 (set_c_flag_IP2022 (alu … s)
 255                  (getn_array8T o7 ? (bits_of_byte8 val)))
 256                 (getn_array8T o6 ? (bits_of_byte8 val)))
 257                (getn_array8T o5 ? (bits_of_byte8 val)))
 258               (oct_of_exH (cnH ? val))))
 259  (* accesso a registro_non_spezzato/normale *)
 260   | false ⇒ IP2022_memory_filter_write_aux t s addr flag
 261              (λb.val)
 262              (λm:aux_mem_type t.λc:aux_chk_type t.λa:word32.mem_update t m c a val) ].
 263
 264 (* scrittura IP2022 di un bit *)
 265 ndefinition IP2022_memory_filter_write_bit ≝
 266 λt:memory_impl.λs:any_status IP2022 t.
 267 λaddr:word32.λsub:oct.λval:bool.
 268  (* PAGE[7:5] Z[2] H[1] C [0] *)
 269  match eq_w32 addr IP2022_STATUS_loc with
 270   [ true ⇒ Some ? (set_alu … s
 271    (match sub with
 272      [ o0 ⇒ set_page_reg_IP2022 (alu … s)
 273                                 ((match val with [ true ⇒ or_oct o4 | false ⇒ and_oct o3 ])
 274                                   (page_reg_IP2022 (alu … s)))
 275      | o1 ⇒ set_page_reg_IP2022 (alu … s)
 276                                 ((match val with [ true ⇒ or_oct o2 | false ⇒ and_oct o5 ])
 277                                   (page_reg_IP2022 (alu … s)))
 278      | o2 ⇒ set_page_reg_IP2022 (alu … s)
 279                                 ((match val with [ true ⇒ or_oct o1 | false ⇒ and_oct o6 ])
 280                                   (page_reg_IP2022 (alu … s)))
 281      | o5 ⇒ set_z_flag_IP2022 (alu … s) val
 282      | o6 ⇒ set_h_flag_IP2022 (alu … s) val
 283      | o7 ⇒ set_c_flag_IP2022 (alu … s) val
 284      | _ ⇒ alu … s ]))
 285  (* accesso a registro_non_spezzato/normale *)
 286   | false ⇒ IP2022_memory_filter_write_aux t s addr auxMode_ok
 287              (λb.byte8_of_bits (setn_array8T sub bool (bits_of_byte8 b) val))
 288              (λm:aux_mem_type t.λc:aux_chk_type t.λa:word32.mem_update_bit t m c a sub val) ].