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