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_addrarray (addrsel_reg_IP2022 alu) (addr_array_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 ? (getn_array16T x0 ? (call_stack_IP2022 alu)) ]
 166  (alu m t s).
 167
 168 ndefinition pop_call_reg ≝
 169 λm:mcu_type.
 170  match m
 171   return λm.Πt.any_status m t → (option (ProdT word16 (any_status m t))) with
 172  [ HC05 ⇒ λt:memory_impl.λs:any_status HC05 t.None ?
 173  | HC08 ⇒ λt:memory_impl.λs:any_status HC08 t.None ?
 174  | HCS08 ⇒ λt:memory_impl.λs:any_status HCS08 t.None ?
 175  | RS08 ⇒ λt:memory_impl.λs:any_status RS08 t.None ?
 176  | IP2022 ⇒ λt:memory_impl.λs:any_status IP2022 t.
 177   match pop_callstack (call_stack_IP2022 (alu IP2022 t s)) with
 178    [ pair val call' ⇒ Some ? (pair … val
 179     (set_alu IP2022 t s
 180      (mk_alu_IP2022
 181       (acc_low_reg_IP2022 (alu IP2022 t s))
 182       (mulh_reg_IP2022 (alu IP2022 t s))
 183       (addrsel_reg_IP2022 (alu IP2022 t s))
 184       (addr_array_IP2022 (alu IP2022 t s))
 185       call'
 186       (ip_reg_IP2022 (alu IP2022 t s))
 187       (dp_reg_IP2022 (alu IP2022 t s))
 188       (data_reg_IP2022 (alu IP2022 t s))
 189       (sp_reg_IP2022 (alu IP2022 t s))
 190       (pc_reg_IP2022 (alu IP2022 t s))
 191       (speed_reg_IP2022 (alu IP2022 t s))
 192       (page_reg_IP2022 (alu IP2022 t s))
 193       (h_flag_IP2022 (alu IP2022 t s))
 194       (z_flag_IP2022 (alu IP2022 t s))
 195       (c_flag_IP2022 (alu IP2022 t s))
 196       (skip_mode_IP2022 (alu IP2022 t s))))) ]].
 197
 198 (* getter di IP, non esiste sempre *)
 199 ndefinition get_ip_reg ≝
 200 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 201  match m
 202   return aux_get_type (option word16) with
 203  [ HC05 ⇒ λalu.None ?
 204  | HC08 ⇒ λalu.None ?
 205  | HCS08 ⇒ λalu.None ?
 206  | RS08 ⇒ λalu.None ?
 207  | IP2022 ⇒ λalu.Some ? (ip_reg_IP2022 alu) ]
 208  (alu m t s).
 209
 210 (* getter di DP, non esiste sempre *)
 211 ndefinition get_dp_reg ≝
 212 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 213  match m
 214   return aux_get_type (option word16) with
 215  [ HC05 ⇒ λalu.None ?
 216  | HC08 ⇒ λalu.None ?
 217  | HCS08 ⇒ λalu.None ?
 218  | RS08 ⇒ λalu.None ?
 219  | IP2022 ⇒ λalu.Some ? (dp_reg_IP2022 alu) ]
 220  (alu m t s).
 221
 222 (* getter di DATA, non esiste sempre *)
 223 ndefinition get_data_reg ≝
 224 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 225  match m
 226   return aux_get_type (option word16) with
 227  [ HC05 ⇒ λalu.None ?
 228  | HC08 ⇒ λalu.None ?
 229  | HCS08 ⇒ λalu.None ?
 230  | RS08 ⇒ λalu.None ?
 231  | IP2022 ⇒ λalu.Some ? (data_reg_IP2022 alu) ]
 232  (alu m t s).
 233
 234 (* getter di SPEED, non esiste sempre *)
 235 ndefinition get_speed_reg ≝
 236 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 237  match m
 238   return aux_get_type (option exadecim) with
 239  [ HC05 ⇒ λalu.None ?
 240  | HC08 ⇒ λalu.None ?
 241  | HCS08 ⇒ λalu.None ?
 242  | RS08 ⇒ λalu.None ?
 243  | IP2022 ⇒ λalu.Some ? (speed_reg_IP2022 alu) ]
 244  (alu m t s).
 245
 246 (* getter di PAGE, non esiste sempre *)
 247 ndefinition get_page_reg ≝
 248 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 249  match m
 250   return aux_get_type (option oct) with
 251  [ HC05 ⇒ λalu.None ?
 252  | HC08 ⇒ λalu.None ?
 253  | HCS08 ⇒ λalu.None ?
 254  | RS08 ⇒ λalu.None ?
 255  | IP2022 ⇒ λalu.Some ? (page_reg_IP2022 alu) ]
 256  (alu m t s).
 257
 258 (* REGISTRI SPECIALI *)
 259
 260 (* getter di memory mapped X, non esiste sempre *)
 261 ndefinition get_x_map ≝
 262 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 263  match m
 264   return aux_get_type (option byte8) with
 265  [ HC05 ⇒ λalu.None ?
 266  | HC08 ⇒ λalu.None ?
 267  | HCS08 ⇒ λalu.None ?
 268  | RS08 ⇒ λalu.Some ? (x_map_RS08 alu)
 269  | IP2022 ⇒ λalu.None ? ]
 270  (alu m t s).
 271
 272 (* getter di memory mapped PS, non esiste sempre *)
 273 ndefinition get_ps_map ≝
 274 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 275  match m
 276   return aux_get_type (option byte8) with
 277  [ HC05 ⇒ λalu.None ?
 278  | HC08 ⇒ λalu.None ?
 279  | HCS08 ⇒ λalu.None ?
 280  | RS08 ⇒ λalu.Some ? (ps_map_RS08 alu)
 281  | IP2022 ⇒ λalu.None ? ]
 282  (alu m t s).
 283
 284 (* getter di skip mode, non esiste sempre *)
 285 ndefinition get_skip_mode ≝
 286 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 287  match m
 288   return aux_get_type (option bool) with
 289  [ HC05 ⇒ λalu.None ?
 290  | HC08 ⇒ λalu.None ?
 291  | HCS08 ⇒ λalu.None ?
 292  | RS08 ⇒ λalu.None ?
 293  | IP2022 ⇒ λalu.Some ? (skip_mode_IP2022 alu) ]
 294  (alu m t s).
 295
 296 (* FLAG *)
 297
 298 (* getter di V, non esiste sempre *)
 299 ndefinition get_v_flag ≝
 300 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 301  match m
 302   return aux_get_type (option bool) with
 303  [ HC05 ⇒ λalu.None ?
 304  | HC08 ⇒ λalu.Some ? (v_flag_HC08 alu)
 305  | HCS08 ⇒ λalu.Some ? (v_flag_HC08 alu)
 306  | RS08 ⇒ λalu.None ?
 307  | IP2022 ⇒ λalu.None ? ]
 308  (alu m t s).
 309
 310 (* getter di H, non esiste sempre *)
 311 ndefinition get_h_flag ≝
 312 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 313  match m
 314   return aux_get_type (option bool) with
 315  [ HC05 ⇒ λalu.Some ? (h_flag_HC05 alu)
 316  | HC08 ⇒ λalu.Some ? (h_flag_HC08 alu)
 317  | HCS08 ⇒ λalu.Some ? (h_flag_HC08 alu)
 318  | RS08 ⇒ λalu.None ?
 319  | IP2022 ⇒ λalu.Some ? (h_flag_IP2022 alu) ]
 320  (alu m t s).
 321
 322 (* getter di I, non esiste sempre *)
 323 ndefinition get_i_flag ≝
 324 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 325  match m
 326   return aux_get_type (option bool) with
 327  [ HC05 ⇒ λalu.Some ? (i_flag_HC05 alu)
 328  | HC08 ⇒ λalu.Some ? (i_flag_HC08 alu)
 329  | HCS08 ⇒ λalu.Some ? (i_flag_HC08 alu)
 330  | RS08 ⇒ λalu.None ?
 331  | IP2022 ⇒ λalu.None ? ]
 332  (alu m t s).
 333
 334 (* getter di N, non esiste sempre *)
 335 ndefinition get_n_flag ≝
 336 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 337  match m
 338   return aux_get_type (option bool) with
 339  [ HC05 ⇒ λalu.Some ? (n_flag_HC05 alu)
 340  | HC08 ⇒ λalu.Some ? (n_flag_HC08 alu)
 341  | HCS08 ⇒ λalu.Some ? (n_flag_HC08 alu)
 342  | RS08 ⇒ λalu.None ?
 343  | IP2022 ⇒ λalu.None ? ]
 344  (alu m t s).
 345
 346 (* getter di Z, esiste sempre *)
 347 ndefinition get_z_flag ≝
 348 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 349  match m
 350   return aux_get_type bool with
 351  [ HC05 ⇒ z_flag_HC05
 352  | HC08 ⇒ z_flag_HC08
 353  | HCS08 ⇒ z_flag_HC08
 354  | RS08 ⇒ z_flag_RS08
 355  | IP2022 ⇒ z_flag_IP2022 ]
 356  (alu m t s).
 357
 358 (* getter di C, esiste sempre *)
 359 ndefinition get_c_flag ≝
 360 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 361  match m
 362   return aux_get_type bool with
 363  [ HC05 ⇒ c_flag_HC05
 364  | HC08 ⇒ c_flag_HC08
 365  | HCS08 ⇒ c_flag_HC08
 366  | RS08 ⇒ c_flag_RS08
 367  | IP2022 ⇒ c_flag_IP2022 ]
 368  (alu m t s).
 369
 370 (* getter di IRQ, non esiste sempre *)
 371 ndefinition get_irq_flag ≝
 372 λm:mcu_type.λt:memory_impl.λs:any_status m t.
 373  match m
 374   return aux_get_type (option bool) with
 375  [ HC05 ⇒ λalu.Some ? (irq_flag_HC05 alu)
 376  | HC08 ⇒ λalu.Some ? (irq_flag_HC08 alu)
 377  | HCS08 ⇒ λalu.Some ? (irq_flag_HC08 alu)
 378  | RS08 ⇒ λalu.None ?
 379  | IP2022 ⇒ λalu.None ? ]
 380  (alu m t s).