helm/software/matita/contribs/ng_assembly/emulator/status/status_getter.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
  25 (* **************** *)
  26 (* GETTER SPECIFICI *)
  27 (* **************** *)
  28
  29 (* funzione ausiliaria per il tipaggio dei getter *)
  30 ndefinition aux_get_type ≝ λx:Type.λm:mcu_type.match m with
  31  [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08
  32  | IP2022 ⇒ alu_IP2022 ] → x.
  33
  34 (* REGISTRI *)
  35
  36 (* getter di A, esiste sempre *)
  37 ndefinition get_acc_8_low_reg ≝
  38 λm:mcu_type.λt:memory_impl.λs:any_status m t.
  39  match m
  40   return aux_get_type byte8 with
  41  [ HC05 ⇒ acc_low_reg_HC05
  42  | HC08 ⇒ acc_low_reg_HC08
  43  | HCS08 ⇒ acc_low_reg_HC08
  44  | RS08 ⇒ acc_low_reg_RS08
  45  | IP2022 ⇒ acc_low_reg_IP2022 ]
  46  (alu m t s).
  47
  48 (* getter di X, non esiste sempre *)
  49 ndefinition get_indX_8_low_reg ≝
  50 λm:mcu_type.λt:memory_impl.λs:any_status m t.
  51  match m
  52   return aux_get_type (option byte8) with
  53  [ HC05 ⇒ λalu.Some ? (indX_low_reg_HC05 alu)
  54  | HC08 ⇒ λalu.Some ? (indX_low_reg_HC08 alu)
  55  | HCS08 ⇒ λalu.Some ? (indX_low_reg_HC08 alu)
  56  | RS08 ⇒ λalu.None ?
  57  | IP2022 ⇒ λalu.None ? ]
  58  (alu m t s).
  59
  60 (* getter di H, non esiste sempre *)
  61 ndefinition get_indX_8_high_reg ≝
  62 λm:mcu_type.λt:memory_impl.λs:any_status m t.
  63  match m
  64   return aux_get_type (option byte8) with
  65  [ HC05 ⇒ λalu.None ?
  66  | HC08 ⇒ λalu.Some ? (indX_high_reg_HC08 alu)
  67  | HCS08 ⇒ λalu.Some ? (indX_high_reg_HC08 alu)
  68  | RS08 ⇒ λalu.None ?
  69  | IP2022 ⇒ λalu.None ? ]
  70  (alu m t s).
  71
  72 (* getter di H:X, non esiste sempre *)
  73 ndefinition get_indX_16_reg ≝
  74 λm:mcu_type.λt:memory_impl.λs:any_status m t.
  75  match m
  76   return aux_get_type (option word16) with
  77  [ HC05 ⇒ λalu.None ?
  78  | HC08 ⇒ λalu.Some ? (mk_word16 (indX_high_reg_HC08 alu) (indX_low_reg_HC08 alu))
  79  | HCS08 ⇒ λalu.Some ? (mk_word16 (indX_high_reg_HC08 alu) (indX_low_reg_HC08 alu))
  80  | RS08 ⇒ λalu.None ?
  81  | IP2022 ⇒ λalu.None ? ]
  82  (alu m t s).
  83
  84 (* getter di SP, non esiste sempre *)
  85 ndefinition get_sp_reg ≝
  86 λm:mcu_type.λt:memory_impl.λs:any_status m t.
  87  match m
  88   return aux_get_type (option word16) with
  89  [ HC05 ⇒ λalu.Some ? (sp_reg_HC05 alu)
  90  | HC08 ⇒ λalu.Some ? (sp_reg_HC08 alu)
  91  | HCS08 ⇒ λalu.Some ? (sp_reg_HC08 alu)
  92  | RS08 ⇒ λalu.None ?
  93  | IP2022 ⇒ λalu.Some ? (sp_reg_IP2022 alu) ]
  94  (alu m t s).
  95
  96 (* getter di PC, esiste sempre *)
  97 ndefinition get_pc_reg ≝
  98 λm:mcu_type.λt:memory_impl.λs:any_status m t.
  99  match m
 100   return aux_get_type word16 with
 101  [ HC05 ⇒ pc_reg_HC05
 102  | HC08 ⇒ pc_reg_HC08
 103  | HCS08 ⇒ pc_reg_HC08
 104  | RS08 ⇒ pc_reg_RS08
 105  | IP2022 ⇒ pc_reg_IP2022 ]
 106  (alu m t s).
 107
 108 (* getter di SPC, non esiste sempre *)
 109 ndefinition get_spc_reg ≝
 110 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 111  match m
 112   return aux_get_type (option word16) with
 113  [ HC05 ⇒ λalu.None ?
 114  | HC08 ⇒ λalu.None ?
 115  | HCS08 ⇒ λalu.None ?
 116  | RS08 ⇒ λalu.Some ? (spc_reg_RS08 alu)
 117  | IP2022 ⇒ λalu.None ? ]
 118  (alu m t s).
 119
 120 (* getter di MULH, non esiste sempre *)
 121 ndefinition get_mulh_reg ≝
 122 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 123  match m
 124   return aux_get_type (option byte8) with
 125  [ HC05 ⇒ λalu.None ?
 126  | HC08 ⇒ λalu.None ?
 127  | HCS08 ⇒ λalu.None ?
 128  | RS08 ⇒ λalu.None ?
 129  | IP2022 ⇒ λalu.Some ? (mulh_reg_IP2022 alu) ]
 130  (alu m t s).
 131
 132 (* getter di ADDRSEL, non esiste sempre *)
 133 ndefinition get_addrsel_reg ≝
 134 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 135  match m
 136   return aux_get_type (option byte8) with
 137  [ HC05 ⇒ λalu.None ?
 138  | HC08 ⇒ λalu.None ?
 139  | HCS08 ⇒ λalu.None ?
 140  | RS08 ⇒ λalu.None ?
 141  | IP2022 ⇒ λalu.Some ? (addrsel_reg_IP2022 alu) ]
 142  (alu m t s).
 143
 144 (* getter di ADDR, non esiste sempre *)
 145 ndefinition get_addr_reg ≝
 146 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 147  match m
 148   return aux_get_type (option word24) with
 149  [ HC05 ⇒ λalu.None ?
 150  | HC08 ⇒ λalu.None ?
 151  | HCS08 ⇒ λalu.None ?
 152  | RS08 ⇒ λalu.None ?
 153  | IP2022 ⇒ λalu.Some ? (get_addr_reg_IP2022 alu) ]
 154  (alu m t s).
 155
 156 (* getter di CALL, non esiste sempre *)
 157 ndefinition get_call_reg ≝
 158 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 159  match m
 160   return aux_get_type (option word16) with
 161  [ HC05 ⇒ λalu.None ?
 162  | HC08 ⇒ λalu.None ?
 163  | HCS08 ⇒ λalu.None ?
 164  | RS08 ⇒ λalu.None ?
 165  | IP2022 ⇒ λalu.Some ? (get_call_reg_IP2022 alu) ]
 166  (alu m t s).
 167
 168 (* getter di IP, non esiste sempre *)
 169 ndefinition get_ip_reg ≝
 170 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 171  match m
 172   return aux_get_type (option word16) with
 173  [ HC05 ⇒ λalu.None ?
 174  | HC08 ⇒ λalu.None ?
 175  | HCS08 ⇒ λalu.None ?
 176  | RS08 ⇒ λalu.None ?
 177  | IP2022 ⇒ λalu.Some ? (ip_reg_IP2022 alu) ]
 178  (alu m t s).
 179
 180 (* getter di DP, non esiste sempre *)
 181 ndefinition get_dp_reg ≝
 182 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 183  match m
 184   return aux_get_type (option word16) with
 185  [ HC05 ⇒ λalu.None ?
 186  | HC08 ⇒ λalu.None ?
 187  | HCS08 ⇒ λalu.None ?
 188  | RS08 ⇒ λalu.None ?
 189  | IP2022 ⇒ λalu.Some ? (dp_reg_IP2022 alu) ]
 190  (alu m t s).
 191
 192 (* getter di DATA, non esiste sempre *)
 193 ndefinition get_data_reg ≝
 194 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 195  match m
 196   return aux_get_type (option word16) with
 197  [ HC05 ⇒ λalu.None ?
 198  | HC08 ⇒ λalu.None ?
 199  | HCS08 ⇒ λalu.None ?
 200  | RS08 ⇒ λalu.None ?
 201  | IP2022 ⇒ λalu.Some ? (data_reg_IP2022 alu) ]
 202  (alu m t s).
 203
 204 (* getter di SPEED, non esiste sempre *)
 205 ndefinition get_speed_reg ≝
 206 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 207  match m
 208   return aux_get_type (option exadecim) with
 209  [ HC05 ⇒ λalu.None ?
 210  | HC08 ⇒ λalu.None ?
 211  | HCS08 ⇒ λalu.None ?
 212  | RS08 ⇒ λalu.None ?
 213  | IP2022 ⇒ λalu.Some ? (speed_reg_IP2022 alu) ]
 214  (alu m t s).
 215
 216 (* getter di PAGE, non esiste sempre *)
 217 ndefinition get_page_reg ≝
 218 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 219  match m
 220   return aux_get_type (option oct) with
 221  [ HC05 ⇒ λalu.None ?
 222  | HC08 ⇒ λalu.None ?
 223  | HCS08 ⇒ λalu.None ?
 224  | RS08 ⇒ λalu.None ?
 225  | IP2022 ⇒ λalu.Some ? (page_reg_IP2022 alu) ]
 226  (alu m t s).
 227
 228 (* REGISTRI SPECIALI *)
 229
 230 (* getter di memory mapped X, non esiste sempre *)
 231 ndefinition get_x_map ≝
 232 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 233  match m
 234   return aux_get_type (option byte8) with
 235  [ HC05 ⇒ λalu.None ?
 236  | HC08 ⇒ λalu.None ?
 237  | HCS08 ⇒ λalu.None ?
 238  | RS08 ⇒ λalu.Some ? (x_map_RS08 alu)
 239  | IP2022 ⇒ λalu.None ? ]
 240  (alu m t s).
 241
 242 (* getter di memory mapped PS, non esiste sempre *)
 243 ndefinition get_ps_map ≝
 244 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 245  match m
 246   return aux_get_type (option byte8) with
 247  [ HC05 ⇒ λalu.None ?
 248  | HC08 ⇒ λalu.None ?
 249  | HCS08 ⇒ λalu.None ?
 250  | RS08 ⇒ λalu.Some ? (ps_map_RS08 alu)
 251  | IP2022 ⇒ λalu.None ? ]
 252  (alu m t s).
 253
 254 (* getter di skip mode, non esiste sempre *)
 255 ndefinition get_skip_mode ≝
 256 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 257  match m
 258   return aux_get_type (option bool) with
 259  [ HC05 ⇒ λalu.None ?
 260  | HC08 ⇒ λalu.None ?
 261  | HCS08 ⇒ λalu.None ?
 262  | RS08 ⇒ λalu.None ?
 263  | IP2022 ⇒ λalu.Some ? (skip_mode_IP2022 alu) ]
 264  (alu m t s).
 265
 266 (* FLAG *)
 267
 268 (* getter di V, non esiste sempre *)
 269 ndefinition get_v_flag ≝
 270 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 271  match m
 272   return aux_get_type (option bool) with
 273  [ HC05 ⇒ λalu.None ?
 274  | HC08 ⇒ λalu.Some ? (v_flag_HC08 alu)
 275  | HCS08 ⇒ λalu.Some ? (v_flag_HC08 alu)
 276  | RS08 ⇒ λalu.None ?
 277  | IP2022 ⇒ λalu.None ? ]
 278  (alu m t s).
 279
 280 (* getter di H, non esiste sempre *)
 281 ndefinition get_h_flag ≝
 282 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 283  match m
 284   return aux_get_type (option bool) with
 285  [ HC05 ⇒ λalu.Some ? (h_flag_HC05 alu)
 286  | HC08 ⇒ λalu.Some ? (h_flag_HC08 alu)
 287  | HCS08 ⇒ λalu.Some ? (h_flag_HC08 alu)
 288  | RS08 ⇒ λalu.None ?
 289  | IP2022 ⇒ λalu.Some ? (h_flag_IP2022 alu) ]
 290  (alu m t s).
 291
 292 (* getter di I, non esiste sempre *)
 293 ndefinition get_i_flag ≝
 294 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 295  match m
 296   return aux_get_type (option bool) with
 297  [ HC05 ⇒ λalu.Some ? (i_flag_HC05 alu)
 298  | HC08 ⇒ λalu.Some ? (i_flag_HC08 alu)
 299  | HCS08 ⇒ λalu.Some ? (i_flag_HC08 alu)
 300  | RS08 ⇒ λalu.None ?
 301  | IP2022 ⇒ λalu.None ? ]
 302  (alu m t s).
 303
 304 (* getter di N, non esiste sempre *)
 305 ndefinition get_n_flag ≝
 306 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 307  match m
 308   return aux_get_type (option bool) with
 309  [ HC05 ⇒ λalu.Some ? (n_flag_HC05 alu)
 310  | HC08 ⇒ λalu.Some ? (n_flag_HC08 alu)
 311  | HCS08 ⇒ λalu.Some ? (n_flag_HC08 alu)
 312  | RS08 ⇒ λalu.None ?
 313  | IP2022 ⇒ λalu.None ? ]
 314  (alu m t s).
 315
 316 (* getter di Z, esiste sempre *)
 317 ndefinition get_z_flag ≝
 318 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 319  match m
 320   return aux_get_type bool with
 321  [ HC05 ⇒ z_flag_HC05
 322  | HC08 ⇒ z_flag_HC08
 323  | HCS08 ⇒ z_flag_HC08
 324  | RS08 ⇒ z_flag_RS08
 325  | IP2022 ⇒ z_flag_IP2022 ]
 326  (alu m t s).
 327
 328 (* getter di C, esiste sempre *)
 329 ndefinition get_c_flag ≝
 330 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 331  match m
 332   return aux_get_type bool with
 333  [ HC05 ⇒ c_flag_HC05
 334  | HC08 ⇒ c_flag_HC08
 335  | HCS08 ⇒ c_flag_HC08
 336  | RS08 ⇒ c_flag_RS08
 337  | IP2022 ⇒ c_flag_IP2022 ]
 338  (alu m t s).
 339
 340 (* getter di IRQ, non esiste sempre *)
 341 ndefinition get_irq_flag ≝
 342 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 343  match m
 344   return aux_get_type (option bool) with
 345  [ HC05 ⇒ λalu.Some ? (irq_flag_HC05 alu)
 346  | HC08 ⇒ λalu.Some ? (irq_flag_HC08 alu)
 347  | HCS08 ⇒ λalu.Some ? (irq_flag_HC08 alu)
 348  | RS08 ⇒ λalu.None ?
 349  | IP2022 ⇒ λalu.None ? ]
 350  (alu m t s).