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