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