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 include "freescale/status.ma".
29 (* *********************************** *)
30 (* IMPOSTAZIONI SPECIFICHE DEI MODELLI *)
31 (* *********************************** *)
34 inductive HC05_mcu_model : Type ≝
35 MC68HC05J5A: HC05_mcu_model
39 inductive HC08_mcu_model : Type ≝
40 MC68HC08AB16A: HC08_mcu_model
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.
79 inductive RS08_mcu_model : Type ≝
80 MC9RS08KA1 : RS08_mcu_model
81 | MC9RS08KA2 : RS08_mcu_model.
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.
96 condizioni errore interne alla MCU
97 (Il programma viene caricato dal produttore in ROM o impostato in EEPROM)
98 HC05: +illegal address during opcode fetch
99 HC08: +illegal address duting opcode fetch (ILAD mascherabile)
100 +illegal opcode (ILOP mascherabile)
102 (Il programma viene programmato nella FLASH)
103 HCS08: +illegal address during opcode fetch (ILAD mascherabile)
104 +illegal opcode (ILOP mascherabile)
105 +security = accesso a RAM e zone FLASH dichiarate sicure da zone sicure
106 da' 0 in lettura e ignore in scrittura, [FLASH]SEC00:SEC01 (1,0)
107 corrisponde a OFF, altre ON, disattivabile solo da modalita' sicura se
108 opzione [FLASH]KEYEN e' 1 passando chiave a 8byte da modalita' sicura.
109 Altrimenti disattivabile solo con FLASH mass erase. Obbiettivo
110 e' impedire duplicazione di software di controllo, dato che esiste
111 modalita' debugging. A restart viene ricaricata da FLASH impostazione
113 RS08: +illegal address durting opcode fetch (ILAD) mascherabile
114 +illegal opcode (ILOP mascherabile)
115 +security = solo la FLASH e' considerata sicura. Stesso meccanismo di HCS08
116 ma governato solo da [FLASH]SECD (0) OFF.Una volta attivato l'unica
117 disattivazione e' la cancellazione della FLASH.
120 (* memoria degli HC05 *)
121 definition memory_type_of_FamilyHC05 ≝
122 λm:HC05_mcu_model.match m with
126 (* 0x0000-0x001F,0x0FF0: sarebbe memory mapped IO *)
128 tripleT ??? 〈〈x0,x0〉:〈x8,x0〉〉 〈〈x0,x0〉:〈xF,xF〉〉 MEM_READ_WRITE (* 128B RAM+STACK *)
129 ; tripleT ??? 〈〈x0,x3〉:〈x0,x0〉〉 〈〈x0,xC〉:〈xF,xF〉〉 MEM_READ_ONLY (* 2560B USER ROM *)
130 ; tripleT ??? 〈〈x0,xE〉:〈x0,x0〉〉 〈〈x0,xF〉:〈xF,xF〉〉 MEM_READ_ONLY (* 512B INTERNAL ROM *)
135 (* memoria degli HC08 *)
136 definition memory_type_of_FamilyHC08 ≝
137 λm:HC08_mcu_model.match m with
141 (* 0x0000-0x004F,0xFE00-0xFE01,0xFE03,
142 0xFE0C-0xFE11,0xFE1A-0xFE1D,0xFE1F: sarebbe memory mapped IO *)
143 (* 0x0500-0x057F,0xFE02,0xFE04-0xFE07,
144 0xFE09-0xFE0B,0xFE12-0xFE19,0xFE1E,0xFFC0-0xFFCF : sarebbe reserved *)
146 tripleT ??? 〈〈x0,x0〉:〈x5,x0〉〉 〈〈x0,x2〉:〈x4,xF〉〉 MEM_READ_WRITE (* 512B RAM *)
147 ; tripleT ??? 〈〈x0,x8〉:〈x0,x0〉〉 〈〈x0,x9〉:〈xF,xF〉〉 MEM_READ_ONLY (* 512B EEPROM *)
148 ; tripleT ??? 〈〈xB,xE〉:〈x0,x0〉〉 〈〈xF,xD〉:〈xF,xF〉〉 MEM_READ_ONLY (* 16384B ROM *)
149 ; tripleT ??? 〈〈xF,xE〉:〈x2,x0〉〉 〈〈xF,xF〉:〈x5,x2〉〉 MEM_READ_ONLY (* 307B ROM *)
150 ; tripleT ??? 〈〈xF,xF〉:〈xD,x0〉〉 〈〈xF,xF〉:〈xF,xF〉〉 MEM_READ_ONLY (* 48B ROM *) ]
154 (* memoria degli HCS08 *)
155 definition memory_type_of_FamilyHCS08 ≝
156 λm:HCS08_mcu_model.match m with
160 (* 0x0000-0x006F,0x1800-0x185F: sarebbe memory mapped IO *)
162 tripleT ??? 〈〈x0,x0〉:〈x7,x0〉〉 〈〈x0,x8〉:〈x6,xF〉〉 MEM_READ_WRITE (* 2048B RAM *)
163 ; tripleT ??? 〈〈x0,x8〉:〈x7,x0〉〉 〈〈x1,x7〉:〈xF,xF〉〉 MEM_READ_ONLY (* 3984B FLASH *)
164 ; tripleT ??? 〈〈x1,x8〉:〈x6,x0〉〉 〈〈xF,xF〉:〈xF,xF〉〉 MEM_READ_ONLY (* 59296B FLASH *) ]
168 (* 0x0000-0x007F,0x1800-0x182B: sarebbe memory mapped IO *)
170 tripleT ??? 〈〈x0,x0〉:〈x8,x0〉〉 〈〈x1,x0〉:〈x7,xF〉〉 MEM_READ_WRITE (* 4096B RAM *)
171 ; tripleT ??? 〈〈x1,x0〉:〈x8,x0〉〉 〈〈x1,x7〉:〈xF,xF〉〉 MEM_READ_ONLY (* 1920B FLASH *)
172 ; tripleT ??? 〈〈x1,x8〉:〈x2,xC〉〉 〈〈xF,xF〉:〈xF,xF〉〉 MEM_READ_ONLY (* 59348B FLASH *) ]
176 (* 0x0000-0x007F,0x1800-0x182B: sarebbe memory mapped IO *)
178 tripleT ??? 〈〈x0,x0〉:〈x8,x0〉〉 〈〈x1,x0〉:〈x7,xF〉〉 MEM_READ_WRITE (* 4096B RAM *)
179 ; tripleT ??? 〈〈x1,x0〉:〈x8,x0〉〉 〈〈x1,x7〉:〈xF,xF〉〉 MEM_READ_ONLY (* 1920B FLASH *)
180 ; tripleT ??? 〈〈x1,x8〉:〈x2,xC〉〉 〈〈xF,xF〉:〈xF,xF〉〉 MEM_READ_ONLY (* 59348B FLASH *) ]
184 (* 0x0000-0x007F,0x1800-0x182B: sarebbe memory mapped IO *)
186 tripleT ??? 〈〈x0,x0〉:〈x8,x0〉〉 〈〈x0,x8〉:〈x7,xF〉〉 MEM_READ_WRITE (* 2048B RAM *)
187 ; tripleT ??? 〈〈x8,x0〉:〈x0,x0〉〉 〈〈xF,xF〉:〈xF,xF〉〉 MEM_READ_ONLY (* 32768B FLASH *) ]
191 (* 0x0000-0x007F,0x1800-0x182B: sarebbe memory mapped IO *)
193 tripleT ??? 〈〈x0,x0〉:〈x8,x0〉〉 〈〈x0,x8〉:〈x7,xF〉〉 MEM_READ_WRITE (* 2048B RAM *)
194 ; tripleT ??? 〈〈x8,x0〉:〈x0,x0〉〉 〈〈xF,xF〉:〈xF,xF〉〉 MEM_READ_ONLY (* 32768B FLASH *) ]
198 (* 0x0000-0x007F,0x1800-0x182B: sarebbe memory mapped IO *)
200 tripleT ??? 〈〈x0,x0〉:〈x8,x0〉〉 〈〈x0,x4〉:〈x7,xF〉〉 MEM_READ_WRITE (* 1024B RAM *)
201 ; tripleT ??? 〈〈xC,x0〉:〈x0,x0〉〉 〈〈xF,xF〉:〈xF,xF〉〉 MEM_READ_ONLY (* 16384B FLASH *) ]
205 (* 0x0000-0x007F,0x1800-0x182B: sarebbe memory mapped IO *)
207 tripleT ??? 〈〈x0,x0〉:〈x8,x0〉〉 〈〈x1,x0〉:〈x7,xF〉〉 MEM_READ_WRITE (* 4096B RAM *)
208 ; tripleT ??? 〈〈x1,x0〉:〈x8,x0〉〉 〈〈x1,x7〉:〈xF,xF〉〉 MEM_READ_ONLY (* 1920B FLASH *)
209 ; tripleT ??? 〈〈x1,x8〉:〈x2,xC〉〉 〈〈xF,xF〉:〈xF,xF〉〉 MEM_READ_ONLY (* 59348B FLASH *) ]
213 (* 0x0000-0x007F,0x1800-0x182B: sarebbe memory mapped IO *)
215 tripleT ??? 〈〈x0,x0〉:〈x8,x0〉〉 〈〈x1,x0〉:〈x7,xF〉〉 MEM_READ_WRITE (* 4096B RAM *)
216 ; tripleT ??? 〈〈x1,x0〉:〈x8,x0〉〉 〈〈x1,x7〉:〈xF,xF〉〉 MEM_READ_ONLY (* 1920B FLASH *)
217 ; tripleT ??? 〈〈x1,x8〉:〈x2,xC〉〉 〈〈xF,xF〉:〈xF,xF〉〉 MEM_READ_ONLY (* 59348B FLASH *) ]
221 (* 0x0000-0x007F,0x1800-0x182B: sarebbe memory mapped IO *)
223 tripleT ??? 〈〈x0,x0〉:〈x8,x0〉〉 〈〈x0,x8〉:〈x7,xF〉〉 MEM_READ_WRITE (* 2048B RAM *)
224 ; tripleT ??? 〈〈x8,x0〉:〈x0,x0〉〉 〈〈xF,xF〉:〈xF,xF〉〉 MEM_READ_ONLY (* 32768B FLASH *) ]
228 (* 0x0000-0x007F,0x1800-0x182B: sarebbe memory mapped IO *)
230 tripleT ??? 〈〈x0,x0〉:〈x8,x0〉〉 〈〈x0,x8〉:〈x7,xF〉〉 MEM_READ_WRITE (* 2048B RAM *)
231 ; tripleT ??? 〈〈x8,x0〉:〈x0,x0〉〉 〈〈xF,xF〉:〈xF,xF〉〉 MEM_READ_ONLY (* 32768B FLASH *) ]
235 (* 0x0000-0x007F,0x1800-0x182B: sarebbe memory mapped IO *)
237 tripleT ??? 〈〈x0,x0〉:〈x8,x0〉〉 〈〈x0,x8〉:〈x7,xF〉〉 MEM_READ_WRITE (* 2048B RAM *)
238 ; tripleT ??? 〈〈xC,x0〉:〈x0,x0〉〉 〈〈xF,xF〉:〈xF,xF〉〉 MEM_READ_ONLY (* 16384B FLASH *) ]
242 (* 0x0000-0x007F,0x1800-0x182B: sarebbe memory mapped IO *)
244 tripleT ??? 〈〈x0,x0〉:〈x8,x0〉〉 〈〈x0,x8〉:〈x7,xF〉〉 MEM_READ_WRITE (* 2048B RAM *)
245 ; tripleT ??? 〈〈xC,x0〉:〈x0,x0〉〉 〈〈xF,xF〉:〈xF,xF〉〉 MEM_READ_ONLY (* 16384B FLASH *) ]
249 (* 0x0000-0x005F,0x1800-0x186F: sarebbe memory mapped IO *)
251 tripleT ??? 〈〈x0,x0〉:〈x6,x0〉〉 〈〈x1,x0〉:〈x5,xF〉〉 MEM_READ_WRITE (* 4096B RAM *)
252 ; tripleT ??? 〈〈x1,x0〉:〈x6,x0〉〉 〈〈x1,x7〉:〈xF,xF〉〉 MEM_READ_ONLY (* 1952B FLASH *)
253 ; tripleT ??? 〈〈x1,x8〉:〈x7,x0〉〉 〈〈xF,xF〉:〈xF,xF〉〉 MEM_READ_ONLY (* 59280B FLASH *) ]
257 (* 0x0000-0x005F,0x1800-0x186F: sarebbe memory mapped IO *)
259 tripleT ??? 〈〈x0,x0〉:〈x6,x0〉〉 〈〈x0,xA〉:〈x5,xF〉〉 MEM_READ_WRITE (* 2560B RAM *)
260 ; tripleT ??? 〈〈x1,x8〉:〈x7,x0〉〉 〈〈x4,x8〉:〈x6,xF〉〉 MEM_READ_ONLY (* 12288B FLASH *)
261 ; tripleT ??? 〈〈xA,x0〉:〈x0,x0〉〉 〈〈xF,xF〉:〈xF,xF〉〉 MEM_READ_ONLY (* 24576B FLASH *) ]
265 (* 0x0000-0x005F,0x1800-0x184F: sarebbe memory mapped IO *)
267 tripleT ??? 〈〈x0,x0〉:〈x6,x0〉〉 〈〈x0,x1〉:〈x5,xF〉〉 MEM_READ_WRITE (* 256B RAM *)
268 ; tripleT ??? 〈〈xF,x0〉:〈x0,x0〉〉 〈〈xF,xF〉:〈xF,xF〉〉 MEM_READ_ONLY (* 4096B FLASH *) ]
272 (* 0x0000-0x005F,0x1800-0x184F: sarebbe memory mapped IO *)
274 tripleT ??? 〈〈x0,x0〉:〈x6,x0〉〉 〈〈x0,x1〉:〈x5,xF〉〉 MEM_READ_WRITE (* 256B RAM *)
275 ; tripleT ??? 〈〈xF,x0〉:〈x0,x0〉〉 〈〈xF,xF〉:〈xF,xF〉〉 MEM_READ_ONLY (* 4096B FLASH *) ]
279 (* 0x0000-0x005F,0x1800-0x184F: sarebbe memory mapped IO *)
281 tripleT ??? 〈〈x0,x0〉:〈x6,x0〉〉 〈〈x0,x2〉:〈x5,xF〉〉 MEM_READ_WRITE (* 512B RAM *)
282 ; tripleT ??? 〈〈xE,x0〉:〈x0,x0〉〉 〈〈xF,xF〉:〈xF,xF〉〉 MEM_READ_ONLY (* 8192B FLASH *) ]
286 (* 0x0000-0x005F,0x1800-0x184F: sarebbe memory mapped IO *)
288 tripleT ??? 〈〈x0,x0〉:〈x6,x0〉〉 〈〈x0,x2〉:〈x5,xF〉〉 MEM_READ_WRITE (* 512B RAM *)
289 ; tripleT ??? 〈〈xE,x0〉:〈x0,x0〉〉 〈〈xF,xF〉:〈xF,xF〉〉 MEM_READ_ONLY (* 8192B FLASH *) ]
293 (* 0x0000-0x0045,0x1800-0x182B: sarebbe memory mapped IO *)
295 tripleT ??? 〈〈x0,x0〉:〈x4,x6〉〉 〈〈x0,x8〉:〈x4,x5〉〉 MEM_READ_WRITE (* 2048B RAM *)
296 ; tripleT ??? 〈〈x0,x8〉:〈x4,x6〉〉 〈〈x1,x7〉:〈xF,xF〉〉 MEM_READ_ONLY (* 4026B FLASH *)
297 ; tripleT ??? 〈〈x1,x8〉:〈x2,xC〉〉 〈〈xF,xF〉:〈xF,xF〉〉 MEM_READ_ONLY (* 59348B FLASH *) ]
301 (* 0x0000-0x0045,0x1800-0x182B: sarebbe memory mapped IO *)
303 tripleT ??? 〈〈x0,x0〉:〈x4,x6〉〉 〈〈x0,x8〉:〈x4,x5〉〉 MEM_READ_WRITE (* 2048B RAM *)
304 ; tripleT ??? 〈〈x0,x8〉:〈x4,x6〉〉 〈〈x1,x7〉:〈xF,xF〉〉 MEM_READ_ONLY (* 4026B FLASH *)
305 ; tripleT ??? 〈〈x1,x8〉:〈x2,xC〉〉 〈〈xF,xF〉:〈xF,xF〉〉 MEM_READ_ONLY (* 59348B FLASH *) ]
309 (* 0x0000-0x0045,0x1800-0x182B: sarebbe memory mapped IO *)
311 tripleT ??? 〈〈x0,x0〉:〈x4,x6〉〉 〈〈x0,x8〉:〈x4,x5〉〉 MEM_READ_WRITE (* 2048B RAM *)
312 ; tripleT ??? 〈〈x0,x8〉:〈x4,x6〉〉 〈〈x1,x7〉:〈xF,xF〉〉 MEM_READ_ONLY (* 4026B FLASH *)
313 ; tripleT ??? 〈〈x1,x8〉:〈x2,xC〉〉 〈〈xF,xF〉:〈xF,xF〉〉 MEM_READ_ONLY (* 59348B FLASH *) ]
317 (* 0x0000-0x0045,0x1800-0x182B: sarebbe memory mapped IO *)
319 tripleT ??? 〈〈x0,x0〉:〈x4,x6〉〉 〈〈x0,x8〉:〈x4,x5〉〉 MEM_READ_WRITE (* 2048B RAM *)
320 ; tripleT ??? 〈〈x0,x8〉:〈x4,x6〉〉 〈〈x1,x7〉:〈xF,xF〉〉 MEM_READ_ONLY (* 4026B FLASH *)
321 ; tripleT ??? 〈〈x1,x8〉:〈x2,xC〉〉 〈〈xF,xF〉:〈xF,xF〉〉 MEM_READ_ONLY (* 59348B FLASH *) ]
325 (* 0x0000-0x0045,0x1800-0x182B: sarebbe memory mapped IO *)
327 tripleT ??? 〈〈x0,x0〉:〈x4,x6〉〉 〈〈x0,x8〉:〈x4,x5〉〉 MEM_READ_WRITE (* 2048B RAM *)
328 ; tripleT ??? 〈〈x8,x0〉:〈x0,x0〉〉 〈〈xF,xF〉:〈xF,xF〉〉 MEM_READ_ONLY (* 32768B FLASH *) ]
332 (* 0x0000-0x0045,0x1800-0x182B: sarebbe memory mapped IO *)
334 tripleT ??? 〈〈x0,x0〉:〈x4,x6〉〉 〈〈x0,x8〉:〈x4,x5〉〉 MEM_READ_WRITE (* 2048B RAM *)
335 ; tripleT ??? 〈〈x8,x0〉:〈x0,x0〉〉 〈〈xF,xF〉:〈xF,xF〉〉 MEM_READ_ONLY (* 32768B FLASH *) ]
339 (* 0x0000-0x0045,0x1800-0x182B: sarebbe memory mapped IO *)
341 tripleT ??? 〈〈x0,x0〉:〈x4,x6〉〉 〈〈x0,x8〉:〈x4,x5〉〉 MEM_READ_WRITE (* 2048B RAM *)
342 ; tripleT ??? 〈〈x8,x0〉:〈x0,x0〉〉 〈〈xF,xF〉:〈xF,xF〉〉 MEM_READ_ONLY (* 32768B FLASH *) ]
346 (* 0x0000-0x0045,0x1800-0x182B: sarebbe memory mapped IO *)
348 tripleT ??? 〈〈x0,x0〉:〈x4,x6〉〉 〈〈x0,x8〉:〈x4,x5〉〉 MEM_READ_WRITE (* 2048B RAM *)
349 ; tripleT ??? 〈〈x8,x0〉:〈x0,x0〉〉 〈〈xF,xF〉:〈xF,xF〉〉 MEM_READ_ONLY (* 32768B FLASH *) ]
353 (* 0x0000-0x003F,0x1800-0x182B: sarebbe memory mapped IO *)
355 tripleT ??? 〈〈x0,x0〉:〈x4,x0〉〉 〈〈x0,x4〉:〈x3,xF〉〉 MEM_READ_WRITE (* 1024B RAM *)
356 ; tripleT ??? 〈〈xC,x0〉:〈x0,x0〉〉 〈〈xF,xF〉:〈xF,xF〉〉 MEM_READ_ONLY (* 16384B FLASH *) ]
360 (* 0x0000-0x003F,0x1800-0x182B: sarebbe memory mapped IO *)
362 tripleT ??? 〈〈x0,x0〉:〈x4,x0〉〉 〈〈x0,x4〉:〈x3,xF〉〉 MEM_READ_WRITE (* 1024B RAM *)
363 ; tripleT ??? 〈〈xC,x0〉:〈x0,x0〉〉 〈〈xF,xF〉:〈xF,xF〉〉 MEM_READ_ONLY (* 16384B FLASH *) ]
367 (* 0x0000-0x003F,0x1800-0x182B: sarebbe memory mapped IO *)
369 tripleT ??? 〈〈x0,x0〉:〈x4,x0〉〉 〈〈x0,x4〉:〈x3,xF〉〉 MEM_READ_WRITE (* 1024B RAM *)
370 ; tripleT ??? 〈〈xC,x0〉:〈x0,x0〉〉 〈〈xF,xF〉:〈xF,xF〉〉 MEM_READ_ONLY (* 16384B FLASH *) ]
374 (* 0x0000-0x003F,0x1800-0x182B: sarebbe memory mapped IO *)
376 tripleT ??? 〈〈x0,x0〉:〈x4,x0〉〉 〈〈x0,x4〉:〈x3,xF〉〉 MEM_READ_WRITE (* 1024B RAM *)
377 ; tripleT ??? 〈〈xE,x0〉:〈x0,x0〉〉 〈〈xF,xF〉:〈xF,xF〉〉 MEM_READ_ONLY (* 8192B FLASH *) ]
381 (* 0x0000-0x003F,0x1800-0x182B: sarebbe memory mapped IO *)
383 tripleT ??? 〈〈x0,x0〉:〈x4,x0〉〉 〈〈x0,x4〉:〈x3,xF〉〉 MEM_READ_WRITE (* 1024B RAM *)
384 ; tripleT ??? 〈〈xE,x0〉:〈x0,x0〉〉 〈〈xF,xF〉:〈xF,xF〉〉 MEM_READ_ONLY (* 8192B FLASH *) ]
388 (* 0x0000-0x003F,0x1800-0x182B: sarebbe memory mapped IO *)
390 tripleT ??? 〈〈x0,x0〉:〈x4,x0〉〉 〈〈x0,x4〉:〈x3,xF〉〉 MEM_READ_WRITE (* 1024B RAM *)
391 ; tripleT ??? 〈〈xE,x0〉:〈x0,x0〉〉 〈〈xF,xF〉:〈xF,xF〉〉 MEM_READ_ONLY (* 8192B FLASH *) ]
394 (* memoria dei RS08 *)
395 definition memory_type_of_FamilyRS08 ≝
396 λm:RS08_mcu_model.match m with
399 tripleT ??? 〈〈x0,x0〉:〈x0,x0〉〉 〈〈x0,x0〉:〈x0,xE〉〉 MEM_READ_WRITE (* 15B RAM *)
400 (* [000F] e' il registro X *)
401 (* 0x0010-0x001E sarebbe memory mapped IO, proviamo per completezza con RAM *)
402 ; tripleT ??? 〈〈x0,x0〉:〈x1,x0〉〉 〈〈x0,x0〉:〈x1,xE〉〉 MEM_READ_WRITE (* 15B MEMORY MAPPED IO *)
403 (* [001F] e' il registro PAGESEL *)
404 ; tripleT ??? 〈〈x0,x0〉:〈x2,x0〉〉 〈〈x0,x0〉:〈x4,xF〉〉 MEM_READ_WRITE (* 48B RAM *)
405 (* [00C0-00FF] mappato da PAGESEL su [00pp pppp ppxx xxxx] *)
406 ; tripleT ??? 〈〈x0,x0〉:〈xC,x0〉〉 〈〈x0,x0〉:〈xF,xF〉〉 MEM_READ_WRITE (* 64B RAM PAGING *)
407 (* 0x0200-0x023F sarebbe memory mapped IO, proviamo per completezza con RAM *)
408 ; tripleT ??? 〈〈x0,x2〉:〈x0,x0〉〉 〈〈x0,x2〉:〈x3,xF〉〉 MEM_READ_WRITE (* 64B MEMORY MAPPED IO *)
409 ; tripleT ??? 〈〈x3,xC〉:〈x0,x0〉〉 〈〈x3,xF〉:〈xF,xF〉〉 MEM_READ_ONLY (* 1024B FLASH *) ]
412 tripleT ??? 〈〈x0,x0〉:〈x0,x0〉〉 〈〈x0,x0〉:〈x0,xE〉〉 MEM_READ_WRITE (* 15B RAM *)
413 (* [000F] e' il registro X *)
414 (* 0x0010-0x001E sarebbe memory mapped IO, proviamo per completezza con RAM *)
415 ; tripleT ??? 〈〈x0,x0〉:〈x1,x0〉〉 〈〈x0,x0〉:〈x1,xE〉〉 MEM_READ_WRITE (* 15B MEMORY MAPPED IO *)
416 (* [001F] e' il registro PAGESEL *)
417 ; tripleT ??? 〈〈x0,x0〉:〈x2,x0〉〉 〈〈x0,x0〉:〈x4,xF〉〉 MEM_READ_WRITE (* 48B RAM *)
418 (* [00C0-00FF] mappato da PAGESEL su [00pp pppp ppxx xxxx] *)
419 ; tripleT ??? 〈〈x0,x0〉:〈xC,x0〉〉 〈〈x0,x0〉:〈xF,xF〉〉 MEM_READ_WRITE (* 64B RAM PAGING *)
420 (* 0x0200-0x023F sarebbe memory mapped IO, proviamo per completezza con RAM *)
421 ; tripleT ??? 〈〈x0,x2〉:〈x0,x0〉〉 〈〈x0,x2〉:〈x3,xF〉〉 MEM_READ_WRITE (* 64B MEMORY MAPPED IO *)
422 ; tripleT ??? 〈〈x3,x8〉:〈x0,x0〉〉 〈〈x3,xF〉:〈xF,xF〉〉 MEM_READ_ONLY (* 2048B FLASH *) ]
425 (* ∀modello.descrizione della memoria installata *)
426 definition memory_type_of_mcu_version ≝
427 λmcu:any_mcu_model.match mcu with
428 [ FamilyHC05 m ⇒ memory_type_of_FamilyHC05 m
429 | FamilyHC08 m ⇒ memory_type_of_FamilyHC08 m
430 | FamilyHCS08 m ⇒ memory_type_of_FamilyHCS08 m
431 | FamilyRS08 m ⇒ memory_type_of_FamilyRS08 m
434 (* dato un modello costruisce un descrittore a partire dalla lista precedente *)
435 definition build_memory_type_of_mcu_version ≝
436 λmcu:any_mcu_model.λt:memory_impl.
437 let rec aux param result ≝
441 aux tl (check_update_ranged t result (fst3T ??? hd) (snd3T ??? hd) (thd3T ??? hd)) ]
442 in aux (memory_type_of_mcu_version mcu) (out_of_bound_memory t).
444 (* sarebbe programma da caricare/zero_memory, ora test *)
445 definition memory_of_mcu_version ≝
446 λmcu:any_mcu_model.λt:memory_impl.match mcu with
447 [ FamilyHC05 m ⇒ match m with
448 [ MC68HC05J5A ⇒ zero_memory t
451 | FamilyHC08 m ⇒ match m with
452 [ MC68HC08AB16A ⇒ zero_memory t
455 (* tralascio l'enumerazione dei casi, per ora e' tutto 0 *)
456 | FamilyHCS08 _ ⇒ zero_memory t
457 | FamilyRS08 _ ⇒ zero_memory t
460 (* inferire la mcu a partire dal modello *)
461 definition mcu_of_model ≝
462 λm:any_mcu_model.match m with
463 [ FamilyHC05 _ ⇒ HC05
464 | FamilyHC08 _ ⇒ HC08
465 | FamilyHCS08 _ ⇒ HCS08
466 | FamilyRS08 _ ⇒ RS08
470 parametrizzati i non deterministici rispetto a tutti i valori casuali
471 che verranno dati dall'esterno di tipo byte8 (ndby1-2) e bool (ndbo1-5).
472 l'ACCENSIONE e' totalmente equivalente ad un reset causato da calo di tensione
473 (reset V-low), la memoria ed il check puo' essere passata, per esempio da
474 - (memory_of_mcu_version MC68HC05J5A)
475 - (build_memory_type_of_mcu_version MC68HC05J5A)
477 definition start_of_mcu_version ≝
478 λmcu:any_mcu_model.λt:memory_impl.
479 let pc_reset_h ≝ 〈〈xF,xF〉:〈xF,xE〉〉 in
480 let pc_reset_l ≝ 〈〈xF,xF〉:〈xF,xF〉〉 in
481 let pc_RS08_reset ≝ 〈〈xF,xF〉:〈xF,xD〉〉 in
482 let sp_reset ≝ 〈〈x0,x0〉:〈xF,xF〉〉 in
484 return λmcu:any_mcu_model.(aux_mem_type t) → (aux_chk_type t) → byte8 → byte8 →
485 bool → bool → bool → bool → bool → bool → any_status (mcu_of_model mcu) t
487 (* HC05: parzialmente non deterministico *)
488 [ FamilyHC05 m ⇒ λmem:aux_mem_type t.λchk:aux_chk_type t.
489 λndby1,ndby2:byte8.λirqfl,ndbo1,ndbo2,ndbo3,ndbo4,ndbo5:bool.
490 let build ≝ λspm,spf,pcm.
491 let fetched_pc ≝ mk_word16 (mem_read_abs t mem (and_w16 pc_reset_h pcm))
492 (mem_read_abs t mem (and_w16 pc_reset_l pcm)) in
495 (* acc_low: ? *) ndby1 (* indx_low: ? *) ndby2
496 (* sp: reset *) (or_w16 (and_w16 sp_reset spm) spf) spm spf
497 (* pc: reset+fetch *) (and_w16 fetched_pc pcm) pcm
498 (* H: ? *) ndbo1 (* I: reset *) true (* N: ? *) ndbo2
499 (* Z: ? *) ndbo3 (* C: ? *) ndbo4 (* IRQ: ? *) irqfl)
502 (* clk: reset *) (None ?) in
504 [ MC68HC05J5A ⇒ build 〈〈x0,x0〉:〈x3,xF〉〉 〈〈x0,x0〉:〈xC,x0〉〉 〈〈x0,xF〉:〈xF,xF〉〉
508 (* HC08: parzialmente non deterministico *)
509 | FamilyHC08 m ⇒ λmem:aux_mem_type t.λchk:aux_chk_type t.
510 λndby1,ndby2:byte8.λirqfl,ndbo1,ndbo2,ndbo3,ndbo4,ndbo5:bool.
512 let fetched_pc ≝ mk_word16 (mem_read_abs t mem pc_reset_h)
513 (mem_read_abs t mem pc_reset_l) in
516 (* acc_low: ? *) ndby1 (* indw_low: ? *) ndby2 (* indx_high: reset *) 〈x0,x0〉
517 (* sp: reset *) sp_reset (* pc: reset+fetch *) fetched_pc
518 (* V: ? *) ndbo1 (* H: ? *) ndbo2 (* I: reset *) true
519 (* N: ? *) ndbo3 (* Z: ? *) ndbo4 (* C: ? *) ndbo5 (* IRQ: ? *) irqfl)
522 (* clk: reset *) (None ?) in
523 (* tralascio l'enumerazione dei casi, tanto non ci sono maschere da impostare *)
526 (* HCS08: parzialmente non deterministico *)
527 | FamilyHCS08 m ⇒ λmem:aux_mem_type t.λchk:aux_chk_type t.
528 λndby1,ndby2:byte8.λirqfl,ndbo1,ndbo2,ndbo3,ndbo4,ndbo5:bool.
530 let fetched_pc ≝ mk_word16 (mem_read_abs t mem pc_reset_h)
531 (mem_read_abs t mem pc_reset_l) in
532 mk_any_status HCS08 t
534 (* acc_low: ? *) ndby1 (* indw_low: ? *) ndby2 (* indx_high: reset *) 〈x0,x0〉
535 (* sp: reset *) sp_reset (* pc: reset+fetch *) fetched_pc
536 (* V: ? *) ndbo1 (* H: ? *) ndbo2 (* I: reset *) true
537 (* N: ? *) ndbo3 (* Z: ? *) ndbo4 (* C: ? *) ndbo5 (* IRQ: ? *) irqfl)
540 (* clk: reset *) (None ?) in
541 (* tralascio l'enumerazione dei casi, tanto non ci sono maschere da impostare *)
544 (* RS08: deterministico *)
545 | FamilyRS08 m ⇒ λmem:aux_mem_type t.λchk:aux_chk_type t.
546 λndby1,ndby2:byte8.λirqfl,ndbo1,ndbo2,ndbo3,ndbo4,ndbo5:bool.
550 (* acc_low: reset *) 〈x0,x0〉
551 (* pc: reset *) (and_w16 pc_RS08_reset pcm) pcm
552 (* spc: reset *) (and_w16 pc_RS08_reset pcm)
553 (* xm: reset *) 〈x0,x0〉 (* psm: *) 〈x8,x0〉
554 (* Z: reset *) false (* C: reset *) false)
557 (* clk: reset *) (None ?) in
558 (* tralascio l'enumerazione dei casi, tanto i valori sono uguali *)
559 build 〈〈x3,xF〉:〈xF,xF〉〉
563 cio' che non viene resettato mantiene il valore precedente: nella documentazione
564 viene riportato come "unaffected"/"indeterminate"/"unpredictable"
565 il soft RESET e' diverso da un calo di tensione e la ram non variera'
567 definition reset_of_mcu ≝
568 λm:mcu_type.λt:memory_impl.
569 let pc_reset_h ≝ 〈〈xF,xF〉:〈xF,xE〉〉 in
570 let pc_reset_l ≝ 〈〈xF,xF〉:〈xF,xF〉〉 in
571 let pc_RS08_reset ≝ 〈〈xF,xF〉:〈xF,xD〉〉 in
572 let sp_reset ≝ 〈〈x0,x0〉:〈xF,xF〉〉 in
573 match m return λm:mcu_type.(any_status m t) → (any_status m t) with
574 (* HC05: parzialmente non deterministico *)
575 [ HC05 ⇒ λs:any_status HC05 t.match s with
576 [ mk_any_status alu mem chk clk ⇒ match alu with
577 [ mk_alu_HC05 acclow indxlow _ spm spf _ pcm hfl _ nfl zfl cfl irqfl ⇒
578 let fetched_pc ≝ mk_word16 (mem_read_abs t mem (and_w16 pc_reset_h pcm))
579 (mem_read_abs t mem (and_w16 pc_reset_l pcm)) in
582 (* acc_low: inv. *) acclow (* indx_low: inv. *) indxlow
583 (* sp: reset *) (or_w16 (and_w16 sp_reset spm) spf) spm spf
584 (* pc: reset+fetch *) (and_w16 fetched_pc pcm) pcm
585 (* H: inv. *) hfl (* I: reset *) true (* N: inv. *) nfl
586 (* Z: inv. *) zfl (* C: inv. *) cfl (* IRQ: inv *) irqfl)
589 (* clk: reset *) (None ?) ]]
590 (* HC08: parzialmente non deterministico *)
591 | HC08 ⇒ λs:any_status HC08 t.match s with
592 [ mk_any_status alu mem chk clk ⇒ match alu with
593 [ mk_alu_HC08 acclow indxlow _ _ _ vfl hfl _ nfl zfl cfl irqfl ⇒
594 let fetched_pc ≝ mk_word16 (mem_read_abs t mem pc_reset_h)
595 (mem_read_abs t mem pc_reset_l) in
598 (* acc_low: inv. *) acclow (* indx_low: inv. *) indxlow (* indx_high: reset *) 〈x0,x0〉
599 (* sp: reset *) sp_reset (* pc: reset+fetch *) fetched_pc
600 (* V: inv. *) vfl (* H: inv. *) hfl (* I: reset *) true
601 (* N: inv. *) nfl (* Z: inv. *) zfl (* C: inv. *) cfl (* IRQ: inv *) irqfl)
604 (* clk: reset *) (None ?) ]]
605 (* HCS08: parzialmente non deterministico *)
606 | HCS08 ⇒ λs:any_status HCS08 t.match s with
607 [ mk_any_status alu mem chk clk ⇒ match alu with
608 [ mk_alu_HC08 acclow indxlow _ _ _ vfl hfl _ nfl zfl cfl irqfl ⇒
609 let fetched_pc ≝ mk_word16 (mem_read_abs t mem pc_reset_h)
610 (mem_read_abs t mem pc_reset_l) in
611 mk_any_status HCS08 t
613 (* acc_low: inv. *) acclow (* indx_low: inv. *) indxlow (* indx_high: reset *) 〈x0,x0〉
614 (* sp: reset *) sp_reset (* pc: reset+fetch *) fetched_pc
615 (* V: inv. *) vfl (* H: inv. *) hfl (* I: reset *) true
616 (* N: inv. *) nfl (* Z: inv. *) zfl (* C: inv. *) cfl (* IRQ: inv *) irqfl)
619 (* clk: reset *) (None ?) ]]
620 (* RS08: deterministico *)
621 | RS08 ⇒ λs:any_status RS08 t.match s with
622 [ mk_any_status alu mem chk clk ⇒ match alu with
623 [ mk_alu_RS08 _ _ pcm _ _ _ _ _ ⇒
626 (* acc_low: reset *) 〈x0,x0〉
627 (* pc: reset *) (and_w16 pc_RS08_reset pcm) pcm
628 (* spc: reset *) (and_w16 pc_RS08_reset pcm)
629 (* xm: reset *) 〈x0,x0〉 (* psm: reset *) 〈x8,x0〉
630 (* Z: reset *) false (* C: reset *) false)
633 (* clk: reset *) (None ?) ]]