matitaB/matita/contribs/ng_assembly2/emulator/status/status_setter.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.ma".
  24
  25 (* ***************************** *)
  26 (* SETTER SPECIFICI FORTI/DEBOLI *)
  27 (* ***************************** *)
  28
  29 (* funzione ausiliaria per il tipaggio dei setter forti *)
  30 ndefinition aux_set_type ≝ λT:Type.λm:mcu_type.aux_alu_type m → T → aux_alu_type m.
  31
  32 (* funzione ausiliaria per il tipaggio dei setter deboli *)
  33 ndefinition aux_set_type_opt ≝ λT:Type.λm:mcu_type.option (aux_set_type T m).
  34
  35 (* DESCRITTORI ESTERNI ALLA ALU *)
  36
  37 (* setter forte della ALU *)
  38 ndefinition set_alu ≝
  39 λm:mcu_type.λt:memory_impl.λs:any_status m t.λalu'.
  40  mk_any_status … alu' (mem_desc … s) (chk_desc … s) (clk_desc … s).
  41
  42 (* setter forte della memoria *)
  43 ndefinition set_mem_desc ≝
  44 λm:mcu_type.λt:memory_impl.λs:any_status m t.λmem':aux_mem_type t.
  45  mk_any_status … (alu … s) mem' (chk_desc … s) (clk_desc … s).
  46
  47 (* setter forte del descrittore *)
  48 ndefinition set_chk_desc ≝
  49 λm:mcu_type.λt:memory_impl.λs:any_status m t.λchk':aux_chk_type t.
  50  mk_any_status … (alu … s) (mem_desc … s) chk' (clk_desc … s).
  51
  52 (* setter forte del clik *)
  53 ndefinition set_clk_desc ≝
  54 λm:mcu_type.λt:memory_impl.λs:any_status m t.λclk':option (aux_clk_type m).
  55  mk_any_status … (alu … s) (mem_desc … s) (chk_desc … s) clk'.
  56
  57 (* REGISTRO A *)
  58
  59 (* setter forte di A *)
  60 ndefinition set_acc_8_low_reg ≝
  61 λm:mcu_type.λt:memory_impl.λs:any_status m t.λval:byte8.
  62  set_alu … s
  63  (match m return aux_set_type byte8 with
  64   [ HC05 ⇒ set_acc_8_low_reg_HC05
  65   | HC08 ⇒ set_acc_8_low_reg_HC08
  66   | HCS08 ⇒ set_acc_8_low_reg_HC08
  67   | RS08 ⇒ set_acc_8_low_reg_RS08
  68   | IP2022 ⇒ set_acc_8_low_reg_IP2022
  69   ] (alu … s) val).
  70
  71 (* REGISTRO X *)
  72
  73 ndefinition set_indX_8_low_reg_sHC05 ≝
  74 λt:memory_impl.λs:any_status HC05 t.λval.
  75  set_alu … s (set_indX_8_low_reg_HC05 (alu … s) val).
  76
  77 ndefinition set_indX_8_low_reg_sHC08 ≝
  78 λt:memory_impl.λs:any_status HC08 t.λval.
  79  set_alu … s (set_indX_8_low_reg_HC08 (alu … s) val).
  80
  81 ndefinition set_indX_8_low_reg_sHCS08 ≝
  82 λt:memory_impl.λs:any_status HCS08 t.λval.
  83  set_alu … s (set_indX_8_low_reg_HC08 (alu … s) val).
  84
  85 (* setter forte di X *)
  86 ndefinition set_indX_8_low_reg ≝
  87 λm:mcu_type.λt.
  88  match m
  89   return λm.any_status m t → byte8 → option (any_status m t)
  90  with
  91   [ HC05 ⇒ λs:any_status ? t.λval.Some ? (set_indX_8_low_reg_sHC05 t s val)
  92   | HC08 ⇒ λs:any_status ? t.λval.Some ? (set_indX_8_low_reg_sHC08 t s val)
  93   | HCS08 ⇒ λs:any_status ? t.λval.Some ? (set_indX_8_low_reg_sHCS08 t s val)
  94   | RS08 ⇒ λs:any_status ? t.λval.None ?
  95   | IP2022 ⇒ λs:any_status ? t.λval.None ?
  96   ].
  97
  98 (* setter debole di X *)
  99 ndefinition setweak_indX_8_low_reg ≝
 100 λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
 101  match set_indX_8_low_reg … s val with
 102   [ None ⇒ s | Some s' ⇒ s' ].
 103
 104 (* REGISTRO H *)
 105
 106 ndefinition set_indX_8_high_reg_sHC08 ≝
 107 λt:memory_impl.λs:any_status HC08 t.λval.
 108  set_alu … s (set_indX_8_high_reg_HC08 (alu … s) val).
 109
 110 ndefinition set_indX_8_high_reg_sHCS08 ≝
 111 λt:memory_impl.λs:any_status HCS08 t.λval.
 112  set_alu … s (set_indX_8_high_reg_HC08 (alu … s) val).
 113
 114 (* setter forte di H *)
 115 ndefinition set_indX_8_high_reg ≝
 116 λm:mcu_type.λt.
 117  match m
 118   return λm.any_status m t → byte8 → option (any_status m t)
 119  with
 120   [ HC05 ⇒ λs:any_status ? t.λval.None ?
 121   | HC08 ⇒ λs:any_status ? t.λval.Some ? (set_indX_8_high_reg_sHC08 t s val)
 122   | HCS08 ⇒ λs:any_status ? t.λval.Some ? (set_indX_8_high_reg_sHCS08 t s val)
 123   | RS08 ⇒ λs:any_status ? t.λval.None ?
 124   | IP2022 ⇒ λs:any_status ? t.λval.None ?
 125   ].
 126
 127 (* setter debole di H *)
 128 ndefinition setweak_indX_8_high_reg ≝
 129 λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
 130  match set_indX_8_high_reg … s val with
 131   [ None ⇒ s | Some s' ⇒ s' ].
 132
 133 (* REGISTRO H:X *)
 134
 135 ndefinition set_indX_16_reg_sHC08 ≝
 136 λt:memory_impl.λs:any_status HC08 t.λval.
 137  set_alu … s (set_indX_16_reg_HC08 (alu … s) val).
 138
 139 ndefinition set_indX_16_reg_sHCS08 ≝
 140 λt:memory_impl.λs:any_status HCS08 t.λval.
 141  set_alu … s (set_indX_16_reg_HC08 (alu … s) val).
 142
 143 (* setter forte di H:X *)
 144 ndefinition set_indX_16_reg ≝
 145 λm:mcu_type.λt.
 146  match m
 147   return λm.any_status m t → word16 → option (any_status m t)
 148  with
 149   [ HC05 ⇒ λs:any_status ? t.λval.None ?
 150   | HC08 ⇒ λs:any_status ? t.λval.Some ? (set_indX_16_reg_sHC08 t s val)
 151   | HCS08 ⇒ λs:any_status ? t.λval.Some ? (set_indX_16_reg_sHCS08 t s val)
 152   | RS08 ⇒ λs:any_status ? t.λval.None ?
 153   | IP2022 ⇒ λs:any_status ? t.λval.None ?
 154   ].
 155
 156 (* setter debole di H:X *)
 157 ndefinition setweak_indX_16_reg ≝
 158 λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
 159  match set_indX_16_reg … s val with
 160   [ None ⇒ s | Some s' ⇒ s' ].
 161
 162 (* REGISTRO SP *)
 163
 164 ndefinition set_sp_reg_sHC05 ≝
 165 λt:memory_impl.λs:any_status HC05 t.λval.
 166  set_alu … s (set_sp_reg_HC05 (alu … s) val).
 167
 168 ndefinition set_sp_reg_sHC08 ≝
 169 λt:memory_impl.λs:any_status HC08 t.λval.
 170  set_alu … s (set_sp_reg_HC08 (alu … s) val).
 171
 172 ndefinition set_sp_reg_sHCS08 ≝
 173 λt:memory_impl.λs:any_status HCS08 t.λval.
 174  set_alu … s (set_sp_reg_HC08 (alu … s) val).
 175
 176 ndefinition set_sp_reg_sIP2022 ≝
 177 λt:memory_impl.λs:any_status IP2022 t.λval.
 178  set_alu … s (set_sp_reg_IP2022 (alu … s) val).
 179
 180 (* setter forte di SP *)
 181 ndefinition set_sp_reg ≝
 182 λm:mcu_type.λt.
 183  match m
 184   return λm.any_status m t → word16 → option (any_status m t)
 185  with
 186   [ HC05 ⇒ λs:any_status ? t.λval.Some ? (set_sp_reg_sHC05 t s val)
 187   | HC08 ⇒ λs:any_status ? t.λval.Some ? (set_sp_reg_sHC08 t s val)
 188   | HCS08 ⇒ λs:any_status ? t.λval.Some ? (set_sp_reg_sHCS08 t s val)
 189   | RS08 ⇒ λs:any_status ? t.λval.None ?
 190   | IP2022 ⇒ λs:any_status ? t.λval.Some ? (set_sp_reg_sIP2022 t s val)
 191   ].
 192
 193 (* setter debole di SP *)
 194 ndefinition setweak_sp_reg ≝
 195 λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
 196  match set_sp_reg … s val with
 197   [ None ⇒ s | Some s' ⇒ s' ].
 198
 199 (* REGISTRO PC *)
 200
 201 (* setter forte di PC *)
 202 ndefinition set_pc_reg ≝
 203 λm:mcu_type.λt:memory_impl.λs:any_status m t.λpc':word16.
 204  set_alu … s
 205  (match m return aux_set_type word16 with
 206   [ HC05 ⇒ set_pc_reg_HC05
 207   | HC08 ⇒ set_pc_reg_HC08
 208   | HCS08 ⇒ set_pc_reg_HC08
 209   | RS08 ⇒ set_pc_reg_RS08
 210   | IP2022 ⇒ set_pc_reg_IP2022
 211   ] (alu … s) pc').
 212
 213 (* REGISTRO SPC *)
 214
 215 ndefinition set_spc_reg_sRS08 ≝
 216 λt:memory_impl.λs:any_status RS08 t.λval.
 217  set_alu … s (set_spc_reg_RS08 (alu … s) val).
 218
 219 (* setter forte di SPC *)
 220 ndefinition set_spc_reg ≝
 221 λm:mcu_type.λt.
 222  match m
 223   return λm.any_status m t → word16 → option (any_status m t)
 224  with
 225   [ HC05 ⇒ λs:any_status ? t.λval.None ?
 226   | HC08 ⇒ λs:any_status ? t.λval.None ?
 227   | HCS08 ⇒ λs:any_status ? t.λval.None ?
 228   | RS08 ⇒ λs:any_status ? t.λval.Some ? (set_spc_reg_sRS08 t s val)
 229   | IP2022 ⇒ λs:any_status ? t.λval.None ?
 230   ].
 231
 232 (* setter debole di SPC *)
 233 ndefinition setweak_spc_reg ≝
 234 λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
 235  match set_spc_reg … s val with
 236   [ None ⇒ s | Some s' ⇒ s' ].
 237
 238 (* REGISTRO MULH *)
 239
 240 ndefinition set_mulh_reg_sIP2022 ≝
 241 λt:memory_impl.λs:any_status IP2022 t.λval.
 242  set_alu … s (set_mulh_reg_IP2022 (alu … s) val).
 243
 244 (* setter forte di MULH *)
 245 ndefinition set_mulh_reg ≝
 246 λm:mcu_type.λt.
 247  match m
 248   return λm.any_status m t → byte8 → option (any_status m t)
 249  with
 250   [ HC05 ⇒ λs:any_status ? t.λval.None ?
 251   | HC08 ⇒ λs:any_status ? t.λval.None ?
 252   | HCS08 ⇒ λs:any_status ? t.λval.None ?
 253   | RS08 ⇒ λs:any_status ? t.λval.None ?
 254   | IP2022 ⇒ λs:any_status ? t.λval.Some ? (set_mulh_reg_sIP2022 t s val)
 255   ].
 256
 257 (* setter debole di MULH *)
 258 ndefinition setweak_mulh_reg ≝
 259 λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
 260  match set_mulh_reg … s val with
 261   [ None ⇒ s | Some s' ⇒ s' ].
 262
 263 (* REGISTRO ADDRSEL *)
 264
 265 ndefinition set_addrsel_reg_sIP2022 ≝
 266 λt:memory_impl.λs:any_status IP2022 t.λval.
 267  set_alu … s (set_addrsel_reg_IP2022 (alu … s) val).
 268
 269 (* setter forte di ADDRSEL *)
 270 ndefinition set_addrsel_reg ≝
 271 λm:mcu_type.λt.
 272  match m
 273   return λm.any_status m t → byte8 → option (any_status m t)
 274  with
 275   [ HC05 ⇒ λs:any_status ? t.λval.None ?
 276   | HC08 ⇒ λs:any_status ? t.λval.None ?
 277   | HCS08 ⇒ λs:any_status ? t.λval.None ?
 278   | RS08 ⇒ λs:any_status ? t.λval.None ?
 279   | IP2022 ⇒ λs:any_status ? t.λval.Some ? (set_addrsel_reg_sIP2022 t s val)
 280   ].
 281
 282 (* setter debole di ADDRSEL *)
 283 ndefinition setweak_addrsel_reg ≝
 284 λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
 285  match set_addrsel_reg … s val with
 286   [ None ⇒ s | Some s' ⇒ s' ].
 287
 288 (* REGISTRO ADDR *)
 289
 290 ndefinition set_addr_reg_sIP2022 ≝
 291 λt:memory_impl.λs:any_status IP2022 t.λval.
 292  set_alu … s (set_addr_reg_IP2022 (alu … s) val).
 293
 294 (* setter forte di ADDR *)
 295 ndefinition set_addr_reg ≝
 296 λm:mcu_type.λt.
 297  match m
 298   return λm.any_status m t → word24 → option (any_status m t)
 299  with
 300   [ HC05 ⇒ λs:any_status ? t.λval.None ?
 301   | HC08 ⇒ λs:any_status ? t.λval.None ?
 302   | HCS08 ⇒ λs:any_status ? t.λval.None ?
 303   | RS08 ⇒ λs:any_status ? t.λval.None ?
 304   | IP2022 ⇒ λs:any_status ? t.λval.Some ? (set_addr_reg_sIP2022 t s val)
 305   ].
 306
 307 (* setter debole di ADDR *)
 308 ndefinition setweak_addr_reg ≝
 309 λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
 310  match set_addr_reg … s val with
 311   [ None ⇒ s | Some s' ⇒ s' ].
 312
 313 (* REGISTRO CALL *)
 314
 315 ndefinition set_call_reg_sIP2022 ≝
 316 λt:memory_impl.λs:any_status IP2022 t.λval.
 317  set_alu … s (set_call_reg_IP2022 (alu … s) val).
 318
 319 (* setter forte di CALL *)
 320 ndefinition set_call_reg ≝
 321 λm:mcu_type.λt.
 322  match m
 323   return λm.any_status m t → word16 → option (any_status m t)
 324  with
 325   [ HC05 ⇒ λs:any_status ? t.λval.None ?
 326   | HC08 ⇒ λs:any_status ? t.λval.None ?
 327   | HCS08 ⇒ λs:any_status ? t.λval.None ?
 328   | RS08 ⇒ λs:any_status ? t.λval.None ?
 329   | IP2022 ⇒ λs:any_status ? t.λval.Some ? (set_call_reg_sIP2022 t s val)
 330   ].
 331
 332 (* setter debole di CALL *)
 333 ndefinition setweak_call_reg ≝
 334 λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
 335  match set_call_reg … s val with
 336   [ None ⇒ s | Some s' ⇒ s' ].
 337
 338 (* REGISTRO CALL [push] *)
 339
 340 ndefinition push_call_reg_sIP2022 ≝
 341 λt:memory_impl.λs:any_status IP2022 t.λval.
 342  set_alu … s (push_call_reg_IP2022 (alu … s) val).
 343
 344 (* push forte di CALL *)
 345 ndefinition push_call_reg ≝
 346 λm:mcu_type.λt.
 347  match m
 348   return λm.any_status m t → word16 → option (any_status m t)
 349  with
 350   [ HC05 ⇒ λs:any_status ? t.λval.None ?
 351   | HC08 ⇒ λs:any_status ? t.λval.None ?
 352   | HCS08 ⇒ λs:any_status ? t.λval.None ?
 353   | RS08 ⇒ λs:any_status ? t.λval.None ?
 354   | IP2022 ⇒ λs:any_status ? t.λval.Some ? (push_call_reg_sIP2022 t s val)
 355   ].
 356
 357 (* REGISTRO CALL [pop] *)
 358
 359 ndefinition pop_call_reg_sIP2022 ≝
 360 λt:memory_impl.λs:any_status IP2022 t.
 361  match pop_call_reg_IP2022 (alu … s) with
 362   [ pair val alu' ⇒ pair … val (set_alu … s alu') ].
 363
 364 (* pop forte di CALL *)
 365 ndefinition pop_call_reg ≝
 366 λm:mcu_type.λt.
 367  match m
 368   return λm.any_status m t → option (ProdT word16 (any_status m t))
 369  with
 370   [ HC05 ⇒ λs:any_status ? t.None ?
 371   | HC08 ⇒ λs:any_status ? t.None ?
 372   | HCS08 ⇒ λs:any_status ? t.None ?
 373   | RS08 ⇒ λs:any_status ? t.None ?
 374   | IP2022 ⇒ λs:any_status ? t.Some ? (pop_call_reg_sIP2022 t s)
 375   ].
 376
 377 (* REGISTRO IP *)
 378
 379 ndefinition set_ip_reg_sIP2022 ≝
 380 λt:memory_impl.λs:any_status IP2022 t.λval.
 381  set_alu … s (set_ip_reg_IP2022 (alu … s) val).
 382
 383 (* setter forte di IP *)
 384 ndefinition set_ip_reg ≝
 385 λm:mcu_type.λt.
 386  match m
 387   return λm.any_status m t → word16 → option (any_status m t)
 388  with
 389   [ HC05 ⇒ λs:any_status ? t.λval.None ?
 390   | HC08 ⇒ λs:any_status ? t.λval.None ?
 391   | HCS08 ⇒ λs:any_status ? t.λval.None ?
 392   | RS08 ⇒ λs:any_status ? t.λval.None ?
 393   | IP2022 ⇒ λs:any_status ? t.λval.Some ? (set_ip_reg_sIP2022 t s val)
 394   ].
 395
 396 (* setter debole di IP *)
 397 ndefinition setweak_ip_reg ≝
 398 λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
 399  match set_ip_reg … s val with
 400   [ None ⇒ s | Some s' ⇒ s' ].
 401
 402 (* REGISTRO DP *)
 403
 404 ndefinition set_dp_reg_sIP2022 ≝
 405 λt:memory_impl.λs:any_status IP2022 t.λval.
 406  set_alu … s (set_dp_reg_IP2022 (alu … s) val).
 407
 408 (* setter forte di DP *)
 409 ndefinition set_dp_reg ≝
 410 λm:mcu_type.λt.
 411  match m
 412   return λm.any_status m t → word16 → option (any_status m t)
 413  with
 414   [ HC05 ⇒ λs:any_status ? t.λval.None ?
 415   | HC08 ⇒ λs:any_status ? t.λval.None ?
 416   | HCS08 ⇒ λs:any_status ? t.λval.None ?
 417   | RS08 ⇒ λs:any_status ? t.λval.None ?
 418   | IP2022 ⇒ λs:any_status ? t.λval.Some ? (set_dp_reg_sIP2022 t s val)
 419   ].
 420
 421 (* setter debole di DP *)
 422 ndefinition setweak_dp_reg ≝
 423 λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
 424  match set_dp_reg … s val with
 425   [ None ⇒ s | Some s' ⇒ s' ].
 426
 427 (* REGISTRO DATA *)
 428
 429 ndefinition set_data_reg_sIP2022 ≝
 430 λt:memory_impl.λs:any_status IP2022 t.λval.
 431  set_alu … s (set_data_reg_IP2022 (alu … s) val).
 432
 433 (* setter forte di DATA *)
 434 ndefinition set_data_reg ≝
 435 λm:mcu_type.λt.
 436  match m
 437   return λm.any_status m t → word16 → option (any_status m t)
 438  with
 439   [ HC05 ⇒ λs:any_status ? t.λval.None ?
 440   | HC08 ⇒ λs:any_status ? t.λval.None ?
 441   | HCS08 ⇒ λs:any_status ? t.λval.None ?
 442   | RS08 ⇒ λs:any_status ? t.λval.None ?
 443   | IP2022 ⇒ λs:any_status ? t.λval.Some ? (set_data_reg_sIP2022 t s val)
 444   ].
 445
 446 (* setter debole di DATA *)
 447 ndefinition setweak_data_reg ≝
 448 λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
 449  match set_data_reg … s val with
 450   [ None ⇒ s | Some s' ⇒ s' ].
 451
 452 (* REGISTRO SPEED *)
 453
 454 ndefinition set_speed_reg_sIP2022 ≝
 455 λt:memory_impl.λs:any_status IP2022 t.λval.
 456  set_alu … s (set_speed_reg_IP2022 (alu … s) val).
 457
 458 (* setter forte di SPEED *)
 459 ndefinition set_speed_reg ≝
 460 λm:mcu_type.λt.
 461  match m
 462   return λm.any_status m t → exadecim → option (any_status m t)
 463  with
 464   [ HC05 ⇒ λs:any_status ? t.λval.None ?
 465   | HC08 ⇒ λs:any_status ? t.λval.None ?
 466   | HCS08 ⇒ λs:any_status ? t.λval.None ?
 467   | RS08 ⇒ λs:any_status ? t.λval.None ?
 468   | IP2022 ⇒ λs:any_status ? t.λval.Some ? (set_speed_reg_sIP2022 t s val)
 469   ].
 470
 471 (* setter debole di SPEED *)
 472 ndefinition setweak_speed_reg ≝
 473 λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
 474  match set_speed_reg … s val with
 475   [ None ⇒ s | Some s' ⇒ s' ].
 476
 477 (* REGISTRO PAGE *)
 478
 479 ndefinition set_page_reg_sIP2022 ≝
 480 λt:memory_impl.λs:any_status IP2022 t.λval.
 481  set_alu … s (set_page_reg_IP2022 (alu … s) val).
 482
 483 (* setter forte di PAGE *)
 484 ndefinition set_page_reg ≝
 485 λm:mcu_type.λt.
 486  match m
 487   return λm.any_status m t → oct → option (any_status m t)
 488  with
 489   [ HC05 ⇒ λs:any_status ? t.λval.None ?
 490   | HC08 ⇒ λs:any_status ? t.λval.None ?
 491   | HCS08 ⇒ λs:any_status ? t.λval.None ?
 492   | RS08 ⇒ λs:any_status ? t.λval.None ?
 493   | IP2022 ⇒ λs:any_status ? t.λval.Some ? (set_page_reg_sIP2022 t s val)
 494   ].
 495
 496 (* setter debole di PAGE *)
 497 ndefinition setweak_page_reg ≝
 498 λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
 499  match set_page_reg … s val with
 500   [ None ⇒ s | Some s' ⇒ s' ].
 501
 502 (* REGISTRO MEMORY MAPPED X *)
 503
 504 ndefinition set_x_map_sRS08 ≝
 505 λt:memory_impl.λs:any_status RS08 t.λval.
 506  set_alu … s (set_x_map_RS08 (alu … s) val).
 507
 508 (* setter forte di memory mapped X *)
 509 ndefinition set_x_map ≝
 510 λm:mcu_type.λt.
 511  match m
 512   return λm.any_status m t → byte8 → option (any_status m t)
 513  with
 514   [ HC05 ⇒ λs:any_status ? t.λval.None ?
 515   | HC08 ⇒ λs:any_status ? t.λval.None ?
 516   | HCS08 ⇒ λs:any_status ? t.λval.None ?
 517   | RS08 ⇒ λs:any_status ? t.λval.Some ? (set_x_map_sRS08 t s val)
 518   | IP2022 ⇒ λs:any_status ? t.λval.None ?
 519   ].
 520
 521 (* setter debole di memory mapped X *)
 522 ndefinition setweak_x_map ≝
 523 λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
 524  match set_x_map … s val with
 525   [ None ⇒ s | Some s' ⇒ s' ].
 526
 527 (* REGISTRO MEMORY MAPPED PS *)
 528
 529 ndefinition set_ps_map_sRS08 ≝
 530 λt:memory_impl.λs:any_status RS08 t.λval.
 531  set_alu … s (set_ps_map_RS08 (alu … s) val).
 532
 533 (* setter forte di memory mapped PS *)
 534 ndefinition set_ps_map ≝
 535 λm:mcu_type.λt.
 536  match m
 537   return λm.any_status m t → byte8 → option (any_status m t)
 538  with
 539   [ HC05 ⇒ λs:any_status ? t.λval.None ?
 540   | HC08 ⇒ λs:any_status ? t.λval.None ?
 541   | HCS08 ⇒ λs:any_status ? t.λval.None ?
 542   | RS08 ⇒ λs:any_status ? t.λval.Some ? (set_ps_map_sRS08 t s val)
 543   | IP2022 ⇒ λs:any_status ? t.λval.None ?
 544   ].
 545
 546 (* setter debole di memory mapped PS *)
 547 ndefinition setweak_ps_map ≝
 548 λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
 549  match set_ps_map … s val with
 550   [ None ⇒ s | Some s' ⇒ s' ].
 551
 552 (* MODALITA SKIP *)
 553
 554 ndefinition set_skip_mode_sIP2022 ≝
 555 λt:memory_impl.λs:any_status IP2022 t.λval.
 556  set_alu … s (set_skip_mode_IP2022 (alu … s) val).
 557
 558 (* setter forte di modalita SKIP *)
 559 ndefinition set_skip_mode ≝
 560 λm:mcu_type.λt.
 561  match m
 562   return λm.any_status m t → bool → option (any_status m t)
 563  with
 564   [ HC05 ⇒ λs:any_status ? t.λval.None ?
 565   | HC08 ⇒ λs:any_status ? t.λval.None ?
 566   | HCS08 ⇒ λs:any_status ? t.λval.None ?
 567   | RS08 ⇒ λs:any_status ? t.λval.None ?
 568   | IP2022 ⇒ λs:any_status ? t.λval.Some ? (set_skip_mode_sIP2022 t s val)
 569   ].
 570
 571 (* setter debole  di SKIP *)
 572 ndefinition setweak_skip_mode ≝
 573 λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
 574  match set_skip_mode … s val with
 575   [ None ⇒ s | Some s' ⇒ s' ].
 576
 577 (* FLAG V *)
 578
 579 ndefinition set_v_flag_sHC08 ≝
 580 λt:memory_impl.λs:any_status HC08 t.λval.
 581  set_alu … s (set_v_flag_HC08 (alu … s) val).
 582
 583 ndefinition set_v_flag_sHCS08 ≝
 584 λt:memory_impl.λs:any_status HCS08 t.λval.
 585  set_alu … s (set_v_flag_HC08 (alu … s) val).
 586
 587 (* setter forte di V *)
 588 ndefinition set_v_flag ≝
 589 λm:mcu_type.λt.
 590  match m
 591   return λm.any_status m t → bool → option (any_status m t)
 592  with
 593   [ HC05 ⇒ λs:any_status ? t.λval.None ?
 594   | HC08 ⇒ λs:any_status ? t.λval.Some ? (set_v_flag_sHC08 t s val)
 595   | HCS08 ⇒ λs:any_status ? t.λval.Some ? (set_v_flag_sHCS08 t s val)
 596   | RS08 ⇒ λs:any_status ? t.λval.None ?
 597   | IP2022 ⇒ λs:any_status ? t.λval.None ?
 598   ].
 599
 600 (* setter debole  di V *)
 601 ndefinition setweak_v_flag ≝
 602 λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
 603  match set_v_flag … s val with
 604   [ None ⇒ s | Some s' ⇒ s' ].
 605
 606 (* FLAG H *)
 607
 608 ndefinition set_h_flag_sHC05 ≝
 609 λt:memory_impl.λs:any_status HC05 t.λval.
 610  set_alu … s (set_h_flag_HC05 (alu … s) val).
 611
 612 ndefinition set_h_flag_sHC08 ≝
 613 λt:memory_impl.λs:any_status HC08 t.λval.
 614  set_alu … s (set_h_flag_HC08 (alu … s) val).
 615
 616 ndefinition set_h_flag_sHCS08 ≝
 617 λt:memory_impl.λs:any_status HCS08 t.λval.
 618  set_alu … s (set_h_flag_HC08 (alu … s) val).
 619
 620 ndefinition set_h_flag_sIP2022 ≝
 621 λt:memory_impl.λs:any_status IP2022 t.λval.
 622  set_alu … s (set_h_flag_IP2022 (alu … s) val).
 623
 624 (* setter forte di H *)
 625 ndefinition set_h_flag ≝
 626 λm:mcu_type.λt.
 627  match m
 628   return λm.any_status m t → bool → option (any_status m t)
 629  with
 630   [ HC05 ⇒ λs:any_status ? t.λval.Some ? (set_h_flag_sHC05 t s val)
 631   | HC08 ⇒ λs:any_status ? t.λval.Some ? (set_h_flag_sHC08 t s val)
 632   | HCS08 ⇒ λs:any_status ? t.λval.Some ? (set_h_flag_sHCS08 t s val)
 633   | RS08 ⇒ λs:any_status ? t.λval.None ?
 634   | IP2022 ⇒ λs:any_status ? t.λval.Some ? (set_h_flag_sIP2022 t s val)
 635   ].
 636
 637 (* setter debole di H *)
 638 ndefinition setweak_h_flag ≝
 639 λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
 640  match set_h_flag … s val with
 641   [ None ⇒ s | Some s' ⇒ s' ].
 642
 643 (* FLAG I *)
 644
 645 ndefinition set_i_flag_sHC05 ≝
 646 λt:memory_impl.λs:any_status HC05 t.λval.
 647  set_alu … s (set_i_flag_HC05 (alu … s) val).
 648
 649 ndefinition set_i_flag_sHC08 ≝
 650 λt:memory_impl.λs:any_status HC08 t.λval.
 651  set_alu … s (set_i_flag_HC08 (alu … s) val).
 652
 653 ndefinition set_i_flag_sHCS08 ≝
 654 λt:memory_impl.λs:any_status HCS08 t.λval.
 655  set_alu … s (set_i_flag_HC08 (alu … s) val).
 656
 657 (* setter forte di I *)
 658 ndefinition set_i_flag ≝
 659 λm:mcu_type.λt.
 660  match m
 661   return λm.any_status m t → bool → option (any_status m t)
 662  with
 663   [ HC05 ⇒ λs:any_status ? t.λval.Some ? (set_i_flag_sHC05 t s val)
 664   | HC08 ⇒ λs:any_status ? t.λval.Some ? (set_i_flag_sHC08 t s val)
 665   | HCS08 ⇒ λs:any_status ? t.λval.Some ? (set_i_flag_sHCS08 t s val)
 666   | RS08 ⇒ λs:any_status ? t.λval.None ?
 667   | IP2022 ⇒ λs:any_status ? t.λval.None ?
 668   ].
 669
 670 (* setter debole di I *)
 671 ndefinition setweak_i_flag ≝
 672 λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
 673  match set_i_flag … s val with
 674   [ None ⇒ s | Some s' ⇒ s' ].
 675
 676 (* FLAG N *)
 677
 678 ndefinition set_n_flag_sHC05 ≝
 679 λt:memory_impl.λs:any_status HC05 t.λval.
 680  set_alu … s (set_n_flag_HC05 (alu … s) val).
 681
 682 ndefinition set_n_flag_sHC08 ≝
 683 λt:memory_impl.λs:any_status HC08 t.λval.
 684  set_alu … s (set_n_flag_HC08 (alu … s) val).
 685
 686 ndefinition set_n_flag_sHCS08 ≝
 687 λt:memory_impl.λs:any_status HCS08 t.λval.
 688  set_alu … s (set_n_flag_HC08 (alu … s) val).
 689
 690 (* setter forte di N *)
 691 ndefinition set_n_flag ≝
 692 λm:mcu_type.λt.
 693  match m
 694   return λm.any_status m t → bool → option (any_status m t)
 695  with
 696   [ HC05 ⇒ λs:any_status ? t.λval.Some ? (set_n_flag_sHC05 t s val)
 697   | HC08 ⇒ λs:any_status ? t.λval.Some ? (set_n_flag_sHC08 t s val)
 698   | HCS08 ⇒ λs:any_status ? t.λval.Some ? (set_n_flag_sHCS08 t s val)
 699   | RS08 ⇒ λs:any_status ? t.λval.None ?
 700   | IP2022 ⇒ λs:any_status ? t.λval.None ?
 701   ].
 702
 703 (* setter debole di N *)
 704 ndefinition setweak_n_flag ≝
 705 λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
 706  match set_n_flag … s val with
 707   [ None ⇒ s | Some s' ⇒ s' ].
 708
 709 (* FLAG Z *)
 710
 711 (* setter forte di Z *)
 712 ndefinition set_z_flag ≝
 713 λm:mcu_type.λt:memory_impl.λs:any_status m t.λzfl':bool.
 714  set_alu m t s
 715  (match m return aux_set_type bool with
 716   [ HC05 ⇒ set_z_flag_HC05
 717   | HC08 ⇒ set_z_flag_HC08
 718   | HCS08 ⇒ set_z_flag_HC08
 719   | RS08 ⇒ set_z_flag_RS08
 720   | IP2022 ⇒ set_z_flag_IP2022
 721   ] (alu m t s) zfl').
 722
 723 (* FLAG C *)
 724
 725 (* setter forte di C *)
 726 ndefinition set_c_flag ≝
 727 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcfl':bool.
 728  set_alu m t s
 729  (match m return aux_set_type bool with
 730   [ HC05 ⇒ set_c_flag_HC05
 731   | HC08 ⇒ set_c_flag_HC08
 732   | HCS08 ⇒ set_c_flag_HC08
 733   | RS08 ⇒ set_c_flag_RS08
 734   | IP2022 ⇒ set_c_flag_IP2022
 735   ] (alu m t s) cfl').
 736
 737 (* FLAG IRQ *)
 738
 739 ndefinition set_irq_flag_sHC05 ≝
 740 λt:memory_impl.λs:any_status HC05 t.λval.
 741  set_alu … s (set_irq_flag_HC05 (alu … s) val).
 742
 743 ndefinition set_irq_flag_sHC08 ≝
 744 λt:memory_impl.λs:any_status HC08 t.λval.
 745  set_alu … s (set_irq_flag_HC08 (alu … s) val).
 746
 747 ndefinition set_irq_flag_sHCS08 ≝
 748 λt:memory_impl.λs:any_status HCS08 t.λval.
 749  set_alu … s (set_irq_flag_HC08 (alu … s) val).
 750
 751 (* setter forte di IRQ *)
 752 ndefinition set_irq_flag ≝
 753 λm:mcu_type.λt.
 754  match m
 755   return λm.any_status m t → bool → option (any_status m t)
 756  with
 757   [ HC05 ⇒ λs:any_status ? t.λval.Some ? (set_irq_flag_sHC05 t s val)
 758   | HC08 ⇒ λs:any_status ? t.λval.Some ? (set_irq_flag_sHC08 t s val)
 759   | HCS08 ⇒ λs:any_status ? t.λval.Some ? (set_irq_flag_sHCS08 t s val)
 760   | RS08 ⇒ λs:any_status ? t.λval.None ?
 761   | IP2022 ⇒ λs:any_status ? t.λval.None ?
 762   ].
 763
 764 (* setter debole di IRQ *)
 765 ndefinition setweak_irq_flag ≝
 766 λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
 767  match set_irq_flag … s val with
 768   [ None ⇒ s | Some s' ⇒ s' ].