1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* ********************************************************************** *)
16 (* Progetto FreeScale *)
19 (* Cosimo Oliboni, oliboni@cs.unibo.it *)
21 (* Questo materiale fa parte della tesi: *)
22 (* "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale" *)
24 (* data ultima modifica 15/11/2007 *)
25 (* ********************************************************************** *)
27 set "baseuri" "cic:/matita/freescale/model/".
29 (*include "/media/VIRTUOSO/freescale/status.ma".*)
30 include "freescale/status.ma".
32 (* *********************************** *)
33 (* IMPOSTAZIONI SPECIFICHE DEI MODELLI *)
34 (* *********************************** *)
37 inductive HC05_mcu_model : Type ≝
38 MC68HC05J5A: HC05_mcu_model
42 inductive HC08_mcu_model : Type ≝
43 MC68HC08AB16A: HC08_mcu_model
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.
82 inductive RS08_mcu_model : Type ≝
83 MC9RS08KA1 : RS08_mcu_model
84 | MC9RS08KA2 : RS08_mcu_model.
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.
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).
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)
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
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.
123 (* memoria degli HC05 *)
124 definition memory_type_of_FamilyHC05 ≝
125 λm:HC05_mcu_model.match m with
129 (* 0x0000-0x001F,0x0FF0: sarebbe memory mapped IO *)
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 *)
138 (* memoria degli HC08 *)
139 definition memory_type_of_FamilyHC08 ≝
140 λm:HC08_mcu_model.match m with
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 *)
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 *) ]
157 (* memoria degli HCS08 *)
158 definition memory_type_of_FamilyHCS08 ≝
159 λm:HCS08_mcu_model.match m with
163 (* 0x0000-0x006F,0x1800-0x185F: sarebbe memory mapped IO *)
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 *) ]
171 (* 0x0000-0x007F,0x1800-0x182B: sarebbe memory mapped IO *)
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 *) ]
179 (* 0x0000-0x007F,0x1800-0x182B: sarebbe memory mapped IO *)
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 *) ]
187 (* 0x0000-0x007F,0x1800-0x182B: sarebbe memory mapped IO *)
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 *) ]
194 (* 0x0000-0x007F,0x1800-0x182B: sarebbe memory mapped IO *)
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 *) ]
201 (* 0x0000-0x007F,0x1800-0x182B: sarebbe memory mapped IO *)
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 *) ]
208 (* 0x0000-0x007F,0x1800-0x182B: sarebbe memory mapped IO *)
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 *) ]
216 (* 0x0000-0x007F,0x1800-0x182B: sarebbe memory mapped IO *)
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 *) ]
224 (* 0x0000-0x007F,0x1800-0x182B: sarebbe memory mapped IO *)
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 *) ]
231 (* 0x0000-0x007F,0x1800-0x182B: sarebbe memory mapped IO *)
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 *) ]
238 (* 0x0000-0x007F,0x1800-0x182B: sarebbe memory mapped IO *)
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 *) ]
245 (* 0x0000-0x007F,0x1800-0x182B: sarebbe memory mapped IO *)
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 *) ]
252 (* 0x0000-0x005F,0x1800-0x186F: sarebbe memory mapped IO *)
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 *) ]
260 (* 0x0000-0x005F,0x1800-0x186F: sarebbe memory mapped IO *)
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 *) ]
268 (* 0x0000-0x005F,0x1800-0x184F: sarebbe memory mapped IO *)
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 *) ]
275 (* 0x0000-0x005F,0x1800-0x184F: sarebbe memory mapped IO *)
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 *) ]
282 (* 0x0000-0x005F,0x1800-0x184F: sarebbe memory mapped IO *)
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 *) ]
289 (* 0x0000-0x005F,0x1800-0x184F: sarebbe memory mapped IO *)
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 *) ]
296 (* 0x0000-0x0045,0x1800-0x182B: sarebbe memory mapped IO *)
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 *) ]
304 (* 0x0000-0x0045,0x1800-0x182B: sarebbe memory mapped IO *)
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 *) ]
312 (* 0x0000-0x0045,0x1800-0x182B: sarebbe memory mapped IO *)
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 *) ]
320 (* 0x0000-0x0045,0x1800-0x182B: sarebbe memory mapped IO *)
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 *) ]
328 (* 0x0000-0x0045,0x1800-0x182B: sarebbe memory mapped IO *)
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 *) ]
335 (* 0x0000-0x0045,0x1800-0x182B: sarebbe memory mapped IO *)
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 *) ]
342 (* 0x0000-0x0045,0x1800-0x182B: sarebbe memory mapped IO *)
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 *) ]
349 (* 0x0000-0x0045,0x1800-0x182B: sarebbe memory mapped IO *)
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 *) ]
356 (* 0x0000-0x003F,0x1800-0x182B: sarebbe memory mapped IO *)
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 *) ]
363 (* 0x0000-0x003F,0x1800-0x182B: sarebbe memory mapped IO *)
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 *) ]
370 (* 0x0000-0x003F,0x1800-0x182B: sarebbe memory mapped IO *)
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 *) ]
377 (* 0x0000-0x003F,0x1800-0x182B: sarebbe memory mapped IO *)
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 *) ]
384 (* 0x0000-0x003F,0x1800-0x182B: sarebbe memory mapped IO *)
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 *) ]
391 (* 0x0000-0x003F,0x1800-0x182B: sarebbe memory mapped IO *)
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 *) ]
397 (* memoria dei RS08 *)
398 definition memory_type_of_FamilyRS08 ≝
399 λm:RS08_mcu_model.match m with
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 *) ]
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 *) ]
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
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 ≝
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).
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
454 | FamilyHC08 m ⇒ match m with
455 [ MC68HC08AB16A ⇒ zero_memory t
458 (* tralascio l'enumerazione dei casi, per ora e' tutto 0 *)
459 | FamilyHCS08 _ ⇒ zero_memory t
460 | FamilyRS08 _ ⇒ zero_memory t
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
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)
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
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
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
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)
505 (* clk: reset *) (None ?) in
507 [ MC68HC05J5A ⇒ build 〈〈x0,x0〉:〈x3,xF〉〉 〈〈x0,x0〉:〈xC,x0〉〉 〈〈x0,xF〉:〈xF,xF〉〉
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.
515 let fetched_pc ≝ mk_word16 (mem_read_abs t mem pc_reset_h)
516 (mem_read_abs t mem pc_reset_l) in
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)
525 (* clk: reset *) (None ?) in
526 (* tralascio l'enumerazione dei casi, tanto non ci sono maschere da impostare *)
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.
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
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)
543 (* clk: reset *) (None ?) in
544 (* tralascio l'enumerazione dei casi, tanto non ci sono maschere da impostare *)
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.
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)
560 (* clk: reset *) (None ?) in
561 (* tralascio l'enumerazione dei casi, tanto i valori sono uguali *)
562 build 〈〈x3,xF〉:〈xF,xF〉〉
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'
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
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)
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
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)
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
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)
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 _ _ _ _ _ ⇒
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)
636 (* clk: reset *) (None ?) ]]