helm/software/matita/contribs/ng_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: Cosimo Oliboni, oliboni@cs.unibo.it                   *)
  19 (*     Cosimo Oliboni, oliboni@cs.unibo.it                                *)
  20 (*                                                                        *)
  21 (* ********************************************************************** *)
  22
  23 include "freescale/status.ma".
  24
  25 (* *********************************** *)
  26 (* IMPOSTAZIONI SPECIFICHE DEI MODELLI *)
  27 (* *********************************** *)
  28
  29 (* modelli di HC05 *)
  30 ninductive HC05_mcu_model : Type ≝
  31   MC68HC05J5A: HC05_mcu_model
  32   (*..*).
  33
  34 ndefinition HC05_mcu_model_ind : ΠP:HC05_mcu_model → Prop.P MC68HC05J5A → Πh:HC05_mcu_model.P h ≝
  35 λP:HC05_mcu_model → Prop.λp:P MC68HC05J5A.λh:HC05_mcu_model.
  36  match h with [ MC68HC05J5A ⇒ p ].
  37
  38 ndefinition HC05_mcu_model_rec : ΠP:HC05_mcu_model → Set.P MC68HC05J5A → Πh:HC05_mcu_model.P h ≝
  39 λP:HC05_mcu_model → Set.λp:P MC68HC05J5A.λh:HC05_mcu_model.
  40  match h with [ MC68HC05J5A ⇒ p ].
  41
  42 ndefinition HC05_mcu_model_rect : ΠP:HC05_mcu_model → Type.P MC68HC05J5A → Πh:HC05_mcu_model.P h ≝
  43 λP:HC05_mcu_model → Type.λp:P MC68HC05J5A.λh:HC05_mcu_model.
  44  match h with [ MC68HC05J5A ⇒ p ].
  45
  46 (* modelli di HC08 *)
  47 ninductive HC08_mcu_model : Type ≝
  48   MC68HC08AB16A: HC08_mcu_model
  49   (*..*).
  50
  51 ndefinition HC08_mcu_model_ind : ΠP:HC08_mcu_model → Prop.P MC68HC08AB16A → Πh:HC08_mcu_model.P h ≝
  52 λP:HC08_mcu_model → Prop.λp:P MC68HC08AB16A.λh:HC08_mcu_model.
  53  match h with [ MC68HC08AB16A ⇒ p ].
  54
  55 ndefinition HC08_mcu_model_rec : ΠP:HC08_mcu_model → Set.P MC68HC08AB16A → Πh:HC08_mcu_model.P h ≝
  56 λP:HC08_mcu_model → Set.λp:P MC68HC08AB16A.λh:HC08_mcu_model.
  57  match h with [ MC68HC08AB16A ⇒ p ].
  58
  59 ndefinition HC08_mcu_model_rect : ΠP:HC08_mcu_model → Type.P MC68HC08AB16A → Πh:HC08_mcu_model.P h ≝
  60 λP:HC08_mcu_model → Type.λp:P MC68HC08AB16A.λh:HC08_mcu_model.
  61  match h with [ MC68HC08AB16A ⇒ p ].
  62
  63 (* modelli di HCS08 *)
  64 ninductive HCS08_mcu_model : Type ≝
  65   MC9S08AW60 : HCS08_mcu_model
  66 | MC9S08GB60 : HCS08_mcu_model
  67   (*..*).
  68
  69 ndefinition HCS08_mcu_model_ind : ΠP:HCS08_mcu_model → Prop.P MC9S08GB60 → P MC9S08AW60 → Πh:HCS08_mcu_model.P h ≝
  70 λP:HCS08_mcu_model → Prop.λp:P MC9S08GB60.λp1:P MC9S08AW60.λh:HCS08_mcu_model.
  71  match h with [ MC9S08GB60 ⇒ p | MC9S08AW60 ⇒ p1 ].
  72
  73 ndefinition HCS08_mcu_model_rec : ΠP:HCS08_mcu_model → Set.P MC9S08GB60 → P MC9S08AW60 → Πh:HCS08_mcu_model.P h ≝
  74 λP:HCS08_mcu_model → Set.λp:P MC9S08GB60.λp1:P MC9S08AW60.λh:HCS08_mcu_model.
  75  match h with [ MC9S08GB60 ⇒ p | MC9S08AW60 ⇒ p1 ].
  76
  77 ndefinition HCS08_mcu_model_rect : ΠP:HCS08_mcu_model → Type.P MC9S08GB60 → P MC9S08AW60 → Πh:HCS08_mcu_model.P h ≝
  78 λP:HCS08_mcu_model → Type.λp:P MC9S08GB60.λp1:P MC9S08AW60.λh:HCS08_mcu_model.
  79  match h with [ MC9S08GB60 ⇒ p | MC9S08AW60 ⇒ p1 ].
  80
  81 (* modelli di RS08 *)
  82 ninductive RS08_mcu_model : Type ≝
  83   MC9RS08KA1 : RS08_mcu_model
  84 | MC9RS08KA2 : RS08_mcu_model.
  85
  86 ndefinition RS08_mcu_model_ind : ΠP:RS08_mcu_model → Prop.P MC9RS08KA1 → P MC9RS08KA2 → Πr:RS08_mcu_model.P r ≝
  87 λP:RS08_mcu_model → Prop.λp:P MC9RS08KA1.λp1:P MC9RS08KA2.λr:RS08_mcu_model.
  88   match r with [ MC9RS08KA1 ⇒ p | MC9RS08KA2 ⇒ p1 ].
  89
  90 ndefinition RS08_mcu_model_rec : ΠP:RS08_mcu_model → Set.P MC9RS08KA1 → P MC9RS08KA2 → Πr:RS08_mcu_model.P r ≝
  91 λP:RS08_mcu_model → Set.λp:P MC9RS08KA1.λp1:P MC9RS08KA2.λr:RS08_mcu_model.
  92   match r with [ MC9RS08KA1 ⇒ p | MC9RS08KA2 ⇒ p1 ].
  93
  94 ndefinition RS08_mcu_model_rect : ΠP:RS08_mcu_model → Type.P MC9RS08KA1 → P MC9RS08KA2 → Πr:RS08_mcu_model.P r ≝
  95 λP:RS08_mcu_model → Type.λp:P MC9RS08KA1.λp1:P MC9RS08KA2.λr:RS08_mcu_model.
  96   match r with [ MC9RS08KA1 ⇒ p | MC9RS08KA2 ⇒ p1 ].
  97
  98 (* raggruppamento dei modelli *)
  99 ninductive any_mcu_model : Type ≝
 100   FamilyHC05  : HC05_mcu_model → any_mcu_model
 101 | FamilyHC08  : HC08_mcu_model → any_mcu_model
 102 | FamilyHCS08 : HCS08_mcu_model → any_mcu_model
 103 | FamilyRS08  : RS08_mcu_model → any_mcu_model.
 104
 105 ndefinition any_mcu_model_ind
 106  : ΠP:any_mcu_model → Prop.(Πn:HC05_mcu_model.P (FamilyHC05 n)) → (Πn:HC08_mcu_model.P (FamilyHC08 n)) →
 107    (Πn:HCS08_mcu_model.P (FamilyHCS08 n)) → (Πn:RS08_mcu_model.P (FamilyRS08 n))→Πa:any_mcu_model.P a ≝
 108 λP:any_mcu_model → Prop.λf:Πn:HC05_mcu_model.P (FamilyHC05 n).λf1:Πn:HC08_mcu_model.P (FamilyHC08 n).
 109 λf2:Πn:HCS08_mcu_model.P (FamilyHCS08 n).λf3:Πn:RS08_mcu_model.P (FamilyRS08 n).λa:any_mcu_model.
 110  match a with [ FamilyHC05 n ⇒ f n | FamilyHC08 n ⇒ f1 n
 111               | FamilyHCS08 n ⇒ f2 n | FamilyRS08 n ⇒ f3 n ].
 112
 113 ndefinition any_mcu_model_rec
 114  : ΠP:any_mcu_model → Set.(Πn:HC05_mcu_model.P (FamilyHC05 n)) → (Πn:HC08_mcu_model.P (FamilyHC08 n)) →
 115    (Πn:HCS08_mcu_model.P (FamilyHCS08 n)) → (Πn:RS08_mcu_model.P (FamilyRS08 n))→Πa:any_mcu_model.P a ≝
 116 λP:any_mcu_model → Set.λf:Πn:HC05_mcu_model.P (FamilyHC05 n).λf1:Πn:HC08_mcu_model.P (FamilyHC08 n).
 117 λf2:Πn:HCS08_mcu_model.P (FamilyHCS08 n).λf3:Πn:RS08_mcu_model.P (FamilyRS08 n).λa:any_mcu_model.
 118  match a with [ FamilyHC05 n ⇒ f n | FamilyHC08 n ⇒ f1 n
 119               | FamilyHCS08 n ⇒ f2 n | FamilyRS08 n ⇒ f3 n ].
 120
 121 ndefinition any_mcu_model_rect
 122  : ΠP:any_mcu_model → Type.(Πn:HC05_mcu_model.P (FamilyHC05 n)) → (Πn:HC08_mcu_model.P (FamilyHC08 n)) →
 123    (Πn:HCS08_mcu_model.P (FamilyHCS08 n)) → (Πn:RS08_mcu_model.P (FamilyRS08 n))→Πa:any_mcu_model.P a ≝
 124 λP:any_mcu_model → Type.λf:Πn:HC05_mcu_model.P (FamilyHC05 n).λf1:Πn:HC08_mcu_model.P (FamilyHC08 n).
 125 λf2:Πn:HCS08_mcu_model.P (FamilyHCS08 n).λf3:Πn:RS08_mcu_model.P (FamilyRS08 n).λa:any_mcu_model.
 126  match a with [ FamilyHC05 n ⇒ f n | FamilyHC08 n ⇒ f1 n
 127               | FamilyHCS08 n ⇒ f2 n | FamilyRS08 n ⇒ f3 n ].
 128
 129 (*
 130 condizioni errore interne alla MCU
 131 (Il programma viene caricato dal produttore in ROM o impostato in EEPROM)
 132 HC05: +illegal address during opcode fetch
 133 HC08: +illegal address duting opcode fetch (ILAD mascherabile)
 134       +illegal opcode (ILOP mascherabile)
 135
 136 (Il programma viene programmato nella FLASH)
 137 HCS08: +illegal address during opcode fetch (ILAD mascherabile)
 138        +illegal opcode (ILOP mascherabile)
 139        +security = accesso a RAM e zone FLASH dichiarate sicure da zone sicure
 140                    da' 0 in lettura e ignore in scrittura, [FLASH]SEC00:SEC01 (1,0)
 141                    corrisponde a OFF, altre ON, disattivabile solo da modalita' sicura se
 142                    opzione [FLASH]KEYEN e' 1 passando chiave a 8byte da modalita' sicura.
 143                    Altrimenti disattivabile solo con FLASH mass erase. Obbiettivo
 144                    e' impedire duplicazione di software di controllo, dato che esiste
 145                    modalita' debugging. A restart viene ricaricata da FLASH impostazione
 146                    sicurezza!
 147 RS08: +illegal address durting opcode fetch (ILAD) mascherabile
 148       +illegal opcode (ILOP mascherabile)
 149       +security = solo la FLASH e' considerata sicura. Stesso meccanismo di HCS08
 150                   ma governato solo da [FLASH]SECD (0) OFF.Una volta attivato l'unica
 151                   disattivazione e' la cancellazione della FLASH.
 152 *)
 153
 154 (* memoria degli HC05 *)
 155 ndefinition memory_type_of_FamilyHC05 ≝
 156 λm:HC05_mcu_model.match m with
 157   [ MC68HC05J5A ⇒
 158    [
 159   (* astraggo molto *)
 160   (* 0x0000-0x001F,0x0FF0: sarebbe memory mapped IO *)
 161
 162      triple ??? 〈〈x0,x0〉:〈x8,x0〉〉 〈〈x0,x0〉:〈xF,xF〉〉 MEM_READ_WRITE (* 128B RAM+STACK *)
 163    ; triple ??? 〈〈x0,x3〉:〈x0,x0〉〉 〈〈x0,xC〉:〈xF,xF〉〉 MEM_READ_ONLY  (* 2560B USER ROM *)
 164    ; triple ??? 〈〈x0,xE〉:〈x0,x0〉〉 〈〈x0,xF〉:〈xF,xF〉〉 MEM_READ_ONLY  (* 512B INTERNAL ROM *)
 165     ]
 166    (*..*)
 167   ].
 168
 169 (* memoria degli HC08 *)
 170 ndefinition memory_type_of_FamilyHC08 ≝
 171 λm:HC08_mcu_model.match m with
 172   [ MC68HC08AB16A ⇒
 173    [
 174   (* astraggo molto *)
 175   (* 0x0000-0x004F,0xFE00-0xFE01,0xFE03,
 176      0xFE0C-0xFE11,0xFE1A-0xFE1D,0xFE1F: sarebbe memory mapped IO *)
 177   (* 0x0500-0x057F,0xFE02,0xFE04-0xFE07,
 178      0xFE09-0xFE0B,0xFE12-0xFE19,0xFE1E,0xFFC0-0xFFCF : sarebbe reserved *)
 179
 180      triple ??? 〈〈x0,x0〉:〈x5,x0〉〉 〈〈x0,x2〉:〈x4,xF〉〉 MEM_READ_WRITE (* 512B RAM *)
 181    ; triple ??? 〈〈x0,x8〉:〈x0,x0〉〉 〈〈x0,x9〉:〈xF,xF〉〉 MEM_READ_ONLY  (* 512B EEPROM *)
 182    ; triple ??? 〈〈xB,xE〉:〈x0,x0〉〉 〈〈xF,xD〉:〈xF,xF〉〉 MEM_READ_ONLY  (* 16384B ROM *)
 183    ; triple ??? 〈〈xF,xE〉:〈x2,x0〉〉 〈〈xF,xF〉:〈x5,x2〉〉 MEM_READ_ONLY  (* 307B ROM *)
 184    ; triple ??? 〈〈xF,xF〉:〈xD,x0〉〉 〈〈xF,xF〉:〈xF,xF〉〉 MEM_READ_ONLY  (* 48B ROM *) ]
 185    (*..*)
 186   ].
 187
 188 (* memoria degli HCS08 *)
 189 ndefinition memory_type_of_FamilyHCS08 ≝
 190 λm:HCS08_mcu_model.match m with
 191   [ MC9S08AW60 ⇒
 192    [
 193   (* astraggo molto *)
 194   (* 0x0000-0x006F,0x1800-0x185F: sarebbe memory mapped IO *)
 195
 196      triple ??? 〈〈x0,x0〉:〈x7,x0〉〉 〈〈x0,x8〉:〈x6,xF〉〉 MEM_READ_WRITE (* 2048B RAM *)
 197    ; triple ??? 〈〈x0,x8〉:〈x7,x0〉〉 〈〈x1,x7〉:〈xF,xF〉〉 MEM_READ_ONLY  (* 3984B FLASH *)
 198    ; triple ??? 〈〈x1,x8〉:〈x6,x0〉〉 〈〈xF,xF〉:〈xF,xF〉〉 MEM_READ_ONLY  (* 59296B FLASH *) ]
 199   | MC9S08GB60 ⇒
 200    [
 201   (* astraggo molto *)
 202   (* 0x0000-0x006F,0x1800-0x185F: sarebbe memory mapped IO *)
 203
 204      triple ??? 〈〈x0,x0〉:〈x8,x0〉〉 〈〈x1,x0〉:〈x7,xF〉〉 MEM_READ_WRITE (* 4096B RAM *)
 205    ; triple ??? 〈〈x1,x0〉:〈x8,x0〉〉 〈〈x1,x7〉:〈xF,xF〉〉 MEM_READ_ONLY  (* 1920B FLASH *)
 206    ; triple ??? 〈〈x1,x8〉:〈x2,xC〉〉 〈〈xF,xF〉:〈xF,xF〉〉 MEM_READ_ONLY  (* 59348B FLASH *) ]
 207   ].
 208
 209 (* memoria dei RS08 *)
 210 ndefinition memory_type_of_FamilyRS08 ≝
 211 λm:RS08_mcu_model.match m with
 212   [ MC9RS08KA1 ⇒
 213    [
 214      triple ??? 〈〈x0,x0〉:〈x0,x0〉〉 〈〈x0,x0〉:〈x0,xE〉〉 MEM_READ_WRITE (* 15B RAM *)
 215   (* [000F] e' il registro X *)
 216   (* 0x0010-0x001E sarebbe memory mapped IO, proviamo per completezza con RAM *)
 217    ; triple ??? 〈〈x0,x0〉:〈x1,x0〉〉 〈〈x0,x0〉:〈x1,xE〉〉 MEM_READ_WRITE (* 15B MEMORY MAPPED IO *)
 218   (* [001F] e' il registro PAGESEL *)
 219    ; triple ??? 〈〈x0,x0〉:〈x2,x0〉〉 〈〈x0,x0〉:〈x4,xF〉〉 MEM_READ_WRITE (* 48B RAM *)
 220   (* [00C0-00FF] mappato da PAGESEL su [00pp pppp ppxx xxxx] *)
 221    ; triple ??? 〈〈x0,x0〉:〈xC,x0〉〉 〈〈x0,x0〉:〈xF,xF〉〉 MEM_READ_WRITE (* 64B RAM PAGING *)
 222   (* 0x0200-0x023F sarebbe memory mapped IO, proviamo per completezza con RAM *)
 223    ; triple ??? 〈〈x0,x2〉:〈x0,x0〉〉 〈〈x0,x2〉:〈x3,xF〉〉 MEM_READ_WRITE (* 64B MEMORY MAPPED IO *)
 224    ; triple ??? 〈〈x3,xC〉:〈x0,x0〉〉 〈〈x3,xF〉:〈xF,xF〉〉 MEM_READ_ONLY  (* 1024B FLASH *) ]
 225   | MC9RS08KA2 ⇒
 226    [
 227      triple ??? 〈〈x0,x0〉:〈x0,x0〉〉 〈〈x0,x0〉:〈x0,xE〉〉 MEM_READ_WRITE (* 15B RAM *)
 228   (* [000F] e' il registro X *)
 229   (* 0x0010-0x001E sarebbe memory mapped IO, proviamo per completezza con RAM *)
 230    ; triple ??? 〈〈x0,x0〉:〈x1,x0〉〉 〈〈x0,x0〉:〈x1,xE〉〉 MEM_READ_WRITE (* 15B MEMORY MAPPED IO *)
 231   (* [001F] e' il registro PAGESEL *)
 232    ; triple ??? 〈〈x0,x0〉:〈x2,x0〉〉 〈〈x0,x0〉:〈x4,xF〉〉 MEM_READ_WRITE (* 48B RAM *)
 233   (* [00C0-00FF] mappato da PAGESEL su [00pp pppp ppxx xxxx] *)
 234    ; triple ??? 〈〈x0,x0〉:〈xC,x0〉〉 〈〈x0,x0〉:〈xF,xF〉〉 MEM_READ_WRITE (* 64B RAM PAGING *)
 235   (* 0x0200-0x023F sarebbe memory mapped IO, proviamo per completezza con RAM *)
 236    ; triple ??? 〈〈x0,x2〉:〈x0,x0〉〉 〈〈x0,x2〉:〈x3,xF〉〉 MEM_READ_WRITE (* 64B MEMORY MAPPED IO *)
 237    ; triple ??? 〈〈x3,x8〉:〈x0,x0〉〉 〈〈x3,xF〉:〈xF,xF〉〉 MEM_READ_ONLY  (* 2048B FLASH *) ]
 238   ].
 239
 240 (* ∀modello.descrizione della memoria installata *)
 241 ndefinition memory_type_of_mcu_version ≝
 242 λmcu:any_mcu_model.match mcu with
 243  [ FamilyHC05  m ⇒ memory_type_of_FamilyHC05 m
 244  | FamilyHC08  m ⇒ memory_type_of_FamilyHC08 m
 245  | FamilyHCS08 m ⇒ memory_type_of_FamilyHCS08 m
 246  | FamilyRS08  m ⇒ memory_type_of_FamilyRS08 m
 247  ].
 248
 249 (* dato un modello costruisce un descrittore a partire dalla lista precedente *)
 250 nlet rec build_memory_type_of_mcu_version_aux t param (result:aux_chk_type t) on param ≝
 251  match param with
 252   [ nil ⇒ result
 253   | cons hd tl ⇒
 254    build_memory_type_of_mcu_version_aux t tl
 255     (check_update_ranged t result (fst3T ??? hd) (snd3T ??? hd) (thd3T ??? hd)) ].
 256
 257 ndefinition build_memory_type_of_mcu_version ≝
 258 λmcu:any_mcu_model.λt:memory_impl.
 259  build_memory_type_of_mcu_version_aux t (memory_type_of_mcu_version mcu) (out_of_bound_memory t).
 260
 261 (* sarebbe programma da caricare/zero_memory, ora test *)
 262 ndefinition memory_of_mcu_version ≝
 263 λmcu:any_mcu_model.λt:memory_impl.match mcu with
 264  [ FamilyHC05 m ⇒ match m with
 265   [ MC68HC05J5A ⇒ zero_memory t
 266     (*..*)
 267   ]
 268  | FamilyHC08 m ⇒ match m with
 269   [ MC68HC08AB16A ⇒ zero_memory t
 270     (*..*)
 271   ]
 272  (* tralascio l'enumerazione dei casi, per ora e' tutto 0 *)
 273  | FamilyHCS08 _ ⇒ zero_memory t
 274  | FamilyRS08 _ ⇒ zero_memory t
 275  ].
 276
 277 (*
 278    parametrizzati i non deterministici rispetto a tutti i valori casuali
 279    che verranno dati dall'esterno di tipo byte8 (ndby1-2) e bool (ndbo1-5).
 280    l'ACCENSIONE e' totalmente equivalente ad un reset causato da calo di tensione
 281    (reset V-low), la memoria ed il check puo' essere passata, per esempio da
 282    - (memory_of_mcu_version MC68HC05J5A)
 283    - (build_memory_type_of_mcu_version MC68HC05J5A)
 284 *)
 285 ndefinition start_of_mcu_version_HC05 ≝
 286 λmcu:HC05_mcu_model.λt:memory_impl.
 287 λmem:aux_mem_type t.λchk:aux_chk_type t.
 288 λndby1,ndby2:byte8.λirqfl,ndbo1,ndbo2,ndbo3,ndbo4,ndbo5:bool.
 289  let build ≝ λspm,spf,pcm:word16.
 290  let fetched_pc ≝ mk_word16 (mem_read_abs t mem (and_w16 〈〈xF,xF〉:〈xF,xE〉〉 pcm))
 291                             (mem_read_abs t mem (and_w16 〈〈xF,xF〉:〈xF,xF〉〉 pcm)) in
 292   mk_any_status HC05 t
 293    (mk_alu_HC05
 294     (* acc_low: ? *) ndby1 (* indx_low: ? *) ndby2
 295     (* sp: reset *) (or_w16 (and_w16 〈〈x0,x0〉:〈xF,xF〉〉 spm) spf) spm spf
 296     (* pc: reset+fetch *) (and_w16 fetched_pc pcm) pcm
 297     (* H: ? *) ndbo1 (* I: reset *) true (* N: ? *) ndbo2
 298     (* Z: ? *) ndbo3 (* C: ? *) ndbo4 (* IRQ: ? *) irqfl)
 299     (* mem *) mem
 300     (* chk *) chk
 301     (* clk: reset *) (None ?) in
 302  match mcu with
 303   [ MC68HC05J5A ⇒ build 〈〈x0,x0〉:〈x3,xF〉〉 〈〈x0,x0〉:〈xC,x0〉〉 〈〈x0,xF〉:〈xF,xF〉〉
 304     (*..*)
 305   ].
 306
 307 ndefinition start_of_mcu_version_HC08 ≝
 308 λmcu:HC08_mcu_model.λt:memory_impl.
 309 λmem:aux_mem_type t.λchk:aux_chk_type t.
 310 λndby1,ndby2:byte8.λirqfl,ndbo1,ndbo2,ndbo3,ndbo4,ndbo5:bool.
 311  let fetched_pc ≝ mk_word16 (mem_read_abs t mem 〈〈xF,xF〉:〈xF,xE〉〉)
 312                             (mem_read_abs t mem 〈〈xF,xF〉:〈xF,xF〉〉) in
 313   mk_any_status HC08 t
 314    (mk_alu_HC08
 315     (* acc_low: ? *) ndby1 (* indw_low: ? *) ndby2 (* indx_high: reset *)  〈x0,x0〉
 316     (* sp: reset *) 〈〈x0,x0〉:〈xF,xF〉〉 (* pc: reset+fetch *) fetched_pc
 317     (* V: ? *) ndbo1 (* H: ? *) ndbo2 (* I: reset *) true
 318     (* N: ? *) ndbo3 (* Z: ? *) ndbo4 (* C: ? *) ndbo5 (* IRQ: ? *) irqfl)
 319     (* mem *) mem
 320     (* chk *) chk
 321     (* clk: reset *) (None ?).
 322
 323 ndefinition start_of_mcu_version_HCS08 ≝
 324 λmcu:HCS08_mcu_model.λt:memory_impl.
 325 λmem:aux_mem_type t.λchk:aux_chk_type t.
 326 λndby1,ndby2:byte8.λirqfl,ndbo1,ndbo2,ndbo3,ndbo4,ndbo5:bool.
 327  let fetched_pc ≝ mk_word16 (mem_read_abs t mem 〈〈xF,xF〉:〈xF,xE〉〉)
 328                             (mem_read_abs t mem 〈〈xF,xF〉:〈xF,xF〉〉) in
 329   mk_any_status HCS08 t
 330    (mk_alu_HC08
 331     (* acc_low: ? *) ndby1 (* indw_low: ? *) ndby2 (* indx_high: reset *)  〈x0,x0〉
 332     (* sp: reset *) 〈〈x0,x0〉:〈xF,xF〉〉 (* pc: reset+fetch *) fetched_pc
 333     (* V: ? *) ndbo1 (* H: ? *) ndbo2 (* I: reset *) true
 334     (* N: ? *) ndbo3 (* Z: ? *) ndbo4 (* C: ? *) ndbo5 (* IRQ: ? *) irqfl)
 335     (* mem *) mem
 336     (* chk *) chk
 337     (* clk: reset *) (None ?).
 338
 339 ndefinition start_of_mcu_version_RS08 ≝
 340 λmcu:RS08_mcu_model.λt:memory_impl.
 341 λmem:aux_mem_type t.λchk:aux_chk_type t.
 342 λndby1,ndby2:byte8.λirqfl,ndbo1,ndbo2,ndbo3,ndbo4,ndbo5:bool.
 343  let build ≝ λpcm.
 344    mk_any_status RS08 t
 345     (mk_alu_RS08
 346      (* acc_low: reset *)  〈x0,x0〉
 347      (* pc: reset *) (and_w16 〈〈xF,xF〉:〈xF,xD〉〉 pcm) pcm
 348      (* spc: reset *) (and_w16 〈〈xF,xF〉:〈xF,xD〉〉 pcm)
 349      (* xm: reset *) 〈x0,x0〉 (* psm: *) 〈x8,x0〉
 350      (* Z: reset *) false (* C: reset *) false)
 351      (* mem *) mem
 352      (* chk *) chk
 353      (* clk: reset *) (None ?) in
 354   (* tralascio l'enumerazione dei casi, tanto i valori sono uguali *)
 355   build 〈〈x3,xF〉:〈xF,xF〉〉.
 356
 357 (*
 358    cio' che non viene resettato mantiene il valore precedente: nella documentazione
 359    viene riportato come "unaffected"/"indeterminate"/"unpredictable"
 360    il soft RESET e' diverso da un calo di tensione e la ram non variera'
 361 *)
 362 ndefinition reset_of_mcu ≝
 363 λm:mcu_type.λt:memory_impl.
 364 let pc_reset_h ≝ 〈〈xF,xF〉:〈xF,xE〉〉 in
 365 let pc_reset_l ≝ 〈〈xF,xF〉:〈xF,xF〉〉 in
 366 let pc_RS08_reset ≝ 〈〈xF,xF〉:〈xF,xD〉〉 in
 367 let sp_reset ≝ 〈〈x0,x0〉:〈xF,xF〉〉 in
 368  match m return λm:mcu_type.(any_status m t) → (any_status m t) with
 369 (* HC05: parzialmente non deterministico *)
 370   [ HC05 ⇒ λs:any_status HC05 t.match s with
 371    [ mk_any_status alu mem chk clk ⇒ match alu with
 372     [ mk_alu_HC05 acclow indxlow _ spm spf _ pcm hfl _ nfl zfl cfl irqfl ⇒
 373     let fetched_pc ≝ mk_word16 (mem_read_abs t mem (and_w16 pc_reset_h pcm))
 374                                (mem_read_abs t mem (and_w16 pc_reset_l pcm)) in
 375     mk_any_status HC05 t
 376      (mk_alu_HC05
 377       (* acc_low: inv. *) acclow (* indx_low: inv. *) indxlow
 378       (* sp: reset *) (or_w16 (and_w16 sp_reset spm) spf) spm spf
 379       (* pc: reset+fetch *) (and_w16 fetched_pc pcm) pcm
 380       (* H: inv. *) hfl (* I: reset *) true (* N: inv. *) nfl
 381       (* Z: inv. *) zfl (* C: inv. *) cfl (* IRQ: inv *) irqfl)
 382       (* mem: inv. *) mem
 383       (* chk: inv. *) chk
 384       (* clk: reset *) (None ?) ]]
 385 (* HC08: parzialmente non deterministico *)
 386   | HC08 ⇒ λs:any_status HC08 t.match s with
 387    [ mk_any_status alu mem chk clk ⇒ match alu with
 388     [ mk_alu_HC08 acclow indxlow _ _ _ vfl hfl _ nfl zfl cfl irqfl ⇒
 389     let fetched_pc ≝ mk_word16 (mem_read_abs t mem pc_reset_h)
 390                                (mem_read_abs t mem pc_reset_l) in
 391     mk_any_status HC08 t
 392      (mk_alu_HC08
 393       (* acc_low: inv. *) acclow (* indx_low: inv. *) indxlow (* indx_high: reset *) 〈x0,x0〉
 394       (* sp: reset *) sp_reset (* pc: reset+fetch *) fetched_pc
 395       (* V: inv. *) vfl (* H: inv. *) hfl (* I: reset *) true
 396       (* N: inv. *) nfl (* Z: inv. *) zfl (* C: inv. *) cfl (* IRQ: inv *) irqfl)
 397       (* mem: inv. *) mem
 398       (* chk: inv. *) chk
 399       (* clk: reset *) (None ?) ]]
 400 (* HCS08: parzialmente non deterministico *)
 401   | HCS08 ⇒ λs:any_status HCS08 t.match s with
 402    [ mk_any_status alu mem chk clk ⇒ match alu with
 403     [ mk_alu_HC08 acclow indxlow _ _ _ vfl hfl _ nfl zfl cfl irqfl ⇒
 404     let fetched_pc ≝ mk_word16 (mem_read_abs t mem pc_reset_h)
 405                                (mem_read_abs t mem pc_reset_l) in
 406     mk_any_status HCS08 t
 407      (mk_alu_HC08
 408       (* acc_low: inv. *) acclow (* indx_low: inv. *) indxlow (* indx_high: reset *) 〈x0,x0〉
 409       (* sp: reset *) sp_reset (* pc: reset+fetch *) fetched_pc
 410       (* V: inv. *) vfl (* H: inv. *) hfl (* I: reset *) true
 411       (* N: inv. *) nfl (* Z: inv. *) zfl (* C: inv. *) cfl (* IRQ: inv *) irqfl)
 412       (* mem: inv. *) mem
 413       (* chk: inv. *) chk
 414       (* clk: reset *) (None ?) ]]
 415 (* RS08: deterministico *)
 416   | RS08 ⇒ λs:any_status RS08 t.match s with
 417    [ mk_any_status alu mem chk clk ⇒ match alu with
 418     [ mk_alu_RS08 _ _ pcm _ _ _ _ _ ⇒
 419     mk_any_status RS08 t
 420      (mk_alu_RS08
 421       (* acc_low: reset *) 〈x0,x0〉
 422       (* pc: reset *) (and_w16 pc_RS08_reset pcm) pcm
 423       (* spc: reset *) (and_w16 pc_RS08_reset pcm)
 424       (* xm: reset *) 〈x0,x0〉 (* psm: reset *) 〈x8,x0〉
 425       (* Z: reset *) false (* C: reset *) false)
 426       (* mem: inv. *) mem
 427       (* chk: inv. *) chk
 428       (* clk: reset *) (None ?) ]]
 429   ].