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/status/".
29 (*include "/media/VIRTUOSO/freescale/memory_abs.ma".*)
30 include "freescale/memory_abs.ma".
32 (* *********************************** *)
33 (* STATUS INTERNO DEL PROCESSORE (ALU) *)
34 (* *********************************** *)
37 record alu_HC05: Type ≝
39 (* A: registo accumulatore *)
40 acc_low_reg_HC05 : byte8;
41 (* X: registro indice *)
42 indX_low_reg_HC05 : byte8;
43 (* SP: registo stack pointer *)
45 (* modificatori di SP: per esempio e' definito come 0000000011xxxxxxb *)
46 (* la logica della sua costruzione e' quindi (SP∧mask)∨fix *)
47 (* totalmente racchiusa nella ALU, bastera' fare get(set(SP)) *)
48 sp_mask_HC05 : word16;
50 (* PC: registro program counter *)
52 (* modificatore di PC: per esempio e' definito come 00xxxxxxxxxxxxxxb *)
53 (* la logica della sua costruzione e' quindi (PC∧mask) *)
54 (* totalmente racchiusa nella ALU, bastera' fare get(set(PC)) *)
55 pc_mask_HC05 : word16;
57 (* H: flag semi-carry (somma nibble basso) *)
59 (* I: flag mascheramento degli interrupt mascherabili: 1=mascherati *)
61 (* N: flag segno/negativita' *)
68 (* IRQ: flag che simula il pin esterno IRQ *)
72 notation "{hvbox('A_Reg' ≝ acclow ; break 'X_Reg' ≝ indxlow ; break 'Sp_Reg' ≝ sp ; break 'Sp_Mask' ≝ spm ; break 'Sp_Fix' ≝ spf ; break 'Pc_Reg' ≝ pc ; break 'Pc_Mask' ≝ pcm ; break 'H_Flag' ≝ hfl ; break 'I_Flag' ≝ ifl ; break 'N_Flag' ≝ nfl ; break 'Z_Flag' ≝ zfl ; break 'C_Flag' ≝ cfl ; break 'IRQ_Flag' ≝ irqfl)}"
73 non associative with precedence 80 for
74 @{ 'mk_alu_HC05 $acclow $indxlow $sp $spm $spf $pc $pcm $hfl $ifl $nfl $zfl $cfl $irqfl }.
75 interpretation "mk_alu_HC05" 'mk_alu_HC05 acclow indxlow sp spm spf pc pcm hfl ifl nfl zfl cfl irqfl =
76 (cic:/matita/freescale/status/alu_HC05.ind#xpointer(1/1/1) acclow indxlow sp spm spf pc pcm hfl ifl nfl zfl cfl irqfl).
78 (* ALU dell'HC08/HCS08 *)
79 record alu_HC08: Type ≝
81 (* A: registo accumulatore *)
82 acc_low_reg_HC08 : byte8;
83 (* X: registro indice parte bassa *)
84 indX_low_reg_HC08 : byte8;
85 (* H: registro indice parte alta *)
86 indX_high_reg_HC08 : byte8;
87 (* SP: registo stack pointer *)
89 (* PC: registro program counter *)
92 (* V: flag overflow *)
94 (* H: flag semi-carry (somma nibble basso) *)
96 (* I: flag mascheramento degli interrupt mascherabili: 1=mascherati *)
98 (* N: flag segno/negativita' *)
105 (* IRQ: flag che simula il pin esterno IRQ *)
109 notation "{hvbox('A_Reg' ≝ acclow ; break 'X_Reg' ≝ indxlow ; break 'H_Reg' ≝ indxhigh ; break 'Sp_Reg' ≝ sp ; break 'Pc_Reg' ≝ pc ; break 'V_Flag' ≝ vfl ; break 'H_Flag' ≝ hfl ; break 'I_Flag' ≝ ifl ; break 'N_Flag' ≝ nfl ; break 'Z_Flag' ≝ zfl ; break 'C_Flag' ≝ cfl ; break 'IRQ_Flag' ≝ irqfl)}"
110 non associative with precedence 80 for
111 @{ 'mk_alu_HC08 $acclow $indxlow $indxhigh $sp $pc $vfl $hfl $ifl $nfl $zfl $cfl $irqfl }.
112 interpretation "mk_alu_HC08" 'mk_alu_HC08 acclow indxlow indxhigh sp pc vfl hfl ifl nfl zfl cfl irqfl =
113 (cic:/matita/freescale/status/alu_HC08.ind#xpointer(1/1/1) acclow indxlow indxhigh sp pc vfl hfl ifl nfl zfl cfl irqfl).
116 record alu_RS08: Type ≝
118 (* A: registo accumulatore *)
119 acc_low_reg_RS08 : byte8;
120 (* PC: registro program counter *)
121 pc_reg_RS08 : word16;
122 (* modificatore di PC: per esempio e' definito come 00xxxxxxxxxxxxxxb *)
123 (* la logica della sua costruzione e' quindi (PC∧mask) *)
124 (* totalmente racchiusa nella ALU, bastera' fare get(set(PC)) *)
125 pc_mask_RS08 : word16;
126 (* SPC: registro shadow program counter *)
127 (* NB: il suo modificatore e' lo stesso di PC *)
128 spc_reg_RS08 : word16;
130 (* X: registro indice parte bassa *)
131 (* NB: in realta' e' mappato in memoria e non risiede nella ALU *)
132 (* la lettura/scrittura avviene tramite la locazione [0x000F] *)
133 (* la funzione memory_filter_read/write si occupera' di intercettare *)
134 (* e deviare sul registro le letture/scritture (modulo load_write) *)
136 (* PS: registro selezione di pagina *)
137 (* serve a indirizzare la finestra RAM di 64b [0x00C0-0x00FF] *)
138 (* su tutta la memoria installata [0x0000-0x3FFF]: [00pp pppp ppxx xxxx] *)
139 (* NB: in realta' e' mappato in memoria e non risiede nella ALU *)
140 (* la lettura/scrittura avviene tramite la locazione [0x001F] *)
141 (* la funzione memory_filter_read/write si occupera' di intercettare *)
142 (* e deviare sul registro le letture/scritture (modulo load_write) *)
151 notation "{hvbox('A_Reg' ≝ acclow ; break 'Pc_Reg' ≝ pc ; break 'Pc_Mask' ≝ pcm ; break 'Spc_Reg' ≝ spc ; break 'X_Map' ≝ xm ; break 'Ps_Map' ≝ psm ; break 'Z_Flag' ≝ zfl ; break 'C_Flag' ≝ cfl)}"
152 non associative with precedence 80 for
153 @{ 'mk_alu_RS08 $acclow $pc $pcm $spc $xm $psm $zfl $cfl }.
154 interpretation "mk_alu_RS08" 'mk_alu_RS08 acclow pc pcm spc xm psm zfl cfl =
155 (cic:/matita/freescale/status/alu_RS08.ind#xpointer(1/1/1) acclow pc pcm spc xm psm zfl cfl).
157 (* tipo processore dipendente dalla mcu, varia solo la ALU *)
158 record any_status (mcu:mcu_type) (t:memory_impl): Type ≝
161 [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ];
163 (* descritore della memoria *)
164 mem_desc : aux_mem_type t;
165 (* descrittore del tipo di memoria installata *)
166 chk_desc : aux_chk_type t;
167 (* descrittore del click = stato di avanzamento dell'esecuzione+cur_pc conseguente a fetch *)
168 (* 1) None = istruzione eseguita, attesa del fetch *)
169 (* 2) Some cur_clk,pseudo,mode,clks,cur_pc = fetch eseguito, countup a esecuzione *)
170 clk_desc : option (Prod5T byte8 (any_opcode mcu) (instr_mode) byte8 word16)
173 (* evitare di mostrare la memoria/descrittore che impalla il visualizzatore *)
174 notation > "{hvbox('Alu' ≝ alu ; break 'Clk' ≝ clk)}" non associative with precedence 80
175 for @{ 'mk_any_status $alu $mem $chk $clk }.
176 interpretation "mk_any_status" 'mk_any_status alu mem chk clk =
177 (cic:/matita/freescale/status/any_status.ind#xpointer(1/1/1) alu mem chk clk).
179 (* **************** *)
180 (* GETTER SPECIFICI *)
181 (* **************** *)
183 (* funzione ausiliaria per il tipaggio dei getter *)
184 definition aux_get_typing ≝ λx:Type.λm:mcu_type.match m with
185 [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ] → x.
189 (* getter di A, esiste sempre *)
190 definition get_acc_8_low_reg ≝
191 λm:mcu_type.λt:memory_impl.λs:any_status m t.
193 return aux_get_typing byte8 with
194 [ HC05 ⇒ acc_low_reg_HC05
195 | HC08 ⇒ acc_low_reg_HC08
196 | HCS08 ⇒ acc_low_reg_HC08
197 | RS08 ⇒ acc_low_reg_RS08 ]
200 (* getter di X, non esiste sempre *)
201 definition get_indX_8_low_reg ≝
202 λm:mcu_type.λt:memory_impl.λs:any_status m t.
204 return aux_get_typing (option byte8) with
205 [ HC05 ⇒ λalu.Some ? (indX_low_reg_HC05 alu)
206 | HC08 ⇒ λalu.Some ? (indX_low_reg_HC08 alu)
207 | HCS08 ⇒ λalu.Some ? (indX_low_reg_HC08 alu)
208 | RS08 ⇒ λalu.None ? ]
211 (* getter di H, non esiste sempre *)
212 definition get_indX_8_high_reg ≝
213 λm:mcu_type.λt:memory_impl.λs:any_status m t.
215 return aux_get_typing (option byte8) with
217 | HC08 ⇒ λalu.Some ? (indX_high_reg_HC08 alu)
218 | HCS08 ⇒ λalu.Some ? (indX_high_reg_HC08 alu)
219 | RS08 ⇒ λalu.None ? ]
222 (* getter di H:X, non esiste sempre *)
223 definition get_indX_16_reg ≝
224 λm:mcu_type.λt:memory_impl.λs:any_status m t.
226 return aux_get_typing (option word16) with
228 | HC08 ⇒ λalu.Some ? (mk_word16 (indX_high_reg_HC08 alu) (indX_low_reg_HC08 alu))
229 | HCS08 ⇒ λalu.Some ? (mk_word16 (indX_high_reg_HC08 alu) (indX_low_reg_HC08 alu))
230 | RS08 ⇒ λalu.None ? ]
233 (* getter di SP, non esiste sempre *)
234 definition get_sp_reg ≝
235 λm:mcu_type.λt:memory_impl.λs:any_status m t.
237 return aux_get_typing (option word16) with
238 [ HC05 ⇒ λalu.Some ? (sp_reg_HC05 alu)
239 | HC08 ⇒ λalu.Some ? (sp_reg_HC08 alu)
240 | HCS08 ⇒ λalu.Some ? (sp_reg_HC08 alu)
241 | RS08 ⇒ λalu.None ? ]
244 (* getter di PC, esiste sempre *)
245 definition get_pc_reg ≝
246 λm:mcu_type.λt:memory_impl.λs:any_status m t.
248 return aux_get_typing word16 with
251 | HCS08 ⇒ pc_reg_HC08
252 | RS08 ⇒ pc_reg_RS08 ]
255 (* getter di SPC, non esiste sempre *)
256 definition get_spc_reg ≝
257 λm:mcu_type.λt:memory_impl.λs:any_status m t.
259 return aux_get_typing (option word16) with
262 | HCS08 ⇒ λalu.None ?
263 | RS08 ⇒ λalu.Some ? (spc_reg_RS08 alu) ]
266 (* REGISTRI MEMORY MAPPED *)
268 (* getter di memory mapped X, non esiste sempre *)
269 definition get_x_map ≝
270 λm:mcu_type.λt:memory_impl.λs:any_status m t.
272 return aux_get_typing (option byte8) with
275 | HCS08 ⇒ λalu.None ?
276 | RS08 ⇒ λalu.Some ? (x_map_RS08 alu) ]
279 (* getter di memory mapped PS, non esiste sempre *)
280 definition get_ps_map ≝
281 λm:mcu_type.λt:memory_impl.λs:any_status m t.
283 return aux_get_typing (option byte8) with
286 | HCS08 ⇒ λalu.None ?
287 | RS08 ⇒ λalu.Some ? (ps_map_RS08 alu) ]
292 (* getter di V, non esiste sempre *)
293 definition get_v_flag ≝
294 λm:mcu_type.λt:memory_impl.λs:any_status m t.
296 return aux_get_typing (option bool) with
298 | HC08 ⇒ λalu.Some ? (v_flag_HC08 alu)
299 | HCS08 ⇒ λalu.Some ? (v_flag_HC08 alu)
300 | RS08 ⇒ λalu.None ? ]
303 (* getter di H, non esiste sempre *)
304 definition get_h_flag ≝
305 λm:mcu_type.λt:memory_impl.λs:any_status m t.
307 return aux_get_typing (option bool) with
308 [ HC05 ⇒ λalu.Some ? (h_flag_HC05 alu)
309 | HC08 ⇒ λalu.Some ? (h_flag_HC08 alu)
310 | HCS08 ⇒ λalu.Some ? (h_flag_HC08 alu)
311 | RS08 ⇒ λalu.None ? ]
314 (* getter di I, non esiste sempre *)
315 definition get_i_flag ≝
316 λm:mcu_type.λt:memory_impl.λs:any_status m t.
318 return aux_get_typing (option bool) with
319 [ HC05 ⇒ λalu.Some ? (i_flag_HC05 alu)
320 | HC08 ⇒ λalu.Some ? (i_flag_HC08 alu)
321 | HCS08 ⇒ λalu.Some ? (i_flag_HC08 alu)
322 | RS08 ⇒ λalu.None ? ]
325 (* getter di N, non esiste sempre *)
326 definition get_n_flag ≝
327 λm:mcu_type.λt:memory_impl.λs:any_status m t.
329 return aux_get_typing (option bool) with
330 [ HC05 ⇒ λalu.Some ? (n_flag_HC05 alu)
331 | HC08 ⇒ λalu.Some ? (n_flag_HC08 alu)
332 | HCS08 ⇒ λalu.Some ? (n_flag_HC08 alu)
333 | RS08 ⇒ λalu.None ? ]
336 (* getter di Z, esiste sempre *)
337 definition get_z_flag ≝
338 λm:mcu_type.λt:memory_impl.λs:any_status m t.
340 return aux_get_typing bool with
343 | HCS08 ⇒ z_flag_HC08
344 | RS08 ⇒ z_flag_RS08 ]
347 (* getter di C, esiste sempre *)
348 definition get_c_flag ≝
349 λm:mcu_type.λt:memory_impl.λs:any_status m t.
351 return aux_get_typing bool with
354 | HCS08 ⇒ c_flag_HC08
355 | RS08 ⇒ c_flag_RS08 ]
358 (* getter di IRQ, non esiste sempre *)
359 definition get_irq_flag ≝
360 λm:mcu_type.λt:memory_impl.λs:any_status m t.
362 return aux_get_typing (option bool) with
363 [ HC05 ⇒ λalu.Some ? (irq_flag_HC05 alu)
364 | HC08 ⇒ λalu.Some ? (irq_flag_HC08 alu)
365 | HCS08 ⇒ λalu.Some ? (irq_flag_HC08 alu)
366 | RS08 ⇒ λalu.None ? ]
369 (* DESCRITTORI ESTERNI ALLA ALU *)
371 (* getter della ALU, esiste sempre *)
372 definition get_alu ≝ λm:mcu_type.λt:memory_impl.λs:any_status m t.alu m t s.
374 (* getter della memoria, esiste sempre *)
375 definition get_mem_desc ≝ λm:mcu_type.λt:memory_impl.λs:any_status m t.mem_desc m t s.
377 (* getter del descrittore, esiste sempre *)
378 definition get_chk_desc ≝ λm:mcu_type.λt:memory_impl.λs:any_status m t.chk_desc m t s.
380 (* getter del clik, esiste sempre *)
381 definition get_clk_desc ≝ λm:mcu_type.λt:memory_impl.λs:any_status m t.clk_desc m t s.
383 (* ***************************** *)
384 (* SETTER SPECIFICI FORTI/DEBOLI *)
385 (* ***************************** *)
387 (* funzione ausiliaria per il tipaggio dei setter forti *)
388 definition aux_set_typing ≝ λx:Type.λm:mcu_type.
389 match m with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ]
391 match m with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ].
393 (* funzione ausiliaria per il tipaggio dei setter deboli *)
394 definition aux_set_typing_opt ≝ λx:Type.λm:mcu_type.option
395 (match m with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ]
397 match m with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ]).
399 (* DESCRITTORI ESTERNI ALLA ALU *)
401 (* setter forte della ALU *)
403 λm:mcu_type.λt:memory_impl.λs:any_status m t.λalu'.match s with
404 [ mk_any_status _ mem chk clk ⇒ mk_any_status m t alu' mem chk clk ].
406 (* setter forte della memoria *)
407 definition set_mem_desc ≝
408 λm:mcu_type.λt:memory_impl.λs:any_status m t.λmem':aux_mem_type t.match s with
409 [ mk_any_status alu _ chk clk ⇒ mk_any_status m t alu mem' chk clk ].
411 (* setter forte del descrittore *)
412 definition set_chk_desc ≝
413 λm:mcu_type.λt:memory_impl.λs:any_status m t.λchk':aux_chk_type t.match s with
414 [ mk_any_status alu mem _ clk ⇒ mk_any_status m t alu mem chk' clk ].
416 (* setter forte del clik *)
417 definition set_clk_desc ≝
418 λm:mcu_type.λt:memory_impl.λs:any_status m t.
419 λclk':option (Prod5T byte8 (any_opcode m) (instr_mode) byte8 word16).match s with
420 [ mk_any_status alu mem chk _ ⇒ mk_any_status m t alu mem chk clk' ].
424 (* setter specifico HC05 di A *)
425 definition set_acc_8_low_reg_HC05 ≝
426 λalu.λacclow':byte8.match alu with
427 [ mk_alu_HC05 _ indxlow sp spm spf pc pcm hfl ifl nfl zfl cfl irqfl ⇒
428 mk_alu_HC05 acclow' indxlow sp spm spf pc pcm hfl ifl nfl zfl cfl irqfl ].
430 (* setter specifico HC08/HCS08 di A *)
431 definition set_acc_8_low_reg_HC08 ≝
432 λalu.λacclow':byte8.match alu with
433 [ mk_alu_HC08 _ indxlow indxhigh sp pc vfl hfl ifl nfl zfl cfl irqfl ⇒
434 mk_alu_HC08 acclow' indxlow indxhigh sp pc vfl hfl ifl nfl zfl cfl irqfl ].
436 (* setter specifico RS08 di A *)
437 definition set_acc_8_low_reg_RS08 ≝
438 λalu.λacclow':byte8.match alu with
439 [ mk_alu_RS08 _ pc pcm spc xm psm zfl cfl ⇒
440 mk_alu_RS08 acclow' pc pcm spc xm psm zfl cfl ].
442 (* setter forte di A *)
443 definition set_acc_8_low_reg ≝
444 λm:mcu_type.λt:memory_impl.λs:any_status m t.λacclow':byte8.
446 (match m return aux_set_typing byte8 with
447 [ HC05 ⇒ set_acc_8_low_reg_HC05
448 | HC08 ⇒ set_acc_8_low_reg_HC08
449 | HCS08 ⇒ set_acc_8_low_reg_HC08
450 | RS08 ⇒ set_acc_8_low_reg_RS08
451 ] (alu m t s) acclow').
455 (* setter specifico HC05 di X *)
456 definition set_indX_8_low_reg_HC05 ≝
457 λalu.λindxlow':byte8.match alu with
458 [ mk_alu_HC05 acclow _ sp spm spf pc pcm hfl ifl nfl zfl cfl irqfl ⇒
459 mk_alu_HC05 acclow indxlow' sp spm spf pc pcm hfl ifl nfl zfl cfl irqfl ].
461 (* setter specifico HC08/HCS08 di X *)
462 definition set_indX_8_low_reg_HC08 ≝
463 λalu.λindxlow':byte8.match alu with
464 [ mk_alu_HC08 acclow _ indxhigh sp pc vfl hfl ifl nfl zfl cfl irqfl ⇒
465 mk_alu_HC08 acclow indxlow' indxhigh sp pc vfl hfl ifl nfl zfl cfl irqfl ].
467 (* setter forte di X *)
468 definition set_indX_8_low_reg ≝
469 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindxlow':byte8.
470 opt_map ?? (match m return aux_set_typing_opt byte8 with
471 [ HC05 ⇒ Some ? set_indX_8_low_reg_HC05
472 | HC08 ⇒ Some ? set_indX_8_low_reg_HC08
473 | HCS08 ⇒ Some ? set_indX_8_low_reg_HC08
475 (λf.Some ? (set_alu m t s (f (alu m t s) indxlow'))).
477 (* setter debole di X *)
478 definition setweak_indX_8_low_reg ≝
479 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindxlow':byte8.
480 match set_indX_8_low_reg m t s indxlow' with
481 [ None ⇒ s | Some s' ⇒ s' ].
485 (* setter specifico HC08/HCS08 di H *)
486 definition set_indX_8_high_reg_HC08 ≝
487 λalu.λindxhigh':byte8.match alu with
488 [ mk_alu_HC08 acclow indxlow _ sp pc vfl hfl ifl nfl zfl cfl irqfl ⇒
489 mk_alu_HC08 acclow indxlow indxhigh' sp pc vfl hfl ifl nfl zfl cfl irqfl ].
491 (* setter forte di H *)
492 definition set_indX_8_high_reg ≝
493 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindxhigh':byte8.
494 opt_map ?? (match m return aux_set_typing_opt byte8 with
496 | HC08 ⇒ Some ? set_indX_8_high_reg_HC08
497 | HCS08 ⇒ Some ? set_indX_8_high_reg_HC08
499 (λf.Some ? (set_alu m t s (f (alu m t s) indxhigh'))).
501 (* setter debole di H *)
502 definition setweak_indX_8_high_reg ≝
503 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindxhigh':byte8.
504 match set_indX_8_high_reg m t s indxhigh' with
505 [ None ⇒ s | Some s' ⇒ s' ].
509 (* setter specifico HC08/HCS08 di H:X *)
510 definition set_indX_16_reg_HC08 ≝
511 λalu.λindx16:word16.match alu with
512 [ mk_alu_HC08 acclow _ _ sp pc vfl hfl ifl nfl zfl cfl irqfl ⇒
513 mk_alu_HC08 acclow (w16l indx16) (w16h indx16) sp pc vfl hfl ifl nfl zfl cfl irqfl ].
515 (* setter forte di H:X *)
516 definition set_indX_16_reg ≝
517 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindx16:word16.
518 opt_map ?? (match m return aux_set_typing_opt word16 with
520 | HC08 ⇒ Some ? set_indX_16_reg_HC08
521 | HCS08 ⇒ Some ? set_indX_16_reg_HC08
523 (λf.Some ? (set_alu m t s (f (alu m t s) indx16))).
525 (* setter debole di H:X *)
526 definition setweak_indX_16_reg ≝
527 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindx16:word16.
528 match set_indX_16_reg m t s indx16 with
529 [ None ⇒ s | Some s' ⇒ s' ].
533 (* setter specifico HC05 di SP, effettua (SP∧mask)∨fix *)
534 definition set_sp_reg_HC05 ≝
535 λalu.λsp':word16.match alu with
536 [ mk_alu_HC05 acclow indxlow _ spm spf pc pcm hfl ifl nfl zfl cfl irqfl ⇒
537 mk_alu_HC05 acclow indxlow (or_w16 (and_w16 sp' spm) spf) spm spf pc pcm hfl ifl nfl zfl cfl irqfl ].
539 (* setter specifico HC08/HCS08 di SP *)
540 definition set_sp_reg_HC08 ≝
541 λalu.λsp':word16.match alu with
542 [ mk_alu_HC08 acclow indxlow indxhigh _ pc vfl hfl ifl nfl zfl cfl irqfl ⇒
543 mk_alu_HC08 acclow indxlow indxhigh sp' pc vfl hfl ifl nfl zfl cfl irqfl ].
545 (* setter forte di SP *)
546 definition set_sp_reg ≝
547 λm:mcu_type.λt:memory_impl.λs:any_status m t.λsp':word16.
548 opt_map ?? (match m return aux_set_typing_opt word16 with
549 [ HC05 ⇒ Some ? set_sp_reg_HC05
550 | HC08 ⇒ Some ? set_sp_reg_HC08
551 | HCS08 ⇒ Some ? set_sp_reg_HC08
553 (λf.Some ? (set_alu m t s (f (alu m t s) sp'))).
555 (* setter debole di SP *)
556 definition setweak_sp_reg ≝
557 λm:mcu_type.λt:memory_impl.λs:any_status m t.λsp':word16.
558 match set_sp_reg m t s sp' with
559 [ None ⇒ s | Some s' ⇒ s' ].
563 (* setter specifico HC05 di PC, effettua PC∧mask *)
564 definition set_pc_reg_HC05 ≝
565 λalu.λpc':word16.match alu with
566 [ mk_alu_HC05 acclow indxlow sp spm spf _ pcm hfl ifl nfl zfl cfl irqfl ⇒
567 mk_alu_HC05 acclow indxlow sp spm spf (and_w16 pc' pcm) pcm hfl ifl nfl zfl cfl irqfl ].
569 (* setter specifico HC08/HCS08 di PC *)
570 definition set_pc_reg_HC08 ≝
571 λalu.λpc':word16.match alu with
572 [ mk_alu_HC08 acclow indxlow indxhigh sp _ vfl hfl ifl nfl zfl cfl irqfl ⇒
573 mk_alu_HC08 acclow indxlow indxhigh sp pc' vfl hfl ifl nfl zfl cfl irqfl ].
575 (* setter specifico RS08 di PC, effettua PC∧mask *)
576 definition set_pc_reg_RS08 ≝
577 λalu.λpc':word16.match alu with
578 [ mk_alu_RS08 acclow _ pcm spc xm psm zfl cfl ⇒
579 mk_alu_RS08 acclow (and_w16 pc' pcm) pcm spc xm psm zfl cfl ].
581 (* setter forte di PC *)
582 definition set_pc_reg ≝
583 λm:mcu_type.λt:memory_impl.λs:any_status m t.λpc':word16.
585 (match m return aux_set_typing word16 with
586 [ HC05 ⇒ set_pc_reg_HC05
587 | HC08 ⇒ set_pc_reg_HC08
588 | HCS08 ⇒ set_pc_reg_HC08
589 | RS08 ⇒ set_pc_reg_RS08
594 (* setter specifico RS08 di SPC, effettua SPC∧mask *)
595 definition set_spc_reg_RS08 ≝
596 λalu.λspc':word16.match alu with
597 [ mk_alu_RS08 acclow pc pcm _ xm psm zfl cfl ⇒
598 mk_alu_RS08 acclow pc pcm (and_w16 spc' pcm) xm psm zfl cfl ].
600 (* setter forte di SPC *)
601 definition set_spc_reg ≝
602 λm:mcu_type.λt:memory_impl.λs:any_status m t.λspc':word16.
603 opt_map ?? (match m return aux_set_typing_opt word16 with
607 | RS08 ⇒ Some ? set_spc_reg_RS08 ])
608 (λf.Some ? (set_alu m t s (f (alu m t s) spc'))).
610 (* setter debole di SPC *)
611 definition setweak_spc_reg ≝
612 λm:mcu_type.λt:memory_impl.λs:any_status m t.λspc':word16.
613 match set_spc_reg m t s spc' with
614 [ None ⇒ s | Some s' ⇒ s' ].
616 (* REGISTRO MEMORY MAPPED X *)
618 (* setter specifico RS08 di memory mapped X *)
619 definition set_x_map_RS08 ≝
620 λalu.λxm':byte8.match alu with
621 [ mk_alu_RS08 acclow pc pcm spc _ psm zfl cfl ⇒
622 mk_alu_RS08 acclow pc pcm spc xm' psm zfl cfl ].
624 (* setter forte di memory mapped X *)
625 definition set_x_map ≝
626 λm:mcu_type.λt:memory_impl.λs:any_status m t.λxm':byte8.
627 opt_map ?? (match m return aux_set_typing_opt byte8 with
631 | RS08 ⇒ Some ? set_x_map_RS08 ])
632 (λf.Some ? (set_alu m t s (f (alu m t s) xm'))).
634 (* setter debole di memory mapped X *)
635 definition setweak_x_map ≝
636 λm:mcu_type.λt:memory_impl.λs:any_status m t.λxm':byte8.
637 match set_x_map m t s xm' with
638 [ None ⇒ s | Some s' ⇒ s' ].
640 (* REGISTRO MEMORY MAPPED PS *)
642 (* setter specifico RS08 di memory mapped PS *)
643 definition set_ps_map_RS08 ≝
644 λalu.λpsm':byte8.match alu with
645 [ mk_alu_RS08 acclow pc pcm spc xm _ zfl cfl ⇒
646 mk_alu_RS08 acclow pc pcm spc xm psm' zfl cfl ].
648 (* setter forte di memory mapped PS *)
649 definition set_ps_map ≝
650 λm:mcu_type.λt:memory_impl.λs:any_status m t.λpsm':byte8.
651 opt_map ?? (match m return aux_set_typing_opt byte8 with
655 | RS08 ⇒ Some ? set_ps_map_RS08 ])
656 (λf.Some ? (set_alu m t s (f (alu m t s) psm'))).
658 (* setter debole di memory mapped PS *)
659 definition setweak_ps_map ≝
660 λm:mcu_type.λt:memory_impl.λs:any_status m t.λpsm':byte8.
661 match set_ps_map m t s psm' with
662 [ None ⇒ s | Some s' ⇒ s' ].
666 (* setter specifico HC08/HCS08 di V *)
667 definition set_v_flag_HC08 ≝
668 λalu.λvfl':bool.match alu with
669 [ mk_alu_HC08 acclow indxlow indxhigh sp pc _ hfl ifl nfl zfl cfl irqfl ⇒
670 mk_alu_HC08 acclow indxlow indxhigh sp pc vfl' hfl ifl nfl zfl cfl irqfl ].
672 (* setter forte di V *)
673 definition set_v_flag ≝
674 λm:mcu_type.λt:memory_impl.λs:any_status m t.λvfl':bool.
675 opt_map ?? (match m return aux_set_typing_opt bool with
677 | HC08 ⇒ Some ? set_v_flag_HC08
678 | HCS08 ⇒ Some ? set_v_flag_HC08
680 (λf.Some ? (set_alu m t s (f (alu m t s) vfl'))).
682 (* setter debole di V *)
683 definition setweak_v_flag ≝
684 λm:mcu_type.λt:memory_impl.λs:any_status m t.λvfl':bool.
685 match set_v_flag m t s vfl' with
686 [ None ⇒ s | Some s' ⇒ s' ].
690 (* setter specifico HC05 di H *)
691 definition set_h_flag_HC05 ≝
692 λalu.λhfl':bool.match alu with
693 [ mk_alu_HC05 acclow indxlow sp spm spf pc pcm _ ifl nfl zfl cfl irqfl ⇒
694 mk_alu_HC05 acclow indxlow sp spm spf pc pcm hfl' ifl nfl zfl cfl irqfl ].
696 (* setter specifico HC08/HCS08 di H *)
697 definition set_h_flag_HC08 ≝
698 λalu.λhfl':bool.match alu with
699 [ mk_alu_HC08 acclow indxlow indxhigh sp pc vfl _ ifl nfl zfl cfl irqfl ⇒
700 mk_alu_HC08 acclow indxlow indxhigh sp pc vfl hfl' ifl nfl zfl cfl irqfl ].
702 (* setter forte di H *)
703 definition set_h_flag ≝
704 λm:mcu_type.λt:memory_impl.λs:any_status m t.λhfl':bool.
705 opt_map ?? (match m return aux_set_typing_opt bool with
706 [ HC05 ⇒ Some ? set_h_flag_HC05
707 | HC08 ⇒ Some ? set_h_flag_HC08
708 | HCS08 ⇒ Some ? set_h_flag_HC08
710 (λf.Some ? (set_alu m t s (f (alu m t s) hfl'))).
712 (* setter debole di H *)
713 definition setweak_h_flag ≝
714 λm:mcu_type.λt:memory_impl.λs:any_status m t.λhfl':bool.
715 match set_h_flag m t s hfl' with
716 [ None ⇒ s | Some s' ⇒ s' ].
720 (* setter specifico HC05 di I *)
721 definition set_i_flag_HC05 ≝
722 λalu.λifl':bool.match alu with
723 [ mk_alu_HC05 acclow indxlow sp spm spf pc pcm hfl _ nfl zfl cfl irqfl ⇒
724 mk_alu_HC05 acclow indxlow sp spm spf pc pcm hfl ifl' nfl zfl cfl irqfl ].
726 (* setter specifico HC08/HCS08 di I *)
727 definition set_i_flag_HC08 ≝
728 λalu.λifl':bool.match alu with
729 [ mk_alu_HC08 acclow indxlow indxhigh sp pc vfl hfl _ nfl zfl cfl irqfl ⇒
730 mk_alu_HC08 acclow indxlow indxhigh sp pc vfl hfl ifl' nfl zfl cfl irqfl ].
732 (* setter forte di I *)
733 definition set_i_flag ≝
734 λm:mcu_type.λt:memory_impl.λs:any_status m t.λifl':bool.
735 opt_map ?? (match m return aux_set_typing_opt bool with
736 [ HC05 ⇒ Some ? set_i_flag_HC05
737 | HC08 ⇒ Some ? set_i_flag_HC08
738 | HCS08 ⇒ Some ? set_i_flag_HC08
740 (λf.Some ? (set_alu m t s (f (alu m t s) ifl'))).
742 (* setter debole di I *)
743 definition setweak_i_flag ≝
744 λm:mcu_type.λt:memory_impl.λs:any_status m t.λifl':bool.
745 match set_i_flag m t s ifl' with
746 [ None ⇒ s | Some s' ⇒ s' ].
750 (* setter specifico HC05 di N *)
751 definition set_n_flag_HC05 ≝
752 λalu.λnfl':bool.match alu with
753 [ mk_alu_HC05 acclow indxlow sp spm spf pc pcm hfl ifl _ zfl cfl irqfl ⇒
754 mk_alu_HC05 acclow indxlow sp spm spf pc pcm hfl ifl nfl' zfl cfl irqfl ].
756 (* setter specifico HC08/HCS08 di N *)
757 definition set_n_flag_HC08 ≝
758 λalu.λnfl':bool.match alu with
759 [ mk_alu_HC08 acclow indxlow indxhigh sp pc vfl hfl ifl _ zfl cfl irqfl ⇒
760 mk_alu_HC08 acclow indxlow indxhigh sp pc vfl hfl ifl nfl' zfl cfl irqfl ].
762 (* setter forte di N *)
763 definition set_n_flag ≝
764 λm:mcu_type.λt:memory_impl.λs:any_status m t.λnfl':bool.
765 opt_map ?? (match m return aux_set_typing_opt bool with
766 [ HC05 ⇒ Some ? set_n_flag_HC05
767 | HC08 ⇒ Some ? set_n_flag_HC08
768 | HCS08 ⇒ Some ? set_n_flag_HC08
770 (λf.Some ? (set_alu m t s (f (alu m t s) nfl'))).
772 (* setter debole di N *)
773 definition setweak_n_flag ≝
774 λm:mcu_type.λt:memory_impl.λs:any_status m t.λnfl':bool.
775 match set_n_flag m t s nfl' with
776 [ None ⇒ s | Some s' ⇒ s' ].
780 (* setter specifico HC05 di Z *)
781 definition set_z_flag_HC05 ≝
782 λalu.λzfl':bool.match alu with
783 [ mk_alu_HC05 acclow indxlow sp spm spf pc pcm hfl ifl nfl _ cfl irqfl ⇒
784 mk_alu_HC05 acclow indxlow sp spm spf pc pcm hfl ifl nfl zfl' cfl irqfl ].
786 (* setter specifico HC08/HCS08 di Z *)
787 definition set_z_flag_HC08 ≝
788 λalu.λzfl':bool.match alu with
789 [ mk_alu_HC08 acclow indxlow indxhigh sp pc vfl hfl ifl nfl _ cfl irqfl ⇒
790 mk_alu_HC08 acclow indxlow indxhigh sp pc vfl hfl ifl nfl zfl' cfl irqfl ].
792 (* setter sprcifico RS08 di Z *)
793 definition set_z_flag_RS08 ≝
794 λalu.λzfl':bool.match alu with
795 [ mk_alu_RS08 acclow pc pcm spc xm psm _ cfl ⇒
796 mk_alu_RS08 acclow pc pcm spc xm psm zfl' cfl ].
798 (* setter forte di Z *)
799 definition set_z_flag ≝
800 λm:mcu_type.λt:memory_impl.λs:any_status m t.λzfl':bool.
802 (match m return aux_set_typing bool with
803 [ HC05 ⇒ set_z_flag_HC05
804 | HC08 ⇒ set_z_flag_HC08
805 | HCS08 ⇒ set_z_flag_HC08
806 | RS08 ⇒ set_z_flag_RS08
811 (* setter specifico HC05 di C *)
812 definition set_c_flag_HC05 ≝
813 λalu.λcfl':bool.match alu with
814 [ mk_alu_HC05 acclow indxlow sp spm spf pc pcm hfl ifl nfl zfl _ irqfl ⇒
815 mk_alu_HC05 acclow indxlow sp spm spf pc pcm hfl ifl nfl zfl cfl' irqfl ].
817 (* setter specifico HC08/HCS08 di C *)
818 definition set_c_flag_HC08 ≝
819 λalu.λcfl':bool.match alu with
820 [ mk_alu_HC08 acclow indxlow indxhigh sp pc vfl hfl ifl nfl zfl _ irqfl ⇒
821 mk_alu_HC08 acclow indxlow indxhigh sp pc vfl hfl ifl nfl zfl cfl' irqfl ].
823 (* setter specifico RS08 di C *)
824 definition set_c_flag_RS08 ≝
825 λalu.λcfl':bool.match alu with
826 [ mk_alu_RS08 acclow pc pcm spc xm psm zfl _ ⇒
827 mk_alu_RS08 acclow pc pcm spc xm psm zfl cfl' ].
829 (* setter forte di C *)
830 definition set_c_flag ≝
831 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcfl':bool.
833 (match m return aux_set_typing bool with
834 [ HC05 ⇒ set_c_flag_HC05
835 | HC08 ⇒ set_c_flag_HC08
836 | HCS08 ⇒ set_c_flag_HC08
837 | RS08 ⇒ set_c_flag_RS08
842 (* setter specifico HC05 di IRQ *)
843 definition set_irq_flag_HC05 ≝
844 λalu.λirqfl':bool.match alu with
845 [ mk_alu_HC05 acclow indxlow sp spm spf pc pcm hfl ifl nfl zfl cfl _ ⇒
846 mk_alu_HC05 acclow indxlow sp spm spf pc pcm hfl ifl nfl zfl cfl irqfl' ].
848 (* setter specifico HC08/HCS08 di IRQ *)
849 definition set_irq_flag_HC08 ≝
850 λalu.λirqfl':bool.match alu with
851 [ mk_alu_HC08 acclow indxlow indxhigh sp pc vfl hfl ifl nfl zfl cfl _ ⇒
852 mk_alu_HC08 acclow indxlow indxhigh sp pc vfl hfl ifl nfl zfl cfl irqfl' ].
854 (* setter forte di IRQ *)
855 definition set_irq_flag ≝
856 λm:mcu_type.λt:memory_impl.λs:any_status m t.λirqfl':bool.
857 opt_map ?? (match m return aux_set_typing_opt bool with
858 [ HC05 ⇒ Some ? set_irq_flag_HC05
859 | HC08 ⇒ Some ? set_irq_flag_HC08
860 | HCS08 ⇒ Some ? set_irq_flag_HC08
862 (λf.Some ? (set_alu m t s (f (alu m t s) irqfl'))).
864 (* setter debole di IRQ *)
865 definition setweak_irq_flag ≝
866 λm:mcu_type.λt:memory_impl.λs:any_status m t.λirqfl':bool.
867 match set_irq_flag m t s irqfl' with
868 [ None ⇒ s | Some s' ⇒ s' ].
870 (* ***************** *)
871 (* CONFRONTO FRA ALU *)
872 (* ***************** *)
874 (* confronto registro per registro dell'HC05 *)
875 definition eq_alu_HC05 ≝
878 [ mk_alu_HC05 acclow1 indxlow1 sp1 spm1 spf1 pc1 pcm1 hfl1 ifl1 nfl1 zfl1 cfl1 irqfl1 ⇒
880 [ mk_alu_HC05 acclow2 indxlow2 sp2 spm2 spf2 pc2 pcm2 hfl2 ifl2 nfl2 zfl2 cfl2 irqfl2 ⇒
881 (eq_b8 acclow1 acclow2) ⊗
882 (eq_b8 indxlow1 indxlow2) ⊗
888 (eq_bool hfl1 hfl2) ⊗
889 (eq_bool ifl1 ifl2) ⊗
890 (eq_bool nfl1 nfl2) ⊗
891 (eq_bool zfl1 zfl2) ⊗
892 (eq_bool cfl1 cfl2) ⊗
893 (eq_bool irqfl1 irqfl2) ]].
895 (* confronto registro per registro dell'HC08 *)
896 definition eq_alu_HC08 ≝
899 [ mk_alu_HC08 acclow1 indxlow1 indxhigh1 sp1 pc1 vfl1 hfl1 ifl1 nfl1 zfl1 cfl1 irqfl1 ⇒
901 [ mk_alu_HC08 acclow2 indxlow2 indxhigh2 sp2 pc2 vfl2 hfl2 ifl2 nfl2 zfl2 cfl2 irqfl2 ⇒
902 (eq_b8 acclow1 acclow2) ⊗
903 (eq_b8 indxlow1 indxlow2) ⊗
904 (eq_b8 indxhigh1 indxhigh2) ⊗
907 (eq_bool vfl1 vfl2) ⊗
908 (eq_bool hfl1 hfl2) ⊗
909 (eq_bool ifl1 ifl2) ⊗
910 (eq_bool nfl1 nfl2) ⊗
911 (eq_bool zfl1 zfl2) ⊗
912 (eq_bool cfl1 cfl2) ⊗
913 (eq_bool irqfl1 irqfl2) ]].
915 (* confronto registro per registro dell'RS08 *)
916 definition eq_alu_RS08 ≝
919 [ mk_alu_RS08 acclow1 pc1 pcm1 spc1 xm1 psm1 zfl1 cfl1 ⇒
921 [ mk_alu_RS08 acclow2 pc2 pcm2 spc2 xm2 psm2 zfl2 cfl2 ⇒
922 (eq_b8 acclow1 acclow2) ⊗
928 (eq_bool zfl1 zfl2) ⊗
929 (eq_bool cfl1 cfl2) ]].
931 (* ******************** *)
932 (* CONFRONTO FRA STATUS *)
933 (* ******************** *)
935 (* la lettura da memoria ritorna un option byte8, quindi bisogna poterli confrontare *)
936 definition eq_b8_opt ≝
939 [ None ⇒ match b2 with
940 [ None ⇒ true | Some _ ⇒ false ]
941 | Some b1' ⇒ match b2 with
942 [ None ⇒ false | Some b2' ⇒ eq_b8 b1' b2' ]
945 (* confronto di una regione di memoria [inf,inf+n] *)
946 let rec forall_memory_ranged
948 (chk1:aux_chk_type t) (chk2:aux_chk_type t)
949 (mem1:aux_mem_type t) (mem2:aux_mem_type t)
950 (inf:word16) (n:nat) on n ≝
951 match n return λ_.bool with
952 [ O ⇒ eq_b8_opt (mem_read t mem1 chk1 inf) (mem_read t mem2 chk2 inf)
953 | S n' ⇒ (eq_b8_opt (mem_read t mem1 chk1 (plus_w16nc inf (word16_of_nat n)))
954 (mem_read t mem2 chk2 (plus_w16nc inf (word16_of_nat n)))) ⊗
955 (forall_memory_ranged t chk1 chk2 mem1 mem2 inf n')
958 (* il clk e' option (Prod5T byte8 (any_opcode m) (instr_mode) byte8 word16) *)
960 λm:mcu_type.λc1,c2:option (Prod5T byte8 (any_opcode m) (instr_mode) byte8 word16).
962 [ None ⇒ match c2 with
963 [ None ⇒ true | Some _ ⇒ false ]
964 | Some c1' ⇒ match c2 with
965 [ None ⇒ false | Some c2' ⇒ (eq_b8 (fst5T ????? c1') (fst5T ????? c2')) ⊗
966 (eqop m (snd5T ????? c1') (snd5T ????? c2')) ⊗
967 (eqim (thd5T ????? c1') (thd5T ????? c2')) ⊗
968 (eq_b8 (frth5T ????? c1') (frth5T ????? c2')) ⊗
969 (eq_w16 (ffth5T ????? c1') (ffth5T ????? c2')) ]
972 (* generalizzazione del confronto fra stati *)
973 definition eq_status ≝
974 λm:mcu_type.λt:memory_impl.λs1,s2:any_status m t.λinf:word16.λn:nat.
975 match s1 with [ mk_any_status alu1 mem1 chk1 clk1 ⇒
976 match s2 with [ mk_any_status alu2 mem2 chk2 clk2 ⇒
978 (* 1) confronto della ALU *)
979 (match m return λm:mcu_type.
981 [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ] →
983 [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ] →
985 [ HC05 ⇒ eq_alu_HC05 | HC08 ⇒ eq_alu_HC08 | HCS08 ⇒ eq_alu_HC08 | RS08 ⇒ eq_alu_RS08 ]
988 (* 2) confronto della memoria in [inf,inf+n] *)
989 (forall_memory_ranged t chk1 chk2 mem1 mem2 inf n) ⊗
991 (* 3) confronto del clik *)
995 (* assioma da applicare per l'uguaglianza degli stati *)
996 axiom eq_status_axiom :
997 ∀inf:word16.∀n:nat.∀m:mcu_type.∀t:memory_impl.∀s1,s2:any_status m t.
998 (eq_status m t s1 s2 inf n = true) →