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 *)
18 (* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *)
19 (* Cosimo Oliboni, oliboni@cs.unibo.it *)
21 (* ********************************************************************** *)
23 include "freescale/status.ma".
25 (* *********************************** *)
26 (* IMPOSTAZIONI SPECIFICHE DEI MODELLI *)
27 (* *********************************** *)
30 ninductive HC05_mcu_model : Type ≝
31 MC68HC05J5A: HC05_mcu_model
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 ].
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 ].
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 ].
47 ninductive HC08_mcu_model : Type ≝
48 MC68HC08AB16A: HC08_mcu_model
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 ].
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 ].
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 ].
63 (* modelli di HCS08 *)
64 ninductive HCS08_mcu_model : Type ≝
65 MC9S08AW60 : HCS08_mcu_model
66 | MC9S08GB60 : HCS08_mcu_model
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 ].
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 ].
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 ].
82 ninductive RS08_mcu_model : Type ≝
83 MC9RS08KA1 : RS08_mcu_model
84 | MC9RS08KA2 : RS08_mcu_model.
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 ].
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 ].
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 ].
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.
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 ].
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 ].
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 ].
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)
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
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.
154 (* memoria degli HC05 *)
155 ndefinition memory_type_of_FamilyHC05 ≝
156 λm:HC05_mcu_model.match m with
160 (* 0x0000-0x001F,0x0FF0: sarebbe memory mapped IO *)
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 *)
169 (* memoria degli HC08 *)
170 ndefinition memory_type_of_FamilyHC08 ≝
171 λm:HC08_mcu_model.match m with
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 *)
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 *) ]
188 (* memoria degli HCS08 *)
189 ndefinition memory_type_of_FamilyHCS08 ≝
190 λm:HCS08_mcu_model.match m with
194 (* 0x0000-0x006F,0x1800-0x185F: sarebbe memory mapped IO *)
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 *) ]
202 (* 0x0000-0x006F,0x1800-0x185F: sarebbe memory mapped IO *)
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 *) ]
209 (* memoria dei RS08 *)
210 ndefinition memory_type_of_FamilyRS08 ≝
211 λm:RS08_mcu_model.match m with
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 *) ]
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 *) ]
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
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 ≝
254 build_memory_type_of_mcu_version_aux t tl
255 (check_update_ranged t result (fst3T ??? hd) (snd3T ??? hd) (thd3T ??? hd)) ].
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).
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
268 | FamilyHC08 m ⇒ match m with
269 [ MC68HC08AB16A ⇒ zero_memory t
272 (* tralascio l'enumerazione dei casi, per ora e' tutto 0 *)
273 | FamilyHCS08 _ ⇒ zero_memory t
274 | FamilyRS08 _ ⇒ zero_memory t
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)
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
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)
301 (* clk: reset *) (None ?) in
303 [ MC68HC05J5A ⇒ build 〈〈x0,x0〉:〈x3,xF〉〉 〈〈x0,x0〉:〈xC,x0〉〉 〈〈x0,xF〉:〈xF,xF〉〉
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
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)
321 (* clk: reset *) (None ?).
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
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)
337 (* clk: reset *) (None ?).
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.
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)
353 (* clk: reset *) (None ?) in
354 (* tralascio l'enumerazione dei casi, tanto i valori sono uguali *)
355 build 〈〈x3,xF〉:〈xF,xF〉〉.
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'
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
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)
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
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)
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
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)
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 _ _ _ _ _ ⇒
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)
428 (* clk: reset *) (None ?) ]]