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/memory_abs.ma".
29 (* *********************************** *)
30 (* STATUS INTERNO DEL PROCESSORE (ALU) *)
31 (* *********************************** *)
34 record alu_HC05: Type ≝
36 (* A: registo accumulatore *)
37 acc_low_reg_HC05 : byte8;
38 (* X: registro indice *)
39 indX_low_reg_HC05 : byte8;
40 (* SP: registo stack pointer *)
42 (* modificatori di SP: per esempio e' definito come 0000000011xxxxxxb *)
43 (* la logica della sua costruzione e' quindi (SP∧mask)∨fix *)
44 (* totalmente racchiusa nella ALU, bastera' fare get(set(SP)) *)
45 sp_mask_HC05 : word16;
47 (* PC: registro program counter *)
49 (* modificatore di PC: per esempio e' definito come 00xxxxxxxxxxxxxxb *)
50 (* la logica della sua costruzione e' quindi (PC∧mask) *)
51 (* totalmente racchiusa nella ALU, bastera' fare get(set(PC)) *)
52 pc_mask_HC05 : word16;
54 (* H: flag semi-carry (somma nibble basso) *)
56 (* I: flag mascheramento degli interrupt mascherabili: 1=mascherati *)
58 (* N: flag segno/negativita' *)
65 (* IRQ: flag che simula il pin esterno IRQ *)
69 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)}"
70 non associative with precedence 80 for
71 @{ 'mk_alu_HC05 $acclow $indxlow $sp $spm $spf $pc $pcm $hfl $ifl $nfl $zfl $cfl $irqfl }.
72 interpretation "mk_alu_HC05" 'mk_alu_HC05 acclow indxlow sp spm spf pc pcm hfl ifl nfl zfl cfl irqfl =
73 (cic:/matita/freescale/status/alu_HC05.ind#xpointer(1/1/1) acclow indxlow sp spm spf pc pcm hfl ifl nfl zfl cfl irqfl).
75 (* ALU dell'HC08/HCS08 *)
76 record alu_HC08: Type ≝
78 (* A: registo accumulatore *)
79 acc_low_reg_HC08 : byte8;
80 (* X: registro indice parte bassa *)
81 indX_low_reg_HC08 : byte8;
82 (* H: registro indice parte alta *)
83 indX_high_reg_HC08 : byte8;
84 (* SP: registo stack pointer *)
86 (* PC: registro program counter *)
89 (* V: flag overflow *)
91 (* H: flag semi-carry (somma nibble basso) *)
93 (* I: flag mascheramento degli interrupt mascherabili: 1=mascherati *)
95 (* N: flag segno/negativita' *)
102 (* IRQ: flag che simula il pin esterno IRQ *)
106 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)}"
107 non associative with precedence 80 for
108 @{ 'mk_alu_HC08 $acclow $indxlow $indxhigh $sp $pc $vfl $hfl $ifl $nfl $zfl $cfl $irqfl }.
109 interpretation "mk_alu_HC08" 'mk_alu_HC08 acclow indxlow indxhigh sp pc vfl hfl ifl nfl zfl cfl irqfl =
110 (cic:/matita/freescale/status/alu_HC08.ind#xpointer(1/1/1) acclow indxlow indxhigh sp pc vfl hfl ifl nfl zfl cfl irqfl).
113 record alu_RS08: Type ≝
115 (* A: registo accumulatore *)
116 acc_low_reg_RS08 : byte8;
117 (* PC: registro program counter *)
118 pc_reg_RS08 : word16;
119 (* modificatore di PC: per esempio e' definito come 00xxxxxxxxxxxxxxb *)
120 (* la logica della sua costruzione e' quindi (PC∧mask) *)
121 (* totalmente racchiusa nella ALU, bastera' fare get(set(PC)) *)
122 pc_mask_RS08 : word16;
123 (* SPC: registro shadow program counter *)
124 (* NB: il suo modificatore e' lo stesso di PC *)
125 spc_reg_RS08 : word16;
127 (* X: registro indice parte bassa *)
128 (* NB: in realta' e' mappato in memoria e non risiede nella ALU *)
129 (* la lettura/scrittura avviene tramite la locazione [0x000F] *)
130 (* la funzione memory_filter_read/write si occupera' di intercettare *)
131 (* e deviare sul registro le letture/scritture (modulo load_write) *)
133 (* PS: registro selezione di pagina *)
134 (* serve a indirizzare la finestra RAM di 64b [0x00C0-0x00FF] *)
135 (* su tutta la memoria installata [0x0000-0x3FFF]: [00pp pppp ppxx xxxx] *)
136 (* NB: in realta' e' mappato in memoria e non risiede nella ALU *)
137 (* la lettura/scrittura avviene tramite la locazione [0x001F] *)
138 (* la funzione memory_filter_read/write si occupera' di intercettare *)
139 (* e deviare sul registro le letture/scritture (modulo load_write) *)
148 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)}"
149 non associative with precedence 80 for
150 @{ 'mk_alu_RS08 $acclow $pc $pcm $spc $xm $psm $zfl $cfl }.
151 interpretation "mk_alu_RS08" 'mk_alu_RS08 acclow pc pcm spc xm psm zfl cfl =
152 (cic:/matita/freescale/status/alu_RS08.ind#xpointer(1/1/1) acclow pc pcm spc xm psm zfl cfl).
154 (* tipo processore dipendente dalla mcu, varia solo la ALU *)
155 record any_status (mcu:mcu_type) (t:memory_impl): Type ≝
158 [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ];
160 (* descritore della memoria *)
161 mem_desc : aux_mem_type t;
162 (* descrittore del tipo di memoria installata *)
163 chk_desc : aux_chk_type t;
164 (* descrittore del click = stato di avanzamento dell'esecuzione+cur_pc conseguente a fetch *)
165 (* 1) None = istruzione eseguita, attesa del fetch *)
166 (* 2) Some cur_clk,pseudo,mode,clks,cur_pc = fetch eseguito, countup a esecuzione *)
167 clk_desc : option (Prod5T byte8 (any_opcode mcu) (instr_mode) byte8 word16)
170 (* evitare di mostrare la memoria/descrittore che impalla il visualizzatore *)
171 notation > "{hvbox('Alu' ≝ alu ; break 'Clk' ≝ clk)}" non associative with precedence 80
172 for @{ 'mk_any_status $alu $mem $chk $clk }.
173 interpretation "mk_any_status" 'mk_any_status alu mem chk clk =
174 (cic:/matita/freescale/status/any_status.ind#xpointer(1/1/1) alu mem chk clk).
176 (* **************** *)
177 (* GETTER SPECIFICI *)
178 (* **************** *)
180 (* funzione ausiliaria per il tipaggio dei getter *)
181 definition aux_get_typing ≝ λx:Type.λm:mcu_type.match m with
182 [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ] → x.
186 (* getter di A, esiste sempre *)
187 definition get_acc_8_low_reg ≝
188 λm:mcu_type.λt:memory_impl.λs:any_status m t.
190 return aux_get_typing byte8 with
191 [ HC05 ⇒ acc_low_reg_HC05
192 | HC08 ⇒ acc_low_reg_HC08
193 | HCS08 ⇒ acc_low_reg_HC08
194 | RS08 ⇒ acc_low_reg_RS08 ]
197 (* getter di X, non esiste sempre *)
198 definition get_indX_8_low_reg ≝
199 λm:mcu_type.λt:memory_impl.λs:any_status m t.
201 return aux_get_typing (option byte8) with
202 [ HC05 ⇒ λalu.Some ? (indX_low_reg_HC05 alu)
203 | HC08 ⇒ λalu.Some ? (indX_low_reg_HC08 alu)
204 | HCS08 ⇒ λalu.Some ? (indX_low_reg_HC08 alu)
205 | RS08 ⇒ λalu.None ? ]
208 (* getter di H, non esiste sempre *)
209 definition get_indX_8_high_reg ≝
210 λm:mcu_type.λt:memory_impl.λs:any_status m t.
212 return aux_get_typing (option byte8) with
214 | HC08 ⇒ λalu.Some ? (indX_high_reg_HC08 alu)
215 | HCS08 ⇒ λalu.Some ? (indX_high_reg_HC08 alu)
216 | RS08 ⇒ λalu.None ? ]
219 (* getter di H:X, non esiste sempre *)
220 definition get_indX_16_reg ≝
221 λm:mcu_type.λt:memory_impl.λs:any_status m t.
223 return aux_get_typing (option word16) with
225 | HC08 ⇒ λalu.Some ? (mk_word16 (indX_high_reg_HC08 alu) (indX_low_reg_HC08 alu))
226 | HCS08 ⇒ λalu.Some ? (mk_word16 (indX_high_reg_HC08 alu) (indX_low_reg_HC08 alu))
227 | RS08 ⇒ λalu.None ? ]
230 (* getter di SP, non esiste sempre *)
231 definition get_sp_reg ≝
232 λm:mcu_type.λt:memory_impl.λs:any_status m t.
234 return aux_get_typing (option word16) with
235 [ HC05 ⇒ λalu.Some ? (sp_reg_HC05 alu)
236 | HC08 ⇒ λalu.Some ? (sp_reg_HC08 alu)
237 | HCS08 ⇒ λalu.Some ? (sp_reg_HC08 alu)
238 | RS08 ⇒ λalu.None ? ]
241 (* getter di PC, esiste sempre *)
242 definition get_pc_reg ≝
243 λm:mcu_type.λt:memory_impl.λs:any_status m t.
245 return aux_get_typing word16 with
248 | HCS08 ⇒ pc_reg_HC08
249 | RS08 ⇒ pc_reg_RS08 ]
252 (* getter di SPC, non esiste sempre *)
253 definition get_spc_reg ≝
254 λm:mcu_type.λt:memory_impl.λs:any_status m t.
256 return aux_get_typing (option word16) with
259 | HCS08 ⇒ λalu.None ?
260 | RS08 ⇒ λalu.Some ? (spc_reg_RS08 alu) ]
263 (* REGISTRI MEMORY MAPPED *)
265 (* getter di memory mapped X, non esiste sempre *)
266 definition get_x_map ≝
267 λm:mcu_type.λt:memory_impl.λs:any_status m t.
269 return aux_get_typing (option byte8) with
272 | HCS08 ⇒ λalu.None ?
273 | RS08 ⇒ λalu.Some ? (x_map_RS08 alu) ]
276 (* getter di memory mapped PS, non esiste sempre *)
277 definition get_ps_map ≝
278 λm:mcu_type.λt:memory_impl.λs:any_status m t.
280 return aux_get_typing (option byte8) with
283 | HCS08 ⇒ λalu.None ?
284 | RS08 ⇒ λalu.Some ? (ps_map_RS08 alu) ]
289 (* getter di V, non esiste sempre *)
290 definition get_v_flag ≝
291 λm:mcu_type.λt:memory_impl.λs:any_status m t.
293 return aux_get_typing (option bool) with
295 | HC08 ⇒ λalu.Some ? (v_flag_HC08 alu)
296 | HCS08 ⇒ λalu.Some ? (v_flag_HC08 alu)
297 | RS08 ⇒ λalu.None ? ]
300 (* getter di H, non esiste sempre *)
301 definition get_h_flag ≝
302 λm:mcu_type.λt:memory_impl.λs:any_status m t.
304 return aux_get_typing (option bool) with
305 [ HC05 ⇒ λalu.Some ? (h_flag_HC05 alu)
306 | HC08 ⇒ λalu.Some ? (h_flag_HC08 alu)
307 | HCS08 ⇒ λalu.Some ? (h_flag_HC08 alu)
308 | RS08 ⇒ λalu.None ? ]
311 (* getter di I, non esiste sempre *)
312 definition get_i_flag ≝
313 λm:mcu_type.λt:memory_impl.λs:any_status m t.
315 return aux_get_typing (option bool) with
316 [ HC05 ⇒ λalu.Some ? (i_flag_HC05 alu)
317 | HC08 ⇒ λalu.Some ? (i_flag_HC08 alu)
318 | HCS08 ⇒ λalu.Some ? (i_flag_HC08 alu)
319 | RS08 ⇒ λalu.None ? ]
322 (* getter di N, non esiste sempre *)
323 definition get_n_flag ≝
324 λm:mcu_type.λt:memory_impl.λs:any_status m t.
326 return aux_get_typing (option bool) with
327 [ HC05 ⇒ λalu.Some ? (n_flag_HC05 alu)
328 | HC08 ⇒ λalu.Some ? (n_flag_HC08 alu)
329 | HCS08 ⇒ λalu.Some ? (n_flag_HC08 alu)
330 | RS08 ⇒ λalu.None ? ]
333 (* getter di Z, esiste sempre *)
334 definition get_z_flag ≝
335 λm:mcu_type.λt:memory_impl.λs:any_status m t.
337 return aux_get_typing bool with
340 | HCS08 ⇒ z_flag_HC08
341 | RS08 ⇒ z_flag_RS08 ]
344 (* getter di C, esiste sempre *)
345 definition get_c_flag ≝
346 λm:mcu_type.λt:memory_impl.λs:any_status m t.
348 return aux_get_typing bool with
351 | HCS08 ⇒ c_flag_HC08
352 | RS08 ⇒ c_flag_RS08 ]
355 (* getter di IRQ, non esiste sempre *)
356 definition get_irq_flag ≝
357 λm:mcu_type.λt:memory_impl.λs:any_status m t.
359 return aux_get_typing (option bool) with
360 [ HC05 ⇒ λalu.Some ? (irq_flag_HC05 alu)
361 | HC08 ⇒ λalu.Some ? (irq_flag_HC08 alu)
362 | HCS08 ⇒ λalu.Some ? (irq_flag_HC08 alu)
363 | RS08 ⇒ λalu.None ? ]
366 (* DESCRITTORI ESTERNI ALLA ALU *)
368 (* getter della ALU, esiste sempre *)
369 definition get_alu ≝ λm:mcu_type.λt:memory_impl.λs:any_status m t.alu m t s.
371 (* getter della memoria, esiste sempre *)
372 definition get_mem_desc ≝ λm:mcu_type.λt:memory_impl.λs:any_status m t.mem_desc m t s.
374 (* getter del descrittore, esiste sempre *)
375 definition get_chk_desc ≝ λm:mcu_type.λt:memory_impl.λs:any_status m t.chk_desc m t s.
377 (* getter del clik, esiste sempre *)
378 definition get_clk_desc ≝ λm:mcu_type.λt:memory_impl.λs:any_status m t.clk_desc m t s.
380 (* ***************************** *)
381 (* SETTER SPECIFICI FORTI/DEBOLI *)
382 (* ***************************** *)
384 (* funzione ausiliaria per il tipaggio dei setter forti *)
385 definition aux_set_typing ≝ λx:Type.λm:mcu_type.
386 match m with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ]
388 match m with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ].
390 (* funzione ausiliaria per il tipaggio dei setter deboli *)
391 definition aux_set_typing_opt ≝ λx:Type.λm:mcu_type.option
392 (match m with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ]
394 match m with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ]).
396 (* DESCRITTORI ESTERNI ALLA ALU *)
398 (* setter forte della ALU *)
400 λm:mcu_type.λt:memory_impl.λs:any_status m t.λalu'.match s with
401 [ mk_any_status _ mem chk clk ⇒ mk_any_status m t alu' mem chk clk ].
403 (* setter forte della memoria *)
404 definition set_mem_desc ≝
405 λm:mcu_type.λt:memory_impl.λs:any_status m t.λmem':aux_mem_type t.match s with
406 [ mk_any_status alu _ chk clk ⇒ mk_any_status m t alu mem' chk clk ].
408 (* setter forte del descrittore *)
409 definition set_chk_desc ≝
410 λm:mcu_type.λt:memory_impl.λs:any_status m t.λchk':aux_chk_type t.match s with
411 [ mk_any_status alu mem _ clk ⇒ mk_any_status m t alu mem chk' clk ].
413 (* setter forte del clik *)
414 definition set_clk_desc ≝
415 λm:mcu_type.λt:memory_impl.λs:any_status m t.
416 λclk':option (Prod5T byte8 (any_opcode m) (instr_mode) byte8 word16).match s with
417 [ mk_any_status alu mem chk _ ⇒ mk_any_status m t alu mem chk clk' ].
421 (* setter specifico HC05 di A *)
422 definition set_acc_8_low_reg_HC05 ≝
423 λalu.λacclow':byte8.match alu with
424 [ mk_alu_HC05 _ indxlow sp spm spf pc pcm hfl ifl nfl zfl cfl irqfl ⇒
425 mk_alu_HC05 acclow' indxlow sp spm spf pc pcm hfl ifl nfl zfl cfl irqfl ].
427 (* setter specifico HC08/HCS08 di A *)
428 definition set_acc_8_low_reg_HC08 ≝
429 λalu.λacclow':byte8.match alu with
430 [ mk_alu_HC08 _ indxlow indxhigh sp pc vfl hfl ifl nfl zfl cfl irqfl ⇒
431 mk_alu_HC08 acclow' indxlow indxhigh sp pc vfl hfl ifl nfl zfl cfl irqfl ].
433 (* setter specifico RS08 di A *)
434 definition set_acc_8_low_reg_RS08 ≝
435 λalu.λacclow':byte8.match alu with
436 [ mk_alu_RS08 _ pc pcm spc xm psm zfl cfl ⇒
437 mk_alu_RS08 acclow' pc pcm spc xm psm zfl cfl ].
439 (* setter forte di A *)
440 definition set_acc_8_low_reg ≝
441 λm:mcu_type.λt:memory_impl.λs:any_status m t.λacclow':byte8.
443 (match m return aux_set_typing byte8 with
444 [ HC05 ⇒ set_acc_8_low_reg_HC05
445 | HC08 ⇒ set_acc_8_low_reg_HC08
446 | HCS08 ⇒ set_acc_8_low_reg_HC08
447 | RS08 ⇒ set_acc_8_low_reg_RS08
448 ] (alu m t s) acclow').
452 (* setter specifico HC05 di X *)
453 definition set_indX_8_low_reg_HC05 ≝
454 λalu.λindxlow':byte8.match alu with
455 [ mk_alu_HC05 acclow _ sp spm spf pc pcm hfl ifl nfl zfl cfl irqfl ⇒
456 mk_alu_HC05 acclow indxlow' sp spm spf pc pcm hfl ifl nfl zfl cfl irqfl ].
458 (* setter specifico HC08/HCS08 di X *)
459 definition set_indX_8_low_reg_HC08 ≝
460 λalu.λindxlow':byte8.match alu with
461 [ mk_alu_HC08 acclow _ indxhigh sp pc vfl hfl ifl nfl zfl cfl irqfl ⇒
462 mk_alu_HC08 acclow indxlow' indxhigh sp pc vfl hfl ifl nfl zfl cfl irqfl ].
464 (* setter forte di X *)
465 definition set_indX_8_low_reg ≝
466 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindxlow':byte8.
467 opt_map ?? (match m return aux_set_typing_opt byte8 with
468 [ HC05 ⇒ Some ? set_indX_8_low_reg_HC05
469 | HC08 ⇒ Some ? set_indX_8_low_reg_HC08
470 | HCS08 ⇒ Some ? set_indX_8_low_reg_HC08
472 (λf.Some ? (set_alu m t s (f (alu m t s) indxlow'))).
474 (* setter debole di X *)
475 definition setweak_indX_8_low_reg ≝
476 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindxlow':byte8.
477 match set_indX_8_low_reg m t s indxlow' with
478 [ None ⇒ s | Some s' ⇒ s' ].
482 (* setter specifico HC08/HCS08 di H *)
483 definition set_indX_8_high_reg_HC08 ≝
484 λalu.λindxhigh':byte8.match alu with
485 [ mk_alu_HC08 acclow indxlow _ sp pc vfl hfl ifl nfl zfl cfl irqfl ⇒
486 mk_alu_HC08 acclow indxlow indxhigh' sp pc vfl hfl ifl nfl zfl cfl irqfl ].
488 (* setter forte di H *)
489 definition set_indX_8_high_reg ≝
490 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindxhigh':byte8.
491 opt_map ?? (match m return aux_set_typing_opt byte8 with
493 | HC08 ⇒ Some ? set_indX_8_high_reg_HC08
494 | HCS08 ⇒ Some ? set_indX_8_high_reg_HC08
496 (λf.Some ? (set_alu m t s (f (alu m t s) indxhigh'))).
498 (* setter debole di H *)
499 definition setweak_indX_8_high_reg ≝
500 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindxhigh':byte8.
501 match set_indX_8_high_reg m t s indxhigh' with
502 [ None ⇒ s | Some s' ⇒ s' ].
506 (* setter specifico HC08/HCS08 di H:X *)
507 definition set_indX_16_reg_HC08 ≝
508 λalu.λindx16:word16.match alu with
509 [ mk_alu_HC08 acclow _ _ sp pc vfl hfl ifl nfl zfl cfl irqfl ⇒
510 mk_alu_HC08 acclow (w16l indx16) (w16h indx16) sp pc vfl hfl ifl nfl zfl cfl irqfl ].
512 (* setter forte di H:X *)
513 definition set_indX_16_reg ≝
514 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindx16:word16.
515 opt_map ?? (match m return aux_set_typing_opt word16 with
517 | HC08 ⇒ Some ? set_indX_16_reg_HC08
518 | HCS08 ⇒ Some ? set_indX_16_reg_HC08
520 (λf.Some ? (set_alu m t s (f (alu m t s) indx16))).
522 (* setter debole di H:X *)
523 definition setweak_indX_16_reg ≝
524 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindx16:word16.
525 match set_indX_16_reg m t s indx16 with
526 [ None ⇒ s | Some s' ⇒ s' ].
530 (* setter specifico HC05 di SP, effettua (SP∧mask)∨fix *)
531 definition set_sp_reg_HC05 ≝
532 λalu.λsp':word16.match alu with
533 [ mk_alu_HC05 acclow indxlow _ spm spf pc pcm hfl ifl nfl zfl cfl irqfl ⇒
534 mk_alu_HC05 acclow indxlow (or_w16 (and_w16 sp' spm) spf) spm spf pc pcm hfl ifl nfl zfl cfl irqfl ].
536 (* setter specifico HC08/HCS08 di SP *)
537 definition set_sp_reg_HC08 ≝
538 λalu.λsp':word16.match alu with
539 [ mk_alu_HC08 acclow indxlow indxhigh _ pc vfl hfl ifl nfl zfl cfl irqfl ⇒
540 mk_alu_HC08 acclow indxlow indxhigh sp' pc vfl hfl ifl nfl zfl cfl irqfl ].
542 (* setter forte di SP *)
543 definition set_sp_reg ≝
544 λm:mcu_type.λt:memory_impl.λs:any_status m t.λsp':word16.
545 opt_map ?? (match m return aux_set_typing_opt word16 with
546 [ HC05 ⇒ Some ? set_sp_reg_HC05
547 | HC08 ⇒ Some ? set_sp_reg_HC08
548 | HCS08 ⇒ Some ? set_sp_reg_HC08
550 (λf.Some ? (set_alu m t s (f (alu m t s) sp'))).
552 (* setter debole di SP *)
553 definition setweak_sp_reg ≝
554 λm:mcu_type.λt:memory_impl.λs:any_status m t.λsp':word16.
555 match set_sp_reg m t s sp' with
556 [ None ⇒ s | Some s' ⇒ s' ].
560 (* setter specifico HC05 di PC, effettua PC∧mask *)
561 definition set_pc_reg_HC05 ≝
562 λalu.λpc':word16.match alu with
563 [ mk_alu_HC05 acclow indxlow sp spm spf _ pcm hfl ifl nfl zfl cfl irqfl ⇒
564 mk_alu_HC05 acclow indxlow sp spm spf (and_w16 pc' pcm) pcm hfl ifl nfl zfl cfl irqfl ].
566 (* setter specifico HC08/HCS08 di PC *)
567 definition set_pc_reg_HC08 ≝
568 λalu.λpc':word16.match alu with
569 [ mk_alu_HC08 acclow indxlow indxhigh sp _ vfl hfl ifl nfl zfl cfl irqfl ⇒
570 mk_alu_HC08 acclow indxlow indxhigh sp pc' vfl hfl ifl nfl zfl cfl irqfl ].
572 (* setter specifico RS08 di PC, effettua PC∧mask *)
573 definition set_pc_reg_RS08 ≝
574 λalu.λpc':word16.match alu with
575 [ mk_alu_RS08 acclow _ pcm spc xm psm zfl cfl ⇒
576 mk_alu_RS08 acclow (and_w16 pc' pcm) pcm spc xm psm zfl cfl ].
578 (* setter forte di PC *)
579 definition set_pc_reg ≝
580 λm:mcu_type.λt:memory_impl.λs:any_status m t.λpc':word16.
582 (match m return aux_set_typing word16 with
583 [ HC05 ⇒ set_pc_reg_HC05
584 | HC08 ⇒ set_pc_reg_HC08
585 | HCS08 ⇒ set_pc_reg_HC08
586 | RS08 ⇒ set_pc_reg_RS08
591 (* setter specifico RS08 di SPC, effettua SPC∧mask *)
592 definition set_spc_reg_RS08 ≝
593 λalu.λspc':word16.match alu with
594 [ mk_alu_RS08 acclow pc pcm _ xm psm zfl cfl ⇒
595 mk_alu_RS08 acclow pc pcm (and_w16 spc' pcm) xm psm zfl cfl ].
597 (* setter forte di SPC *)
598 definition set_spc_reg ≝
599 λm:mcu_type.λt:memory_impl.λs:any_status m t.λspc':word16.
600 opt_map ?? (match m return aux_set_typing_opt word16 with
604 | RS08 ⇒ Some ? set_spc_reg_RS08 ])
605 (λf.Some ? (set_alu m t s (f (alu m t s) spc'))).
607 (* setter debole di SPC *)
608 definition setweak_spc_reg ≝
609 λm:mcu_type.λt:memory_impl.λs:any_status m t.λspc':word16.
610 match set_spc_reg m t s spc' with
611 [ None ⇒ s | Some s' ⇒ s' ].
613 (* REGISTRO MEMORY MAPPED X *)
615 (* setter specifico RS08 di memory mapped X *)
616 definition set_x_map_RS08 ≝
617 λalu.λxm':byte8.match alu with
618 [ mk_alu_RS08 acclow pc pcm spc _ psm zfl cfl ⇒
619 mk_alu_RS08 acclow pc pcm spc xm' psm zfl cfl ].
621 (* setter forte di memory mapped X *)
622 definition set_x_map ≝
623 λm:mcu_type.λt:memory_impl.λs:any_status m t.λxm':byte8.
624 opt_map ?? (match m return aux_set_typing_opt byte8 with
628 | RS08 ⇒ Some ? set_x_map_RS08 ])
629 (λf.Some ? (set_alu m t s (f (alu m t s) xm'))).
631 (* setter debole di memory mapped X *)
632 definition setweak_x_map ≝
633 λm:mcu_type.λt:memory_impl.λs:any_status m t.λxm':byte8.
634 match set_x_map m t s xm' with
635 [ None ⇒ s | Some s' ⇒ s' ].
637 (* REGISTRO MEMORY MAPPED PS *)
639 (* setter specifico RS08 di memory mapped PS *)
640 definition set_ps_map_RS08 ≝
641 λalu.λpsm':byte8.match alu with
642 [ mk_alu_RS08 acclow pc pcm spc xm _ zfl cfl ⇒
643 mk_alu_RS08 acclow pc pcm spc xm psm' zfl cfl ].
645 (* setter forte di memory mapped PS *)
646 definition set_ps_map ≝
647 λm:mcu_type.λt:memory_impl.λs:any_status m t.λpsm':byte8.
648 opt_map ?? (match m return aux_set_typing_opt byte8 with
652 | RS08 ⇒ Some ? set_ps_map_RS08 ])
653 (λf.Some ? (set_alu m t s (f (alu m t s) psm'))).
655 (* setter debole di memory mapped PS *)
656 definition setweak_ps_map ≝
657 λm:mcu_type.λt:memory_impl.λs:any_status m t.λpsm':byte8.
658 match set_ps_map m t s psm' with
659 [ None ⇒ s | Some s' ⇒ s' ].
663 (* setter specifico HC08/HCS08 di V *)
664 definition set_v_flag_HC08 ≝
665 λalu.λvfl':bool.match alu with
666 [ mk_alu_HC08 acclow indxlow indxhigh sp pc _ hfl ifl nfl zfl cfl irqfl ⇒
667 mk_alu_HC08 acclow indxlow indxhigh sp pc vfl' hfl ifl nfl zfl cfl irqfl ].
669 (* setter forte di V *)
670 definition set_v_flag ≝
671 λm:mcu_type.λt:memory_impl.λs:any_status m t.λvfl':bool.
672 opt_map ?? (match m return aux_set_typing_opt bool with
674 | HC08 ⇒ Some ? set_v_flag_HC08
675 | HCS08 ⇒ Some ? set_v_flag_HC08
677 (λf.Some ? (set_alu m t s (f (alu m t s) vfl'))).
679 (* setter debole di V *)
680 definition setweak_v_flag ≝
681 λm:mcu_type.λt:memory_impl.λs:any_status m t.λvfl':bool.
682 match set_v_flag m t s vfl' with
683 [ None ⇒ s | Some s' ⇒ s' ].
687 (* setter specifico HC05 di H *)
688 definition set_h_flag_HC05 ≝
689 λalu.λhfl':bool.match alu with
690 [ mk_alu_HC05 acclow indxlow sp spm spf pc pcm _ ifl nfl zfl cfl irqfl ⇒
691 mk_alu_HC05 acclow indxlow sp spm spf pc pcm hfl' ifl nfl zfl cfl irqfl ].
693 (* setter specifico HC08/HCS08 di H *)
694 definition set_h_flag_HC08 ≝
695 λalu.λhfl':bool.match alu with
696 [ mk_alu_HC08 acclow indxlow indxhigh sp pc vfl _ ifl nfl zfl cfl irqfl ⇒
697 mk_alu_HC08 acclow indxlow indxhigh sp pc vfl hfl' ifl nfl zfl cfl irqfl ].
699 (* setter forte di H *)
700 definition set_h_flag ≝
701 λm:mcu_type.λt:memory_impl.λs:any_status m t.λhfl':bool.
702 opt_map ?? (match m return aux_set_typing_opt bool with
703 [ HC05 ⇒ Some ? set_h_flag_HC05
704 | HC08 ⇒ Some ? set_h_flag_HC08
705 | HCS08 ⇒ Some ? set_h_flag_HC08
707 (λf.Some ? (set_alu m t s (f (alu m t s) hfl'))).
709 (* setter debole di H *)
710 definition setweak_h_flag ≝
711 λm:mcu_type.λt:memory_impl.λs:any_status m t.λhfl':bool.
712 match set_h_flag m t s hfl' with
713 [ None ⇒ s | Some s' ⇒ s' ].
717 (* setter specifico HC05 di I *)
718 definition set_i_flag_HC05 ≝
719 λalu.λifl':bool.match alu with
720 [ mk_alu_HC05 acclow indxlow sp spm spf pc pcm hfl _ nfl zfl cfl irqfl ⇒
721 mk_alu_HC05 acclow indxlow sp spm spf pc pcm hfl ifl' nfl zfl cfl irqfl ].
723 (* setter specifico HC08/HCS08 di I *)
724 definition set_i_flag_HC08 ≝
725 λalu.λifl':bool.match alu with
726 [ mk_alu_HC08 acclow indxlow indxhigh sp pc vfl hfl _ nfl zfl cfl irqfl ⇒
727 mk_alu_HC08 acclow indxlow indxhigh sp pc vfl hfl ifl' nfl zfl cfl irqfl ].
729 (* setter forte di I *)
730 definition set_i_flag ≝
731 λm:mcu_type.λt:memory_impl.λs:any_status m t.λifl':bool.
732 opt_map ?? (match m return aux_set_typing_opt bool with
733 [ HC05 ⇒ Some ? set_i_flag_HC05
734 | HC08 ⇒ Some ? set_i_flag_HC08
735 | HCS08 ⇒ Some ? set_i_flag_HC08
737 (λf.Some ? (set_alu m t s (f (alu m t s) ifl'))).
739 (* setter debole di I *)
740 definition setweak_i_flag ≝
741 λm:mcu_type.λt:memory_impl.λs:any_status m t.λifl':bool.
742 match set_i_flag m t s ifl' with
743 [ None ⇒ s | Some s' ⇒ s' ].
747 (* setter specifico HC05 di N *)
748 definition set_n_flag_HC05 ≝
749 λalu.λnfl':bool.match alu with
750 [ mk_alu_HC05 acclow indxlow sp spm spf pc pcm hfl ifl _ zfl cfl irqfl ⇒
751 mk_alu_HC05 acclow indxlow sp spm spf pc pcm hfl ifl nfl' zfl cfl irqfl ].
753 (* setter specifico HC08/HCS08 di N *)
754 definition set_n_flag_HC08 ≝
755 λalu.λnfl':bool.match alu with
756 [ mk_alu_HC08 acclow indxlow indxhigh sp pc vfl hfl ifl _ zfl cfl irqfl ⇒
757 mk_alu_HC08 acclow indxlow indxhigh sp pc vfl hfl ifl nfl' zfl cfl irqfl ].
759 (* setter forte di N *)
760 definition set_n_flag ≝
761 λm:mcu_type.λt:memory_impl.λs:any_status m t.λnfl':bool.
762 opt_map ?? (match m return aux_set_typing_opt bool with
763 [ HC05 ⇒ Some ? set_n_flag_HC05
764 | HC08 ⇒ Some ? set_n_flag_HC08
765 | HCS08 ⇒ Some ? set_n_flag_HC08
767 (λf.Some ? (set_alu m t s (f (alu m t s) nfl'))).
769 (* setter debole di N *)
770 definition setweak_n_flag ≝
771 λm:mcu_type.λt:memory_impl.λs:any_status m t.λnfl':bool.
772 match set_n_flag m t s nfl' with
773 [ None ⇒ s | Some s' ⇒ s' ].
777 (* setter specifico HC05 di Z *)
778 definition set_z_flag_HC05 ≝
779 λalu.λzfl':bool.match alu with
780 [ mk_alu_HC05 acclow indxlow sp spm spf pc pcm hfl ifl nfl _ cfl irqfl ⇒
781 mk_alu_HC05 acclow indxlow sp spm spf pc pcm hfl ifl nfl zfl' cfl irqfl ].
783 (* setter specifico HC08/HCS08 di Z *)
784 definition set_z_flag_HC08 ≝
785 λalu.λzfl':bool.match alu with
786 [ mk_alu_HC08 acclow indxlow indxhigh sp pc vfl hfl ifl nfl _ cfl irqfl ⇒
787 mk_alu_HC08 acclow indxlow indxhigh sp pc vfl hfl ifl nfl zfl' cfl irqfl ].
789 (* setter sprcifico RS08 di Z *)
790 definition set_z_flag_RS08 ≝
791 λalu.λzfl':bool.match alu with
792 [ mk_alu_RS08 acclow pc pcm spc xm psm _ cfl ⇒
793 mk_alu_RS08 acclow pc pcm spc xm psm zfl' cfl ].
795 (* setter forte di Z *)
796 definition set_z_flag ≝
797 λm:mcu_type.λt:memory_impl.λs:any_status m t.λzfl':bool.
799 (match m return aux_set_typing bool with
800 [ HC05 ⇒ set_z_flag_HC05
801 | HC08 ⇒ set_z_flag_HC08
802 | HCS08 ⇒ set_z_flag_HC08
803 | RS08 ⇒ set_z_flag_RS08
808 (* setter specifico HC05 di C *)
809 definition set_c_flag_HC05 ≝
810 λalu.λcfl':bool.match alu with
811 [ mk_alu_HC05 acclow indxlow sp spm spf pc pcm hfl ifl nfl zfl _ irqfl ⇒
812 mk_alu_HC05 acclow indxlow sp spm spf pc pcm hfl ifl nfl zfl cfl' irqfl ].
814 (* setter specifico HC08/HCS08 di C *)
815 definition set_c_flag_HC08 ≝
816 λalu.λcfl':bool.match alu with
817 [ mk_alu_HC08 acclow indxlow indxhigh sp pc vfl hfl ifl nfl zfl _ irqfl ⇒
818 mk_alu_HC08 acclow indxlow indxhigh sp pc vfl hfl ifl nfl zfl cfl' irqfl ].
820 (* setter specifico RS08 di C *)
821 definition set_c_flag_RS08 ≝
822 λalu.λcfl':bool.match alu with
823 [ mk_alu_RS08 acclow pc pcm spc xm psm zfl _ ⇒
824 mk_alu_RS08 acclow pc pcm spc xm psm zfl cfl' ].
826 (* setter forte di C *)
827 definition set_c_flag ≝
828 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcfl':bool.
830 (match m return aux_set_typing bool with
831 [ HC05 ⇒ set_c_flag_HC05
832 | HC08 ⇒ set_c_flag_HC08
833 | HCS08 ⇒ set_c_flag_HC08
834 | RS08 ⇒ set_c_flag_RS08
839 (* setter specifico HC05 di IRQ *)
840 definition set_irq_flag_HC05 ≝
841 λalu.λirqfl':bool.match alu with
842 [ mk_alu_HC05 acclow indxlow sp spm spf pc pcm hfl ifl nfl zfl cfl _ ⇒
843 mk_alu_HC05 acclow indxlow sp spm spf pc pcm hfl ifl nfl zfl cfl irqfl' ].
845 (* setter specifico HC08/HCS08 di IRQ *)
846 definition set_irq_flag_HC08 ≝
847 λalu.λirqfl':bool.match alu with
848 [ mk_alu_HC08 acclow indxlow indxhigh sp pc vfl hfl ifl nfl zfl cfl _ ⇒
849 mk_alu_HC08 acclow indxlow indxhigh sp pc vfl hfl ifl nfl zfl cfl irqfl' ].
851 (* setter forte di IRQ *)
852 definition set_irq_flag ≝
853 λm:mcu_type.λt:memory_impl.λs:any_status m t.λirqfl':bool.
854 opt_map ?? (match m return aux_set_typing_opt bool with
855 [ HC05 ⇒ Some ? set_irq_flag_HC05
856 | HC08 ⇒ Some ? set_irq_flag_HC08
857 | HCS08 ⇒ Some ? set_irq_flag_HC08
859 (λf.Some ? (set_alu m t s (f (alu m t s) irqfl'))).
861 (* setter debole di IRQ *)
862 definition setweak_irq_flag ≝
863 λm:mcu_type.λt:memory_impl.λs:any_status m t.λirqfl':bool.
864 match set_irq_flag m t s irqfl' with
865 [ None ⇒ s | Some s' ⇒ s' ].
867 (* ***************** *)
868 (* CONFRONTO FRA ALU *)
869 (* ***************** *)
871 (* confronto registro per registro dell'HC05 *)
872 definition eq_alu_HC05 ≝
875 [ mk_alu_HC05 acclow1 indxlow1 sp1 spm1 spf1 pc1 pcm1 hfl1 ifl1 nfl1 zfl1 cfl1 irqfl1 ⇒
877 [ mk_alu_HC05 acclow2 indxlow2 sp2 spm2 spf2 pc2 pcm2 hfl2 ifl2 nfl2 zfl2 cfl2 irqfl2 ⇒
878 (eq_b8 acclow1 acclow2) ⊗
879 (eq_b8 indxlow1 indxlow2) ⊗
885 (eq_bool hfl1 hfl2) ⊗
886 (eq_bool ifl1 ifl2) ⊗
887 (eq_bool nfl1 nfl2) ⊗
888 (eq_bool zfl1 zfl2) ⊗
889 (eq_bool cfl1 cfl2) ⊗
890 (eq_bool irqfl1 irqfl2) ]].
892 (* confronto registro per registro dell'HC08 *)
893 definition eq_alu_HC08 ≝
896 [ mk_alu_HC08 acclow1 indxlow1 indxhigh1 sp1 pc1 vfl1 hfl1 ifl1 nfl1 zfl1 cfl1 irqfl1 ⇒
898 [ mk_alu_HC08 acclow2 indxlow2 indxhigh2 sp2 pc2 vfl2 hfl2 ifl2 nfl2 zfl2 cfl2 irqfl2 ⇒
899 (eq_b8 acclow1 acclow2) ⊗
900 (eq_b8 indxlow1 indxlow2) ⊗
901 (eq_b8 indxhigh1 indxhigh2) ⊗
904 (eq_bool vfl1 vfl2) ⊗
905 (eq_bool hfl1 hfl2) ⊗
906 (eq_bool ifl1 ifl2) ⊗
907 (eq_bool nfl1 nfl2) ⊗
908 (eq_bool zfl1 zfl2) ⊗
909 (eq_bool cfl1 cfl2) ⊗
910 (eq_bool irqfl1 irqfl2) ]].
912 (* confronto registro per registro dell'RS08 *)
913 definition eq_alu_RS08 ≝
916 [ mk_alu_RS08 acclow1 pc1 pcm1 spc1 xm1 psm1 zfl1 cfl1 ⇒
918 [ mk_alu_RS08 acclow2 pc2 pcm2 spc2 xm2 psm2 zfl2 cfl2 ⇒
919 (eq_b8 acclow1 acclow2) ⊗
925 (eq_bool zfl1 zfl2) ⊗
926 (eq_bool cfl1 cfl2) ]].
928 (* ******************** *)
929 (* CONFRONTO FRA STATUS *)
930 (* ******************** *)
932 (* la lettura da memoria ritorna un option byte8, quindi bisogna poterli confrontare *)
933 definition eq_b8_opt ≝
936 [ None ⇒ match b2 with
937 [ None ⇒ true | Some _ ⇒ false ]
938 | Some b1' ⇒ match b2 with
939 [ None ⇒ false | Some b2' ⇒ eq_b8 b1' b2' ]
942 (* confronto di una regione di memoria [inf,inf+n] *)
943 let rec forall_memory_ranged
945 (chk1:aux_chk_type t) (chk2:aux_chk_type t)
946 (mem1:aux_mem_type t) (mem2:aux_mem_type t)
947 (inf:word16) (n:nat) on n ≝
948 match n return λ_.bool with
949 [ O ⇒ eq_b8_opt (mem_read t mem1 chk1 inf) (mem_read t mem2 chk2 inf)
950 | S n' ⇒ (eq_b8_opt (mem_read t mem1 chk1 (plus_w16nc inf (word16_of_nat n)))
951 (mem_read t mem2 chk2 (plus_w16nc inf (word16_of_nat n)))) ⊗
952 (forall_memory_ranged t chk1 chk2 mem1 mem2 inf n')
955 (* il clk e' option (Prod5T byte8 (any_opcode m) (instr_mode) byte8 word16) *)
957 λm:mcu_type.λc1,c2:option (Prod5T byte8 (any_opcode m) (instr_mode) byte8 word16).
959 [ None ⇒ match c2 with
960 [ None ⇒ true | Some _ ⇒ false ]
961 | Some c1' ⇒ match c2 with
962 [ None ⇒ false | Some c2' ⇒ (eq_b8 (fst5T ????? c1') (fst5T ????? c2')) ⊗
963 (eqop m (snd5T ????? c1') (snd5T ????? c2')) ⊗
964 (eqim (thd5T ????? c1') (thd5T ????? c2')) ⊗
965 (eq_b8 (frth5T ????? c1') (frth5T ????? c2')) ⊗
966 (eq_w16 (ffth5T ????? c1') (ffth5T ????? c2')) ]
969 (* generalizzazione del confronto fra stati *)
970 definition eq_status ≝
971 λm:mcu_type.λt:memory_impl.λs1,s2:any_status m t.λinf:word16.λn:nat.
972 match s1 with [ mk_any_status alu1 mem1 chk1 clk1 ⇒
973 match s2 with [ mk_any_status alu2 mem2 chk2 clk2 ⇒
975 (* 1) confronto della ALU *)
976 (match m return λm:mcu_type.
978 [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ] →
980 [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ] →
982 [ HC05 ⇒ eq_alu_HC05 | HC08 ⇒ eq_alu_HC08 | HCS08 ⇒ eq_alu_HC08 | RS08 ⇒ eq_alu_RS08 ]
985 (* 2) confronto della memoria in [inf,inf+n] *)
986 (forall_memory_ranged t chk1 chk2 mem1 mem2 inf n) ⊗
988 (* 3) confronto del clik *)
992 (* assioma da applicare per l'uguaglianza degli stati *)
993 axiom eq_status_axiom :
994 ∀inf:word16.∀n:nat.∀m:mcu_type.∀t:memory_impl.∀s1,s2:any_status m t.
995 (eq_status m t s1 s2 inf n = true) →