matita/contribs/assembly/freescale/model.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:                                                         *)
  19 (*   Cosimo Oliboni, oliboni@cs.unibo.it                                  *)
  20 (*                                                                        *)
  21 (* Questo materiale fa parte della tesi:                                  *)
  22 (*   "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale"   *)
  23 (*                                                                        *)
  24 (*                    data ultima modifica 15/11/2007                     *)
  25 (* ********************************************************************** *)
  26
  27 include "freescale/status.ma".
  28
  29 (* *********************************** *)
  30 (* IMPOSTAZIONI SPECIFICHE DEI MODELLI *)
  31 (* *********************************** *)
  32
  33 (* modelli di HC05 *)
  34 inductive HC05_mcu_model : Type ≝
  35   MC68HC05J5A: HC05_mcu_model
  36   (*..*).
  37
  38 (* modelli di HC08 *)
  39 inductive HC08_mcu_model : Type ≝
  40   MC68HC08AB16A: HC08_mcu_model
  41   (*..*).
  42
  43 (* modelli di HCS08 *)
  44 inductive HCS08_mcu_model : Type ≝
  45   MC9S08AW60  : HCS08_mcu_model
  46 | MC9S08GB60  : HCS08_mcu_model
  47 | MC9S08GT60  : HCS08_mcu_model
  48 | MC9S08GB32  : HCS08_mcu_model
  49 | MC9S08GT32  : HCS08_mcu_model
  50 | MC9S08GT16  : HCS08_mcu_model
  51 | MC9S08GB60A : HCS08_mcu_model
  52 | MC9S08GT60A : HCS08_mcu_model
  53 | MC9S08GB32A : HCS08_mcu_model
  54 | MC9S08GT32A : HCS08_mcu_model
  55 | MC9S08GT16A : HCS08_mcu_model
  56 | MC9S08GT8A  : HCS08_mcu_model
  57 | MC9S08LC60  : HCS08_mcu_model
  58 | MC9S08LC36  : HCS08_mcu_model
  59 | MC9S08QD4   : HCS08_mcu_model
  60 | MC9S08QD2   : HCS08_mcu_model
  61 | MC9S08QG8   : HCS08_mcu_model
  62 | MC9S08QG4   : HCS08_mcu_model
  63 | MC9S08RC60  : HCS08_mcu_model
  64 | MC9S08RD60  : HCS08_mcu_model
  65 | MC9S08RE60  : HCS08_mcu_model
  66 | MC9S08RG60  : HCS08_mcu_model
  67 | MC9S08RC32  : HCS08_mcu_model
  68 | MC9S08RD32  : HCS08_mcu_model
  69 | MC9S08RE32  : HCS08_mcu_model
  70 | MC9S08RG32  : HCS08_mcu_model
  71 | MC9S08RC16  : HCS08_mcu_model
  72 | MC9S08RD16  : HCS08_mcu_model
  73 | MC9S08RE16  : HCS08_mcu_model
  74 | MC9S08RC8   : HCS08_mcu_model
  75 | MC9S08RD8   : HCS08_mcu_model
  76 | MC9S08RE8   : HCS08_mcu_model.
  77
  78 (* modelli di RS08 *)
  79 inductive RS08_mcu_model : Type ≝
  80   MC9RS08KA1 : RS08_mcu_model
  81 | MC9RS08KA2 : RS08_mcu_model.
  82
  83 (* raggruppamento dei modelli *)
  84 inductive any_mcu_model : Type ≝
  85   FamilyHC05  : HC05_mcu_model → any_mcu_model
  86 | FamilyHC08  : HC08_mcu_model → any_mcu_model
  87 | FamilyHCS08 : HCS08_mcu_model → any_mcu_model
  88 | FamilyRS08  : RS08_mcu_model → any_mcu_model.
  89
  90 coercion cic:/matita/freescale/model/any_mcu_model.ind#xpointer(1/1/1).
  91 coercion cic:/matita/freescale/model/any_mcu_model.ind#xpointer(1/1/2).
  92 coercion cic:/matita/freescale/model/any_mcu_model.ind#xpointer(1/1/3).
  93 coercion cic:/matita/freescale/model/any_mcu_model.ind#xpointer(1/1/4).
  94
  95 (*
  96 condizioni errore interne alla MCU
  97 (Il programma viene caricato dal produttore in ROM o impostato in EEPROM)
  98 HC05: +illegal address during opcode fetch
  99 HC08: +illegal address duting opcode fetch (ILAD mascherabile)
 100       +illegal opcode (ILOP mascherabile)
 101
 102 (Il programma viene programmato nella FLASH)
 103 HCS08: +illegal address during opcode fetch (ILAD mascherabile)
 104        +illegal opcode (ILOP mascherabile)
 105        +security = accesso a RAM e zone FLASH dichiarate sicure da zone sicure
 106                    da' 0 in lettura e ignore in scrittura, [FLASH]SEC00:SEC01 (1,0)
 107                    corrisponde a OFF, altre ON, disattivabile solo da modalita' sicura se
 108                    opzione [FLASH]KEYEN e' 1 passando chiave a 8byte da modalita' sicura.
 109                    Altrimenti disattivabile solo con FLASH mass erase. Obbiettivo
 110                    e' impedire duplicazione di software di controllo, dato che esiste
 111                    modalita' debugging. A restart viene ricaricata da FLASH impostazione
 112                    sicurezza!
 113 RS08: +illegal address durting opcode fetch (ILAD) mascherabile
 114       +illegal opcode (ILOP mascherabile)
 115       +security = solo la FLASH e' considerata sicura. Stesso meccanismo di HCS08
 116                   ma governato solo da [FLASH]SECD (0) OFF.Una volta attivato l'unica
 117                   disattivazione e' la cancellazione della FLASH.
 118 *)
 119
 120 (* memoria degli HC05 *)
 121 definition memory_type_of_FamilyHC05 ≝
 122 λm:HC05_mcu_model.match m with
 123   [ MC68HC05J5A ⇒
 124    [
 125   (* astraggo molto *)
 126   (* 0x0000-0x001F,0x0FF0: sarebbe memory mapped IO *)
 127
 128      tripleT ??? 〈〈x0,x0〉:〈x8,x0〉〉 〈〈x0,x0〉:〈xF,xF〉〉 MEM_READ_WRITE (* 128B RAM+STACK *)
 129    ; tripleT ??? 〈〈x0,x3〉:〈x0,x0〉〉 〈〈x0,xC〉:〈xF,xF〉〉 MEM_READ_ONLY  (* 2560B USER ROM *)
 130    ; tripleT ??? 〈〈x0,xE〉:〈x0,x0〉〉 〈〈x0,xF〉:〈xF,xF〉〉 MEM_READ_ONLY  (* 512B INTERNAL ROM *)
 131     ]
 132    (*..*)
 133   ].
 134
 135 (* memoria degli HC08 *)
 136 definition memory_type_of_FamilyHC08 ≝
 137 λm:HC08_mcu_model.match m with
 138   [ MC68HC08AB16A ⇒
 139    [
 140   (* astraggo molto *)
 141   (* 0x0000-0x004F,0xFE00-0xFE01,0xFE03,
 142      0xFE0C-0xFE11,0xFE1A-0xFE1D,0xFE1F: sarebbe memory mapped IO *)
 143   (* 0x0500-0x057F,0xFE02,0xFE04-0xFE07,
 144      0xFE09-0xFE0B,0xFE12-0xFE19,0xFE1E,0xFFC0-0xFFCF : sarebbe reserved *)
 145
 146      tripleT ??? 〈〈x0,x0〉:〈x5,x0〉〉 〈〈x0,x2〉:〈x4,xF〉〉 MEM_READ_WRITE (* 512B RAM *)
 147    ; tripleT ??? 〈〈x0,x8〉:〈x0,x0〉〉 〈〈x0,x9〉:〈xF,xF〉〉 MEM_READ_ONLY  (* 512B EEPROM *)
 148    ; tripleT ??? 〈〈xB,xE〉:〈x0,x0〉〉 〈〈xF,xD〉:〈xF,xF〉〉 MEM_READ_ONLY  (* 16384B ROM *)
 149    ; tripleT ??? 〈〈xF,xE〉:〈x2,x0〉〉 〈〈xF,xF〉:〈x5,x2〉〉 MEM_READ_ONLY  (* 307B ROM *)
 150    ; tripleT ??? 〈〈xF,xF〉:〈xD,x0〉〉 〈〈xF,xF〉:〈xF,xF〉〉 MEM_READ_ONLY  (* 48B ROM *) ]
 151    (*..*)
 152   ].
 153
 154 (* memoria degli HCS08 *)
 155 definition memory_type_of_FamilyHCS08 ≝
 156 λm:HCS08_mcu_model.match m with
 157   [ MC9S08AW60 ⇒
 158    [
 159   (* astraggo molto *)
 160   (* 0x0000-0x006F,0x1800-0x185F: sarebbe memory mapped IO *)
 161
 162      tripleT ??? 〈〈x0,x0〉:〈x7,x0〉〉 〈〈x0,x8〉:〈x6,xF〉〉 MEM_READ_WRITE (* 2048B RAM *)
 163    ; tripleT ??? 〈〈x0,x8〉:〈x7,x0〉〉 〈〈x1,x7〉:〈xF,xF〉〉 MEM_READ_ONLY  (* 3984B FLASH *)
 164    ; tripleT ??? 〈〈x1,x8〉:〈x6,x0〉〉 〈〈xF,xF〉:〈xF,xF〉〉 MEM_READ_ONLY  (* 59296B FLASH *) ]
 165   | MC9S08GB60 ⇒
 166    [
 167   (* astraggo molto *)
 168   (* 0x0000-0x007F,0x1800-0x182B: sarebbe memory mapped IO *)
 169
 170      tripleT ??? 〈〈x0,x0〉:〈x8,x0〉〉 〈〈x1,x0〉:〈x7,xF〉〉 MEM_READ_WRITE (* 4096B RAM *)
 171    ; tripleT ??? 〈〈x1,x0〉:〈x8,x0〉〉 〈〈x1,x7〉:〈xF,xF〉〉 MEM_READ_ONLY  (* 1920B FLASH *)
 172    ; tripleT ??? 〈〈x1,x8〉:〈x2,xC〉〉 〈〈xF,xF〉:〈xF,xF〉〉 MEM_READ_ONLY  (* 59348B FLASH *) ]
 173   | MC9S08GT60 ⇒
 174    [
 175   (* astraggo molto *)
 176   (* 0x0000-0x007F,0x1800-0x182B: sarebbe memory mapped IO *)
 177
 178      tripleT ??? 〈〈x0,x0〉:〈x8,x0〉〉 〈〈x1,x0〉:〈x7,xF〉〉 MEM_READ_WRITE (* 4096B RAM *)
 179    ; tripleT ??? 〈〈x1,x0〉:〈x8,x0〉〉 〈〈x1,x7〉:〈xF,xF〉〉 MEM_READ_ONLY  (* 1920B FLASH *)
 180    ; tripleT ??? 〈〈x1,x8〉:〈x2,xC〉〉 〈〈xF,xF〉:〈xF,xF〉〉 MEM_READ_ONLY  (* 59348B FLASH *) ]
 181   | MC9S08GB32 ⇒
 182    [
 183   (* astraggo molto *)
 184   (* 0x0000-0x007F,0x1800-0x182B: sarebbe memory mapped IO *)
 185
 186      tripleT ??? 〈〈x0,x0〉:〈x8,x0〉〉 〈〈x0,x8〉:〈x7,xF〉〉 MEM_READ_WRITE (* 2048B RAM *)
 187    ; tripleT ??? 〈〈x8,x0〉:〈x0,x0〉〉 〈〈xF,xF〉:〈xF,xF〉〉 MEM_READ_ONLY  (* 32768B FLASH *) ]
 188   | MC9S08GT32 ⇒
 189    [
 190   (* astraggo molto *)
 191   (* 0x0000-0x007F,0x1800-0x182B: sarebbe memory mapped IO *)
 192
 193      tripleT ??? 〈〈x0,x0〉:〈x8,x0〉〉 〈〈x0,x8〉:〈x7,xF〉〉 MEM_READ_WRITE (* 2048B RAM *)
 194    ; tripleT ??? 〈〈x8,x0〉:〈x0,x0〉〉 〈〈xF,xF〉:〈xF,xF〉〉 MEM_READ_ONLY  (* 32768B FLASH *) ]
 195   | MC9S08GT16 ⇒
 196    [
 197   (* astraggo molto *)
 198   (* 0x0000-0x007F,0x1800-0x182B: sarebbe memory mapped IO *)
 199
 200      tripleT ??? 〈〈x0,x0〉:〈x8,x0〉〉 〈〈x0,x4〉:〈x7,xF〉〉 MEM_READ_WRITE (* 1024B RAM *)
 201    ; tripleT ??? 〈〈xC,x0〉:〈x0,x0〉〉 〈〈xF,xF〉:〈xF,xF〉〉 MEM_READ_ONLY  (* 16384B FLASH *) ]
 202   | MC9S08GB60A ⇒
 203    [
 204   (* astraggo molto *)
 205   (* 0x0000-0x007F,0x1800-0x182B: sarebbe memory mapped IO *)
 206
 207      tripleT ??? 〈〈x0,x0〉:〈x8,x0〉〉 〈〈x1,x0〉:〈x7,xF〉〉 MEM_READ_WRITE (* 4096B RAM *)
 208    ; tripleT ??? 〈〈x1,x0〉:〈x8,x0〉〉 〈〈x1,x7〉:〈xF,xF〉〉 MEM_READ_ONLY  (* 1920B FLASH *)
 209    ; tripleT ??? 〈〈x1,x8〉:〈x2,xC〉〉 〈〈xF,xF〉:〈xF,xF〉〉 MEM_READ_ONLY  (* 59348B FLASH *) ]
 210   | MC9S08GT60A ⇒
 211    [
 212   (* astraggo molto *)
 213   (* 0x0000-0x007F,0x1800-0x182B: sarebbe memory mapped IO *)
 214
 215      tripleT ??? 〈〈x0,x0〉:〈x8,x0〉〉 〈〈x1,x0〉:〈x7,xF〉〉 MEM_READ_WRITE (* 4096B RAM *)
 216    ; tripleT ??? 〈〈x1,x0〉:〈x8,x0〉〉 〈〈x1,x7〉:〈xF,xF〉〉 MEM_READ_ONLY  (* 1920B FLASH *)
 217    ; tripleT ??? 〈〈x1,x8〉:〈x2,xC〉〉 〈〈xF,xF〉:〈xF,xF〉〉 MEM_READ_ONLY  (* 59348B FLASH *) ]
 218   | MC9S08GB32A ⇒
 219    [
 220   (* astraggo molto *)
 221   (* 0x0000-0x007F,0x1800-0x182B: sarebbe memory mapped IO *)
 222
 223      tripleT ??? 〈〈x0,x0〉:〈x8,x0〉〉 〈〈x0,x8〉:〈x7,xF〉〉 MEM_READ_WRITE (* 2048B RAM *)
 224    ; tripleT ??? 〈〈x8,x0〉:〈x0,x0〉〉 〈〈xF,xF〉:〈xF,xF〉〉 MEM_READ_ONLY  (* 32768B FLASH *) ]
 225   | MC9S08GT32A ⇒
 226    [
 227   (* astraggo molto *)
 228   (* 0x0000-0x007F,0x1800-0x182B: sarebbe memory mapped IO *)
 229
 230      tripleT ??? 〈〈x0,x0〉:〈x8,x0〉〉 〈〈x0,x8〉:〈x7,xF〉〉 MEM_READ_WRITE (* 2048B RAM *)
 231    ; tripleT ??? 〈〈x8,x0〉:〈x0,x0〉〉 〈〈xF,xF〉:〈xF,xF〉〉 MEM_READ_ONLY  (* 32768B FLASH *) ]
 232   | MC9S08GT16A ⇒
 233    [
 234   (* astraggo molto *)
 235   (* 0x0000-0x007F,0x1800-0x182B: sarebbe memory mapped IO *)
 236
 237      tripleT ??? 〈〈x0,x0〉:〈x8,x0〉〉 〈〈x0,x8〉:〈x7,xF〉〉 MEM_READ_WRITE (* 2048B RAM *)
 238    ; tripleT ??? 〈〈xC,x0〉:〈x0,x0〉〉 〈〈xF,xF〉:〈xF,xF〉〉 MEM_READ_ONLY  (* 16384B FLASH *) ]
 239   | MC9S08GT8A ⇒
 240    [
 241   (* astraggo molto *)
 242   (* 0x0000-0x007F,0x1800-0x182B: sarebbe memory mapped IO *)
 243
 244      tripleT ??? 〈〈x0,x0〉:〈x8,x0〉〉 〈〈x0,x8〉:〈x7,xF〉〉 MEM_READ_WRITE (* 2048B RAM *)
 245    ; tripleT ??? 〈〈xC,x0〉:〈x0,x0〉〉 〈〈xF,xF〉:〈xF,xF〉〉 MEM_READ_ONLY  (* 16384B FLASH *) ]
 246   | MC9S08LC60 ⇒
 247    [
 248   (* astraggo molto *)
 249   (* 0x0000-0x005F,0x1800-0x186F: sarebbe memory mapped IO *)
 250
 251      tripleT ??? 〈〈x0,x0〉:〈x6,x0〉〉 〈〈x1,x0〉:〈x5,xF〉〉 MEM_READ_WRITE (* 4096B RAM *)
 252    ; tripleT ??? 〈〈x1,x0〉:〈x6,x0〉〉 〈〈x1,x7〉:〈xF,xF〉〉 MEM_READ_ONLY  (* 1952B FLASH *)
 253    ; tripleT ??? 〈〈x1,x8〉:〈x7,x0〉〉 〈〈xF,xF〉:〈xF,xF〉〉 MEM_READ_ONLY  (* 59280B FLASH *) ]
 254   | MC9S08LC36 ⇒
 255    [
 256   (* astraggo molto *)
 257   (* 0x0000-0x005F,0x1800-0x186F: sarebbe memory mapped IO *)
 258
 259      tripleT ??? 〈〈x0,x0〉:〈x6,x0〉〉 〈〈x0,xA〉:〈x5,xF〉〉 MEM_READ_WRITE (* 2560B RAM *)
 260    ; tripleT ??? 〈〈x1,x8〉:〈x7,x0〉〉 〈〈x4,x8〉:〈x6,xF〉〉 MEM_READ_ONLY  (* 12288B FLASH *)
 261    ; tripleT ??? 〈〈xA,x0〉:〈x0,x0〉〉 〈〈xF,xF〉:〈xF,xF〉〉 MEM_READ_ONLY  (* 24576B FLASH *) ]
 262   | MC9S08QD4 ⇒
 263    [
 264   (* astraggo molto *)
 265   (* 0x0000-0x005F,0x1800-0x184F: sarebbe memory mapped IO *)
 266
 267      tripleT ??? 〈〈x0,x0〉:〈x6,x0〉〉 〈〈x0,x1〉:〈x5,xF〉〉 MEM_READ_WRITE (* 256B RAM *)
 268    ; tripleT ??? 〈〈xF,x0〉:〈x0,x0〉〉 〈〈xF,xF〉:〈xF,xF〉〉 MEM_READ_ONLY  (* 4096B FLASH *) ]
 269   | MC9S08QD2 ⇒
 270    [
 271   (* astraggo molto *)
 272   (* 0x0000-0x005F,0x1800-0x184F: sarebbe memory mapped IO *)
 273
 274      tripleT ??? 〈〈x0,x0〉:〈x6,x0〉〉 〈〈x0,x1〉:〈x5,xF〉〉 MEM_READ_WRITE (* 256B RAM *)
 275    ; tripleT ??? 〈〈xF,x0〉:〈x0,x0〉〉 〈〈xF,xF〉:〈xF,xF〉〉 MEM_READ_ONLY  (* 4096B FLASH *) ]
 276   | MC9S08QG8 ⇒
 277    [
 278   (* astraggo molto *)
 279   (* 0x0000-0x005F,0x1800-0x184F: sarebbe memory mapped IO *)
 280
 281      tripleT ??? 〈〈x0,x0〉:〈x6,x0〉〉 〈〈x0,x2〉:〈x5,xF〉〉 MEM_READ_WRITE (* 512B RAM *)
 282    ; tripleT ??? 〈〈xE,x0〉:〈x0,x0〉〉 〈〈xF,xF〉:〈xF,xF〉〉 MEM_READ_ONLY  (* 8192B FLASH *) ]
 283   | MC9S08QG4 ⇒
 284    [
 285   (* astraggo molto *)
 286   (* 0x0000-0x005F,0x1800-0x184F: sarebbe memory mapped IO *)
 287
 288      tripleT ??? 〈〈x0,x0〉:〈x6,x0〉〉 〈〈x0,x2〉:〈x5,xF〉〉 MEM_READ_WRITE (* 512B RAM *)
 289    ; tripleT ??? 〈〈xE,x0〉:〈x0,x0〉〉 〈〈xF,xF〉:〈xF,xF〉〉 MEM_READ_ONLY  (* 8192B FLASH *) ]
 290   | MC9S08RC60 ⇒
 291    [
 292   (* astraggo molto *)
 293   (* 0x0000-0x0045,0x1800-0x182B: sarebbe memory mapped IO *)
 294
 295      tripleT ??? 〈〈x0,x0〉:〈x4,x6〉〉 〈〈x0,x8〉:〈x4,x5〉〉 MEM_READ_WRITE (* 2048B RAM *)
 296    ; tripleT ??? 〈〈x0,x8〉:〈x4,x6〉〉 〈〈x1,x7〉:〈xF,xF〉〉 MEM_READ_ONLY  (* 4026B FLASH *)
 297    ; tripleT ??? 〈〈x1,x8〉:〈x2,xC〉〉 〈〈xF,xF〉:〈xF,xF〉〉 MEM_READ_ONLY  (* 59348B FLASH *) ]
 298   | MC9S08RD60 ⇒
 299    [
 300   (* astraggo molto *)
 301   (* 0x0000-0x0045,0x1800-0x182B: sarebbe memory mapped IO *)
 302
 303      tripleT ??? 〈〈x0,x0〉:〈x4,x6〉〉 〈〈x0,x8〉:〈x4,x5〉〉 MEM_READ_WRITE (* 2048B RAM *)
 304    ; tripleT ??? 〈〈x0,x8〉:〈x4,x6〉〉 〈〈x1,x7〉:〈xF,xF〉〉 MEM_READ_ONLY  (* 4026B FLASH *)
 305    ; tripleT ??? 〈〈x1,x8〉:〈x2,xC〉〉 〈〈xF,xF〉:〈xF,xF〉〉 MEM_READ_ONLY  (* 59348B FLASH *) ]
 306   | MC9S08RE60 ⇒
 307    [
 308   (* astraggo molto *)
 309   (* 0x0000-0x0045,0x1800-0x182B: sarebbe memory mapped IO *)
 310
 311      tripleT ??? 〈〈x0,x0〉:〈x4,x6〉〉 〈〈x0,x8〉:〈x4,x5〉〉 MEM_READ_WRITE (* 2048B RAM *)
 312    ; tripleT ??? 〈〈x0,x8〉:〈x4,x6〉〉 〈〈x1,x7〉:〈xF,xF〉〉 MEM_READ_ONLY  (* 4026B FLASH *)
 313    ; tripleT ??? 〈〈x1,x8〉:〈x2,xC〉〉 〈〈xF,xF〉:〈xF,xF〉〉 MEM_READ_ONLY  (* 59348B FLASH *) ]
 314   | MC9S08RG60 ⇒
 315    [
 316   (* astraggo molto *)
 317   (* 0x0000-0x0045,0x1800-0x182B: sarebbe memory mapped IO *)
 318
 319      tripleT ??? 〈〈x0,x0〉:〈x4,x6〉〉 〈〈x0,x8〉:〈x4,x5〉〉 MEM_READ_WRITE (* 2048B RAM *)
 320    ; tripleT ??? 〈〈x0,x8〉:〈x4,x6〉〉 〈〈x1,x7〉:〈xF,xF〉〉 MEM_READ_ONLY  (* 4026B FLASH *)
 321    ; tripleT ??? 〈〈x1,x8〉:〈x2,xC〉〉 〈〈xF,xF〉:〈xF,xF〉〉 MEM_READ_ONLY  (* 59348B FLASH *) ]
 322   | MC9S08RC32 ⇒
 323    [
 324   (* astraggo molto *)
 325   (* 0x0000-0x0045,0x1800-0x182B: sarebbe memory mapped IO *)
 326
 327      tripleT ??? 〈〈x0,x0〉:〈x4,x6〉〉 〈〈x0,x8〉:〈x4,x5〉〉 MEM_READ_WRITE (* 2048B RAM *)
 328    ; tripleT ??? 〈〈x8,x0〉:〈x0,x0〉〉 〈〈xF,xF〉:〈xF,xF〉〉 MEM_READ_ONLY  (* 32768B FLASH *) ]
 329   | MC9S08RD32 ⇒
 330    [
 331   (* astraggo molto *)
 332   (* 0x0000-0x0045,0x1800-0x182B: sarebbe memory mapped IO *)
 333
 334      tripleT ??? 〈〈x0,x0〉:〈x4,x6〉〉 〈〈x0,x8〉:〈x4,x5〉〉 MEM_READ_WRITE (* 2048B RAM *)
 335    ; tripleT ??? 〈〈x8,x0〉:〈x0,x0〉〉 〈〈xF,xF〉:〈xF,xF〉〉 MEM_READ_ONLY  (* 32768B FLASH *) ]
 336   | MC9S08RE32 ⇒
 337    [
 338   (* astraggo molto *)
 339   (* 0x0000-0x0045,0x1800-0x182B: sarebbe memory mapped IO *)
 340
 341      tripleT ??? 〈〈x0,x0〉:〈x4,x6〉〉 〈〈x0,x8〉:〈x4,x5〉〉 MEM_READ_WRITE (* 2048B RAM *)
 342    ; tripleT ??? 〈〈x8,x0〉:〈x0,x0〉〉 〈〈xF,xF〉:〈xF,xF〉〉 MEM_READ_ONLY  (* 32768B FLASH *) ]
 343   | MC9S08RG32 ⇒
 344    [
 345   (* astraggo molto *)
 346   (* 0x0000-0x0045,0x1800-0x182B: sarebbe memory mapped IO *)
 347
 348      tripleT ??? 〈〈x0,x0〉:〈x4,x6〉〉 〈〈x0,x8〉:〈x4,x5〉〉 MEM_READ_WRITE (* 2048B RAM *)
 349    ; tripleT ??? 〈〈x8,x0〉:〈x0,x0〉〉 〈〈xF,xF〉:〈xF,xF〉〉 MEM_READ_ONLY  (* 32768B FLASH *) ]
 350   | MC9S08RC16 ⇒
 351    [
 352   (* astraggo molto *)
 353   (* 0x0000-0x003F,0x1800-0x182B: sarebbe memory mapped IO *)
 354
 355      tripleT ??? 〈〈x0,x0〉:〈x4,x0〉〉 〈〈x0,x4〉:〈x3,xF〉〉 MEM_READ_WRITE (* 1024B RAM *)
 356    ; tripleT ??? 〈〈xC,x0〉:〈x0,x0〉〉 〈〈xF,xF〉:〈xF,xF〉〉 MEM_READ_ONLY  (* 16384B FLASH *) ]
 357   | MC9S08RD16 ⇒
 358    [
 359   (* astraggo molto *)
 360   (* 0x0000-0x003F,0x1800-0x182B: sarebbe memory mapped IO *)
 361
 362      tripleT ??? 〈〈x0,x0〉:〈x4,x0〉〉 〈〈x0,x4〉:〈x3,xF〉〉 MEM_READ_WRITE (* 1024B RAM *)
 363    ; tripleT ??? 〈〈xC,x0〉:〈x0,x0〉〉 〈〈xF,xF〉:〈xF,xF〉〉 MEM_READ_ONLY  (* 16384B FLASH *) ]
 364   | MC9S08RE16 ⇒
 365    [
 366   (* astraggo molto *)
 367   (* 0x0000-0x003F,0x1800-0x182B: sarebbe memory mapped IO *)
 368
 369      tripleT ??? 〈〈x0,x0〉:〈x4,x0〉〉 〈〈x0,x4〉:〈x3,xF〉〉 MEM_READ_WRITE (* 1024B RAM *)
 370    ; tripleT ??? 〈〈xC,x0〉:〈x0,x0〉〉 〈〈xF,xF〉:〈xF,xF〉〉 MEM_READ_ONLY  (* 16384B FLASH *) ]
 371   | MC9S08RC8 ⇒
 372    [
 373   (* astraggo molto *)
 374   (* 0x0000-0x003F,0x1800-0x182B: sarebbe memory mapped IO *)
 375
 376      tripleT ??? 〈〈x0,x0〉:〈x4,x0〉〉 〈〈x0,x4〉:〈x3,xF〉〉 MEM_READ_WRITE (* 1024B RAM *)
 377    ; tripleT ??? 〈〈xE,x0〉:〈x0,x0〉〉 〈〈xF,xF〉:〈xF,xF〉〉 MEM_READ_ONLY  (* 8192B FLASH *) ]
 378   | MC9S08RD8 ⇒
 379    [
 380   (* astraggo molto *)
 381   (* 0x0000-0x003F,0x1800-0x182B: sarebbe memory mapped IO *)
 382
 383      tripleT ??? 〈〈x0,x0〉:〈x4,x0〉〉 〈〈x0,x4〉:〈x3,xF〉〉 MEM_READ_WRITE (* 1024B RAM *)
 384    ; tripleT ??? 〈〈xE,x0〉:〈x0,x0〉〉 〈〈xF,xF〉:〈xF,xF〉〉 MEM_READ_ONLY  (* 8192B FLASH *) ]
 385   | MC9S08RE8 ⇒
 386    [
 387   (* astraggo molto *)
 388   (* 0x0000-0x003F,0x1800-0x182B: sarebbe memory mapped IO *)
 389
 390      tripleT ??? 〈〈x0,x0〉:〈x4,x0〉〉 〈〈x0,x4〉:〈x3,xF〉〉 MEM_READ_WRITE (* 1024B RAM *)
 391    ; tripleT ??? 〈〈xE,x0〉:〈x0,x0〉〉 〈〈xF,xF〉:〈xF,xF〉〉 MEM_READ_ONLY  (* 8192B FLASH *) ]
 392   ].
 393
 394 (* memoria dei RS08 *)
 395 definition memory_type_of_FamilyRS08 ≝
 396 λm:RS08_mcu_model.match m with
 397   [ MC9RS08KA1 ⇒
 398    [
 399      tripleT ??? 〈〈x0,x0〉:〈x0,x0〉〉 〈〈x0,x0〉:〈x0,xE〉〉 MEM_READ_WRITE (* 15B RAM *)
 400   (* [000F] e' il registro X *)
 401   (* 0x0010-0x001E sarebbe memory mapped IO, proviamo per completezza con RAM *)
 402    ; tripleT ??? 〈〈x0,x0〉:〈x1,x0〉〉 〈〈x0,x0〉:〈x1,xE〉〉 MEM_READ_WRITE (* 15B MEMORY MAPPED IO *)
 403   (* [001F] e' il registro PAGESEL *)
 404    ; tripleT ??? 〈〈x0,x0〉:〈x2,x0〉〉 〈〈x0,x0〉:〈x4,xF〉〉 MEM_READ_WRITE (* 48B RAM *)
 405   (* [00C0-00FF] mappato da PAGESEL su [00pp pppp ppxx xxxx] *)
 406    ; tripleT ??? 〈〈x0,x0〉:〈xC,x0〉〉 〈〈x0,x0〉:〈xF,xF〉〉 MEM_READ_WRITE (* 64B RAM PAGING *)
 407   (* 0x0200-0x023F sarebbe memory mapped IO, proviamo per completezza con RAM *)
 408    ; tripleT ??? 〈〈x0,x2〉:〈x0,x0〉〉 〈〈x0,x2〉:〈x3,xF〉〉 MEM_READ_WRITE (* 64B MEMORY MAPPED IO *)
 409    ; tripleT ??? 〈〈x3,xC〉:〈x0,x0〉〉 〈〈x3,xF〉:〈xF,xF〉〉 MEM_READ_ONLY  (* 1024B FLASH *) ]
 410   | MC9RS08KA2 ⇒
 411    [
 412      tripleT ??? 〈〈x0,x0〉:〈x0,x0〉〉 〈〈x0,x0〉:〈x0,xE〉〉 MEM_READ_WRITE (* 15B RAM *)
 413   (* [000F] e' il registro X *)
 414   (* 0x0010-0x001E sarebbe memory mapped IO, proviamo per completezza con RAM *)
 415    ; tripleT ??? 〈〈x0,x0〉:〈x1,x0〉〉 〈〈x0,x0〉:〈x1,xE〉〉 MEM_READ_WRITE (* 15B MEMORY MAPPED IO *)
 416   (* [001F] e' il registro PAGESEL *)
 417    ; tripleT ??? 〈〈x0,x0〉:〈x2,x0〉〉 〈〈x0,x0〉:〈x4,xF〉〉 MEM_READ_WRITE (* 48B RAM *)
 418   (* [00C0-00FF] mappato da PAGESEL su [00pp pppp ppxx xxxx] *)
 419    ; tripleT ??? 〈〈x0,x0〉:〈xC,x0〉〉 〈〈x0,x0〉:〈xF,xF〉〉 MEM_READ_WRITE (* 64B RAM PAGING *)
 420   (* 0x0200-0x023F sarebbe memory mapped IO, proviamo per completezza con RAM *)
 421    ; tripleT ??? 〈〈x0,x2〉:〈x0,x0〉〉 〈〈x0,x2〉:〈x3,xF〉〉 MEM_READ_WRITE (* 64B MEMORY MAPPED IO *)
 422    ; tripleT ??? 〈〈x3,x8〉:〈x0,x0〉〉 〈〈x3,xF〉:〈xF,xF〉〉 MEM_READ_ONLY  (* 2048B FLASH *) ]
 423   ].
 424
 425 (* ∀modello.descrizione della memoria installata *)
 426 definition memory_type_of_mcu_version ≝
 427 λmcu:any_mcu_model.match mcu with
 428  [ FamilyHC05  m ⇒ memory_type_of_FamilyHC05 m
 429  | FamilyHC08  m ⇒ memory_type_of_FamilyHC08 m
 430  | FamilyHCS08 m ⇒ memory_type_of_FamilyHCS08 m
 431  | FamilyRS08  m ⇒ memory_type_of_FamilyRS08 m
 432  ].
 433
 434 (* dato un modello costruisce un descrittore a partire dalla lista precedente *)
 435 definition build_memory_type_of_mcu_version ≝
 436 λmcu:any_mcu_model.λt:memory_impl.
 437  let rec aux param result ≝
 438   match param with
 439    [ nil ⇒ result
 440    | cons hd tl ⇒
 441     aux tl (check_update_ranged t result (fst3T ??? hd) (snd3T ??? hd) (thd3T ??? hd)) ]
 442  in aux (memory_type_of_mcu_version mcu) (out_of_bound_memory t).
 443
 444 (* sarebbe programma da caricare/zero_memory, ora test *)
 445 definition memory_of_mcu_version ≝
 446 λmcu:any_mcu_model.λt:memory_impl.match mcu with
 447  [ FamilyHC05 m ⇒ match m with
 448   [ MC68HC05J5A ⇒ zero_memory t
 449     (*..*)
 450   ]
 451  | FamilyHC08 m ⇒ match m with
 452   [ MC68HC08AB16A ⇒ zero_memory t
 453     (*..*)
 454   ]
 455  (* tralascio l'enumerazione dei casi, per ora e' tutto 0 *)
 456  | FamilyHCS08 _ ⇒ zero_memory t
 457  | FamilyRS08 _ ⇒ zero_memory t
 458  ].
 459
 460 (* inferire la mcu a partire dal modello *)
 461 definition mcu_of_model ≝
 462 λm:any_mcu_model.match m with
 463  [ FamilyHC05  _ ⇒ HC05
 464  | FamilyHC08  _ ⇒ HC08
 465  | FamilyHCS08 _ ⇒ HCS08
 466  | FamilyRS08  _ ⇒ RS08
 467  ].
 468
 469 (*
 470    parametrizzati i non deterministici rispetto a tutti i valori casuali
 471    che verranno dati dall'esterno di tipo byte8 (ndby1-2) e bool (ndbo1-5).
 472    l'ACCENSIONE e' totalmente equivalente ad un reset causato da calo di tensione
 473    (reset V-low), la memoria ed il check puo' essere passata, per esempio da
 474    - (memory_of_mcu_version MC68HC05J5A)
 475    - (build_memory_type_of_mcu_version MC68HC05J5A)
 476 *)
 477 definition start_of_mcu_version ≝
 478 λmcu:any_mcu_model.λt:memory_impl.
 479 let pc_reset_h ≝ 〈〈xF,xF〉:〈xF,xE〉〉 in
 480 let pc_reset_l ≝ 〈〈xF,xF〉:〈xF,xF〉〉 in
 481 let pc_RS08_reset ≝ 〈〈xF,xF〉:〈xF,xD〉〉 in
 482 let sp_reset ≝ 〈〈x0,x0〉:〈xF,xF〉〉 in
 483 match mcu
 484  return λmcu:any_mcu_model.(aux_mem_type t) → (aux_chk_type t) → byte8 → byte8 →
 485         bool → bool → bool → bool → bool → bool → any_status (mcu_of_model mcu) t
 486 with
 487 (* HC05: parzialmente non deterministico *)
 488  [ FamilyHC05 m ⇒ λmem:aux_mem_type t.λchk:aux_chk_type t.
 489                   λndby1,ndby2:byte8.λirqfl,ndbo1,ndbo2,ndbo3,ndbo4,ndbo5:bool.
 490   let build ≝ λspm,spf,pcm.
 491   let fetched_pc ≝ mk_word16 (mem_read_abs t mem (and_w16 pc_reset_h pcm))
 492                              (mem_read_abs t mem (and_w16 pc_reset_l pcm)) in
 493    mk_any_status HC05 t
 494     (mk_alu_HC05
 495      (* acc_low: ? *) ndby1 (* indx_low: ? *) ndby2
 496      (* sp: reset *) (or_w16 (and_w16 sp_reset spm) spf) spm spf
 497      (* pc: reset+fetch *) (and_w16 fetched_pc pcm) pcm
 498      (* H: ? *) ndbo1 (* I: reset *) true (* N: ? *) ndbo2
 499      (* Z: ? *) ndbo3 (* C: ? *) ndbo4 (* IRQ: ? *) irqfl)
 500      (* mem *) mem
 501      (* chk *) chk
 502      (* clk: reset *) (None ?) in
 503   match m with
 504    [ MC68HC05J5A ⇒ build 〈〈x0,x0〉:〈x3,xF〉〉 〈〈x0,x0〉:〈xC,x0〉〉 〈〈x0,xF〉:〈xF,xF〉〉
 505      (*..*)
 506    ]
 507
 508 (* HC08: parzialmente non deterministico *)
 509  | FamilyHC08 m ⇒ λmem:aux_mem_type t.λchk:aux_chk_type t.
 510                   λndby1,ndby2:byte8.λirqfl,ndbo1,ndbo2,ndbo3,ndbo4,ndbo5:bool.
 511   let build ≝
 512   let fetched_pc ≝ mk_word16 (mem_read_abs t mem pc_reset_h)
 513                              (mem_read_abs t mem pc_reset_l) in
 514    mk_any_status HC08 t
 515     (mk_alu_HC08
 516      (* acc_low: ? *) ndby1 (* indw_low: ? *) ndby2 (* indx_high: reset *)  〈x0,x0〉
 517      (* sp: reset *) sp_reset (* pc: reset+fetch *) fetched_pc
 518      (* V: ? *) ndbo1 (* H: ? *) ndbo2 (* I: reset *) true
 519      (* N: ? *) ndbo3 (* Z: ? *) ndbo4 (* C: ? *) ndbo5 (* IRQ: ? *) irqfl)
 520      (* mem *) mem
 521      (* chk *) chk
 522      (* clk: reset *) (None ?) in
 523   (* tralascio l'enumerazione dei casi, tanto non ci sono maschere da impostare *)
 524   build
 525
 526 (* HCS08: parzialmente non deterministico *)
 527  | FamilyHCS08 m ⇒ λmem:aux_mem_type t.λchk:aux_chk_type t.
 528                    λndby1,ndby2:byte8.λirqfl,ndbo1,ndbo2,ndbo3,ndbo4,ndbo5:bool.
 529   let build ≝
 530   let fetched_pc ≝ mk_word16 (mem_read_abs t mem pc_reset_h)
 531                              (mem_read_abs t mem pc_reset_l) in
 532    mk_any_status HCS08 t
 533     (mk_alu_HC08
 534      (* acc_low: ? *) ndby1 (* indw_low: ? *) ndby2 (* indx_high: reset *)  〈x0,x0〉
 535      (* sp: reset *) sp_reset (* pc: reset+fetch *) fetched_pc
 536      (* V: ? *) ndbo1 (* H: ? *) ndbo2 (* I: reset *) true
 537      (* N: ? *) ndbo3 (* Z: ? *) ndbo4 (* C: ? *) ndbo5 (* IRQ: ? *) irqfl)
 538      (* mem *) mem
 539      (* chk *) chk
 540      (* clk: reset *) (None ?) in
 541   (* tralascio l'enumerazione dei casi, tanto non ci sono maschere da impostare *)
 542   build
 543
 544 (* RS08: deterministico *)
 545  | FamilyRS08 m ⇒ λmem:aux_mem_type t.λchk:aux_chk_type t.
 546                   λndby1,ndby2:byte8.λirqfl,ndbo1,ndbo2,ndbo3,ndbo4,ndbo5:bool.
 547   let build ≝ λpcm.
 548    mk_any_status RS08 t
 549     (mk_alu_RS08
 550      (* acc_low: reset *)  〈x0,x0〉
 551      (* pc: reset *) (and_w16 pc_RS08_reset pcm) pcm
 552      (* spc: reset *) (and_w16 pc_RS08_reset pcm)
 553      (* xm: reset *) 〈x0,x0〉 (* psm: *) 〈x8,x0〉
 554      (* Z: reset *) false (* C: reset *) false)
 555      (* mem *) mem
 556      (* chk *) chk
 557      (* clk: reset *) (None ?) in
 558   (* tralascio l'enumerazione dei casi, tanto i valori sono uguali *)
 559   build 〈〈x3,xF〉:〈xF,xF〉〉
 560  ].
 561
 562 (*
 563    cio' che non viene resettato mantiene il valore precedente: nella documentazione
 564    viene riportato come "unaffected"/"indeterminate"/"unpredictable"
 565    il soft RESET e' diverso da un calo di tensione e la ram non variera'
 566 *)
 567 definition reset_of_mcu ≝
 568 λm:mcu_type.λt:memory_impl.
 569 let pc_reset_h ≝ 〈〈xF,xF〉:〈xF,xE〉〉 in
 570 let pc_reset_l ≝ 〈〈xF,xF〉:〈xF,xF〉〉 in
 571 let pc_RS08_reset ≝ 〈〈xF,xF〉:〈xF,xD〉〉 in
 572 let sp_reset ≝ 〈〈x0,x0〉:〈xF,xF〉〉 in
 573  match m return λm:mcu_type.(any_status m t) → (any_status m t) with
 574 (* HC05: parzialmente non deterministico *)
 575   [ HC05 ⇒ λs:any_status HC05 t.match s with
 576    [ mk_any_status alu mem chk clk ⇒ match alu with
 577     [ mk_alu_HC05 acclow indxlow _ spm spf _ pcm hfl _ nfl zfl cfl irqfl ⇒
 578     let fetched_pc ≝ mk_word16 (mem_read_abs t mem (and_w16 pc_reset_h pcm))
 579                                (mem_read_abs t mem (and_w16 pc_reset_l pcm)) in
 580     mk_any_status HC05 t
 581      (mk_alu_HC05
 582       (* acc_low: inv. *) acclow (* indx_low: inv. *) indxlow
 583       (* sp: reset *) (or_w16 (and_w16 sp_reset spm) spf) spm spf
 584       (* pc: reset+fetch *) (and_w16 fetched_pc pcm) pcm
 585       (* H: inv. *) hfl (* I: reset *) true (* N: inv. *) nfl
 586       (* Z: inv. *) zfl (* C: inv. *) cfl (* IRQ: inv *) irqfl)
 587       (* mem: inv. *) mem
 588       (* chk: inv. *) chk
 589       (* clk: reset *) (None ?) ]]
 590 (* HC08: parzialmente non deterministico *)
 591   | HC08 ⇒ λs:any_status HC08 t.match s with
 592    [ mk_any_status alu mem chk clk ⇒ match alu with
 593     [ mk_alu_HC08 acclow indxlow _ _ _ vfl hfl _ nfl zfl cfl irqfl ⇒
 594     let fetched_pc ≝ mk_word16 (mem_read_abs t mem pc_reset_h)
 595                                (mem_read_abs t mem pc_reset_l) in
 596     mk_any_status HC08 t
 597      (mk_alu_HC08
 598       (* acc_low: inv. *) acclow (* indx_low: inv. *) indxlow (* indx_high: reset *) 〈x0,x0〉
 599       (* sp: reset *) sp_reset (* pc: reset+fetch *) fetched_pc
 600       (* V: inv. *) vfl (* H: inv. *) hfl (* I: reset *) true
 601       (* N: inv. *) nfl (* Z: inv. *) zfl (* C: inv. *) cfl (* IRQ: inv *) irqfl)
 602       (* mem: inv. *) mem
 603       (* chk: inv. *) chk
 604       (* clk: reset *) (None ?) ]]
 605 (* HCS08: parzialmente non deterministico *)
 606   | HCS08 ⇒ λs:any_status HCS08 t.match s with
 607    [ mk_any_status alu mem chk clk ⇒ match alu with
 608     [ mk_alu_HC08 acclow indxlow _ _ _ vfl hfl _ nfl zfl cfl irqfl ⇒
 609     let fetched_pc ≝ mk_word16 (mem_read_abs t mem pc_reset_h)
 610                                (mem_read_abs t mem pc_reset_l) in
 611     mk_any_status HCS08 t
 612      (mk_alu_HC08
 613       (* acc_low: inv. *) acclow (* indx_low: inv. *) indxlow (* indx_high: reset *) 〈x0,x0〉
 614       (* sp: reset *) sp_reset (* pc: reset+fetch *) fetched_pc
 615       (* V: inv. *) vfl (* H: inv. *) hfl (* I: reset *) true
 616       (* N: inv. *) nfl (* Z: inv. *) zfl (* C: inv. *) cfl (* IRQ: inv *) irqfl)
 617       (* mem: inv. *) mem
 618       (* chk: inv. *) chk
 619       (* clk: reset *) (None ?) ]]
 620 (* RS08: deterministico *)
 621   | RS08 ⇒ λs:any_status RS08 t.match s with
 622    [ mk_any_status alu mem chk clk ⇒ match alu with
 623     [ mk_alu_RS08 _ _ pcm _ _ _ _ _ ⇒
 624     mk_any_status RS08 t
 625      (mk_alu_RS08
 626       (* acc_low: reset *) 〈x0,x0〉
 627       (* pc: reset *) (and_w16 pc_RS08_reset pcm) pcm
 628       (* spc: reset *) (and_w16 pc_RS08_reset pcm)
 629       (* xm: reset *) 〈x0,x0〉 (* psm: reset *) 〈x8,x0〉
 630       (* Z: reset *) false (* C: reset *) false)
 631       (* mem: inv. *) mem
 632       (* chk: inv. *) chk
 633       (* clk: reset *) (None ?) ]]
 634   ].