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