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