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: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
19 (* Ultima modifica: 05/08/2009 *)
21 (* ********************************************************************** *)
23 include "freescale/memory_abs.ma".
24 include "freescale/opcode_base.ma".
26 (* *********************************** *)
27 (* STATUS INTERNO DEL PROCESSORE (ALU) *)
28 (* *********************************** *)
31 nrecord alu_HC05: Type ≝
33 (* A: registo accumulatore *)
34 acc_low_reg_HC05 : byte8;
35 (* X: registro indice *)
36 indX_low_reg_HC05 : byte8;
37 (* SP: registo stack pointer *)
39 (* modificatori di SP: per esempio e' definito come 0000000011xxxxxxb *)
40 (* la logica della sua costruzione e' quindi (SP∧mask)∨fix *)
41 (* totalmente racchiusa nella ALU, bastera' fare get(set(SP)) *)
42 sp_mask_HC05 : word16;
44 (* PC: registro program counter *)
46 (* modificatore di PC: per esempio e' definito come 00xxxxxxxxxxxxxxb *)
47 (* la logica della sua costruzione e' quindi (PC∧mask) *)
48 (* totalmente racchiusa nella ALU, bastera' fare get(set(PC)) *)
49 pc_mask_HC05 : word16;
51 (* H: flag semi-carry (somma nibble basso) *)
53 (* I: flag mascheramento degli interrupt mascherabili: 1=mascherati *)
55 (* N: flag segno/negativita' *)
62 (* IRQ: flag che simula il pin esterno IRQ *)
66 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)}"
67 non associative with precedence 80 for
68 @{ 'mk_alu_HC05 $acclow $indxlow $sp $spm $spf $pc $pcm $hfl $ifl $nfl $zfl $cfl $irqfl }.
69 interpretation "mk_alu_HC05" 'mk_alu_HC05 acclow indxlow sp spm spf pc pcm hfl ifl nfl zfl cfl irqfl =
70 (mk_alu_HC05 acclow indxlow sp spm spf pc pcm hfl ifl nfl zfl cfl irqfl).
72 (* ALU dell'HC08/HCS08 *)
73 nrecord alu_HC08: Type ≝
75 (* A: registo accumulatore *)
76 acc_low_reg_HC08 : byte8;
77 (* X: registro indice parte bassa *)
78 indX_low_reg_HC08 : byte8;
79 (* H: registro indice parte alta *)
80 indX_high_reg_HC08 : byte8;
81 (* SP: registo stack pointer *)
83 (* PC: registro program counter *)
86 (* V: flag overflow *)
88 (* H: flag semi-carry (somma nibble basso) *)
90 (* I: flag mascheramento degli interrupt mascherabili: 1=mascherati *)
92 (* N: flag segno/negativita' *)
99 (* IRQ: flag che simula il pin esterno IRQ *)
103 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)}"
104 non associative with precedence 80 for
105 @{ 'mk_alu_HC08 $acclow $indxlow $indxhigh $sp $pc $vfl $hfl $ifl $nfl $zfl $cfl $irqfl }.
106 interpretation "mk_alu_HC08" 'mk_alu_HC08 acclow indxlow indxhigh sp pc vfl hfl ifl nfl zfl cfl irqfl =
107 (mk_alu_HC08 acclow indxlow indxhigh sp pc vfl hfl ifl nfl zfl cfl irqfl).
110 nrecord alu_RS08: Type ≝
112 (* A: registo accumulatore *)
113 acc_low_reg_RS08 : byte8;
114 (* PC: registro program counter *)
115 pc_reg_RS08 : word16;
116 (* modificatore di PC: per esempio e' definito come 00xxxxxxxxxxxxxxb *)
117 (* la logica della sua costruzione e' quindi (PC∧mask) *)
118 (* totalmente racchiusa nella ALU, bastera' fare get(set(PC)) *)
119 pc_mask_RS08 : word16;
120 (* SPC: registro shadow program counter *)
121 (* NB: il suo modificatore e' lo stesso di PC *)
122 spc_reg_RS08 : word16;
124 (* X: registro indice parte bassa *)
125 (* NB: in realta' e' mappato in memoria e non risiede nella ALU *)
126 (* la lettura/scrittura avviene tramite la locazione [0x000F] *)
127 (* la funzione memory_filter_read/write si occupera' di intercettare *)
128 (* e deviare sul registro le letture/scritture (modulo load_write) *)
130 (* PS: registro selezione di pagina *)
131 (* serve a indirizzare la finestra RAM di 64b [0x00C0-0x00FF] *)
132 (* su tutta la memoria installata [0x0000-0x3FFF]: [00pp pppp ppxx xxxx] *)
133 (* NB: in realta' e' mappato in memoria e non risiede nella ALU *)
134 (* la lettura/scrittura avviene tramite la locazione [0x001F] *)
135 (* la funzione memory_filter_read/write si occupera' di intercettare *)
136 (* e deviare sul registro le letture/scritture (modulo load_write) *)
145 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)}"
146 non associative with precedence 80 for
147 @{ 'mk_alu_RS08 $acclow $pc $pcm $spc $xm $psm $zfl $cfl }.
148 interpretation "mk_alu_RS08" 'mk_alu_RS08 acclow pc pcm spc xm psm zfl cfl =
149 (mk_alu_RS08 acclow pc pcm spc xm psm zfl cfl).
151 (* tipo processore dipendente dalla mcu, varia solo la ALU *)
152 nrecord any_status (mcu:mcu_type) (t:memory_impl): Type ≝
155 [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ];
157 (* descritore della memoria *)
158 mem_desc : aux_mem_type t;
159 (* descrittore del tipo di memoria installata *)
160 chk_desc : aux_chk_type t;
161 (* descrittore del click = stato di avanzamento dell'esecuzione+cur_pc conseguente a fetch *)
162 (* 1) None = istruzione eseguita, attesa del fetch *)
163 (* 2) Some cur_clk,pseudo,mode,clks,cur_pc = fetch eseguito, countup a esecuzione *)
164 clk_desc : option (Prod5T byte8 (any_opcode mcu) (instr_mode) byte8 word16)
167 (* evitare di mostrare la memoria/descrittore che impalla il visualizzatore *)
168 notation > "{hvbox('Alu' ≝ alu ; break 'Clk' ≝ clk)}" non associative with precedence 80
169 for @{ 'mk_any_status $alu $mem $chk $clk }.
170 interpretation "mk_any_status" 'mk_any_status alu mem chk clk =
171 (mk_any_status alu mem chk clk).
173 (* **************** *)
174 (* GETTER SPECIFICI *)
175 (* **************** *)
177 (* funzione ausiliaria per il tipaggio dei getter *)
178 ndefinition aux_get_typing ≝ λx:Type.λm:mcu_type.match m with
179 [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ] → x.
183 (* getter di A, esiste sempre *)
184 ndefinition get_acc_8_low_reg ≝
185 λm:mcu_type.λt:memory_impl.λs:any_status m t.
187 return aux_get_typing byte8 with
188 [ HC05 ⇒ acc_low_reg_HC05
189 | HC08 ⇒ acc_low_reg_HC08
190 | HCS08 ⇒ acc_low_reg_HC08
191 | RS08 ⇒ acc_low_reg_RS08 ]
194 (* getter di X, non esiste sempre *)
195 ndefinition get_indX_8_low_reg ≝
196 λm:mcu_type.λt:memory_impl.λs:any_status m t.
198 return aux_get_typing (option byte8) with
199 [ HC05 ⇒ λalu.Some ? (indX_low_reg_HC05 alu)
200 | HC08 ⇒ λalu.Some ? (indX_low_reg_HC08 alu)
201 | HCS08 ⇒ λalu.Some ? (indX_low_reg_HC08 alu)
202 | RS08 ⇒ λalu.None ? ]
205 (* getter di H, non esiste sempre *)
206 ndefinition get_indX_8_high_reg ≝
207 λm:mcu_type.λt:memory_impl.λs:any_status m t.
209 return aux_get_typing (option byte8) with
211 | HC08 ⇒ λalu.Some ? (indX_high_reg_HC08 alu)
212 | HCS08 ⇒ λalu.Some ? (indX_high_reg_HC08 alu)
213 | RS08 ⇒ λalu.None ? ]
216 (* getter di H:X, non esiste sempre *)
217 ndefinition get_indX_16_reg ≝
218 λm:mcu_type.λt:memory_impl.λs:any_status m t.
220 return aux_get_typing (option word16) with
222 | HC08 ⇒ λalu.Some ? (mk_word16 (indX_high_reg_HC08 alu) (indX_low_reg_HC08 alu))
223 | HCS08 ⇒ λalu.Some ? (mk_word16 (indX_high_reg_HC08 alu) (indX_low_reg_HC08 alu))
224 | RS08 ⇒ λalu.None ? ]
227 (* getter di SP, non esiste sempre *)
228 ndefinition get_sp_reg ≝
229 λm:mcu_type.λt:memory_impl.λs:any_status m t.
231 return aux_get_typing (option word16) with
232 [ HC05 ⇒ λalu.Some ? (sp_reg_HC05 alu)
233 | HC08 ⇒ λalu.Some ? (sp_reg_HC08 alu)
234 | HCS08 ⇒ λalu.Some ? (sp_reg_HC08 alu)
235 | RS08 ⇒ λalu.None ? ]
238 (* getter di PC, esiste sempre *)
239 ndefinition get_pc_reg ≝
240 λm:mcu_type.λt:memory_impl.λs:any_status m t.
242 return aux_get_typing word16 with
245 | HCS08 ⇒ pc_reg_HC08
246 | RS08 ⇒ pc_reg_RS08 ]
249 (* getter di SPC, non esiste sempre *)
250 ndefinition get_spc_reg ≝
251 λm:mcu_type.λt:memory_impl.λs:any_status m t.
253 return aux_get_typing (option word16) with
256 | HCS08 ⇒ λalu.None ?
257 | RS08 ⇒ λalu.Some ? (spc_reg_RS08 alu) ]
260 (* REGISTRI MEMORY MAPPED *)
262 (* getter di memory mapped X, non esiste sempre *)
263 ndefinition get_x_map ≝
264 λm:mcu_type.λt:memory_impl.λs:any_status m t.
266 return aux_get_typing (option byte8) with
269 | HCS08 ⇒ λalu.None ?
270 | RS08 ⇒ λalu.Some ? (x_map_RS08 alu) ]
273 (* getter di memory mapped PS, non esiste sempre *)
274 ndefinition get_ps_map ≝
275 λm:mcu_type.λt:memory_impl.λs:any_status m t.
277 return aux_get_typing (option byte8) with
280 | HCS08 ⇒ λalu.None ?
281 | RS08 ⇒ λalu.Some ? (ps_map_RS08 alu) ]
286 (* getter di V, non esiste sempre *)
287 ndefinition get_v_flag ≝
288 λm:mcu_type.λt:memory_impl.λs:any_status m t.
290 return aux_get_typing (option bool) with
292 | HC08 ⇒ λalu.Some ? (v_flag_HC08 alu)
293 | HCS08 ⇒ λalu.Some ? (v_flag_HC08 alu)
294 | RS08 ⇒ λalu.None ? ]
297 (* getter di H, non esiste sempre *)
298 ndefinition get_h_flag ≝
299 λm:mcu_type.λt:memory_impl.λs:any_status m t.
301 return aux_get_typing (option bool) with
302 [ HC05 ⇒ λalu.Some ? (h_flag_HC05 alu)
303 | HC08 ⇒ λalu.Some ? (h_flag_HC08 alu)
304 | HCS08 ⇒ λalu.Some ? (h_flag_HC08 alu)
305 | RS08 ⇒ λalu.None ? ]
308 (* getter di I, non esiste sempre *)
309 ndefinition get_i_flag ≝
310 λm:mcu_type.λt:memory_impl.λs:any_status m t.
312 return aux_get_typing (option bool) with
313 [ HC05 ⇒ λalu.Some ? (i_flag_HC05 alu)
314 | HC08 ⇒ λalu.Some ? (i_flag_HC08 alu)
315 | HCS08 ⇒ λalu.Some ? (i_flag_HC08 alu)
316 | RS08 ⇒ λalu.None ? ]
319 (* getter di N, non esiste sempre *)
320 ndefinition get_n_flag ≝
321 λm:mcu_type.λt:memory_impl.λs:any_status m t.
323 return aux_get_typing (option bool) with
324 [ HC05 ⇒ λalu.Some ? (n_flag_HC05 alu)
325 | HC08 ⇒ λalu.Some ? (n_flag_HC08 alu)
326 | HCS08 ⇒ λalu.Some ? (n_flag_HC08 alu)
327 | RS08 ⇒ λalu.None ? ]
330 (* getter di Z, esiste sempre *)
331 ndefinition get_z_flag ≝
332 λm:mcu_type.λt:memory_impl.λs:any_status m t.
334 return aux_get_typing bool with
337 | HCS08 ⇒ z_flag_HC08
338 | RS08 ⇒ z_flag_RS08 ]
341 (* getter di C, esiste sempre *)
342 ndefinition get_c_flag ≝
343 λm:mcu_type.λt:memory_impl.λs:any_status m t.
345 return aux_get_typing bool with
348 | HCS08 ⇒ c_flag_HC08
349 | RS08 ⇒ c_flag_RS08 ]
352 (* getter di IRQ, non esiste sempre *)
353 ndefinition get_irq_flag ≝
354 λm:mcu_type.λt:memory_impl.λs:any_status m t.
356 return aux_get_typing (option bool) with
357 [ HC05 ⇒ λalu.Some ? (irq_flag_HC05 alu)
358 | HC08 ⇒ λalu.Some ? (irq_flag_HC08 alu)
359 | HCS08 ⇒ λalu.Some ? (irq_flag_HC08 alu)
360 | RS08 ⇒ λalu.None ? ]
363 (* ***************************** *)
364 (* SETTER SPECIFICI FORTI/DEBOLI *)
365 (* ***************************** *)
367 (* funzione ausiliaria per il tipaggio dei setter forti *)
368 ndefinition aux_set_typing ≝ λx:Type.λm:mcu_type.
369 match m with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ]
371 match m with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ].
373 (* funzione ausiliaria per il tipaggio dei setter deboli *)
374 ndefinition aux_set_typing_opt ≝ λx:Type.λm:mcu_type.option
375 (match m with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ]
377 match m with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ]).
379 (* DESCRITTORI ESTERNI ALLA ALU *)
381 (* setter forte della ALU *)
382 ndefinition set_alu ≝
383 λm:mcu_type.λt:memory_impl.λs:any_status m t.λalu'.
384 mk_any_status m t alu' (mem_desc m t s) (chk_desc m t s) (clk_desc m t s).
386 (* setter forte della memoria *)
387 ndefinition set_mem_desc ≝
388 λm:mcu_type.λt:memory_impl.λs:any_status m t.λmem':aux_mem_type t.
389 mk_any_status m t (alu m t s) mem' (chk_desc m t s) (clk_desc m t s).
391 (* setter forte del descrittore *)
392 ndefinition set_chk_desc ≝
393 λm:mcu_type.λt:memory_impl.λs:any_status m t.λchk':aux_chk_type t.
394 mk_any_status m t (alu m t s) (mem_desc m t s) chk' (clk_desc m t s).
396 (* setter forte del clik *)
397 ndefinition set_clk_desc ≝
398 λm:mcu_type.λt:memory_impl.λs:any_status m t.
399 λclk':option (Prod5T byte8 (any_opcode m) (instr_mode) byte8 word16).
400 mk_any_status m t (alu m t s) (mem_desc m t s) (chk_desc m t s) clk'.
404 (* setter specifico HC05 di A *)
405 ndefinition set_acc_8_low_reg_HC05 ≝
409 (indX_low_reg_HC05 alu)
422 (* setter specifico HC08/HCS08 di A *)
423 ndefinition set_acc_8_low_reg_HC08 ≝
427 (indX_low_reg_HC08 alu)
428 (indX_high_reg_HC08 alu)
439 (* setter specifico RS08 di A *)
440 ndefinition set_acc_8_low_reg_RS08 ≝
452 (* setter forte di A *)
453 ndefinition set_acc_8_low_reg ≝
454 λm:mcu_type.λt:memory_impl.λs:any_status m t.λacclow':byte8.
456 (match m return aux_set_typing byte8 with
457 [ HC05 ⇒ set_acc_8_low_reg_HC05
458 | HC08 ⇒ set_acc_8_low_reg_HC08
459 | HCS08 ⇒ set_acc_8_low_reg_HC08
460 | RS08 ⇒ set_acc_8_low_reg_RS08
461 ] (alu m t s) acclow').
465 (* setter specifico HC05 di X *)
466 ndefinition set_indX_8_low_reg_HC05 ≝
467 λalu.λindxlow':byte8.
469 (acc_low_reg_HC05 alu)
483 (* setter specifico HC08/HCS08 di X *)
484 ndefinition set_indX_8_low_reg_HC08 ≝
485 λalu.λindxlow':byte8.
487 (acc_low_reg_HC08 alu)
489 (indX_high_reg_HC08 alu)
500 (* setter forte di X *)
501 ndefinition set_indX_8_low_reg ≝
502 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindxlow':byte8.
503 opt_map … (match m return aux_set_typing_opt byte8 with
504 [ HC05 ⇒ Some ? set_indX_8_low_reg_HC05
505 | HC08 ⇒ Some ? set_indX_8_low_reg_HC08
506 | HCS08 ⇒ Some ? set_indX_8_low_reg_HC08
508 (λf.Some ? (set_alu m t s (f (alu m t s) indxlow'))).
510 (* setter debole di X *)
511 ndefinition setweak_indX_8_low_reg ≝
512 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindxlow':byte8.
513 match set_indX_8_low_reg m t s indxlow' with
514 [ None ⇒ s | Some s' ⇒ s' ].
518 (* setter specifico HC08/HCS08 di H *)
519 ndefinition set_indX_8_high_reg_HC08 ≝
520 λalu.λindxhigh':byte8.
522 (acc_low_reg_HC08 alu)
523 (indX_low_reg_HC08 alu)
535 (* setter forte di H *)
536 ndefinition set_indX_8_high_reg ≝
537 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindxhigh':byte8.
538 opt_map … (match m return aux_set_typing_opt byte8 with
540 | HC08 ⇒ Some ? set_indX_8_high_reg_HC08
541 | HCS08 ⇒ Some ? set_indX_8_high_reg_HC08
543 (λf.Some ? (set_alu m t s (f (alu m t s) indxhigh'))).
545 (* setter debole di H *)
546 ndefinition setweak_indX_8_high_reg ≝
547 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindxhigh':byte8.
548 match set_indX_8_high_reg m t s indxhigh' with
549 [ None ⇒ s | Some s' ⇒ s' ].
553 (* setter specifico HC08/HCS08 di H:X *)
554 ndefinition set_indX_16_reg_HC08 ≝
557 (acc_low_reg_HC08 alu)
570 (* setter forte di H:X *)
571 ndefinition set_indX_16_reg ≝
572 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindx16:word16.
573 opt_map … (match m return aux_set_typing_opt word16 with
575 | HC08 ⇒ Some ? set_indX_16_reg_HC08
576 | HCS08 ⇒ Some ? set_indX_16_reg_HC08
578 (λf.Some ? (set_alu m t s (f (alu m t s) indx16))).
580 (* setter debole di H:X *)
581 ndefinition setweak_indX_16_reg ≝
582 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindx16:word16.
583 match set_indX_16_reg m t s indx16 with
584 [ None ⇒ s | Some s' ⇒ s' ].
588 (* setter specifico HC05 di SP, effettua (SP∧mask)∨fix *)
589 ndefinition set_sp_reg_HC05 ≝
592 (acc_low_reg_HC05 alu)
593 (indX_low_reg_HC05 alu)
594 (or_w16 (and_w16 sp' (sp_mask_HC05 alu)) (sp_fix_HC05 alu))
606 (* setter specifico HC08/HCS08 di SP *)
607 ndefinition set_sp_reg_HC08 ≝
610 (acc_low_reg_HC08 alu)
611 (indX_low_reg_HC08 alu)
612 (indX_high_reg_HC08 alu)
623 (* setter forte di SP *)
624 ndefinition set_sp_reg ≝
625 λm:mcu_type.λt:memory_impl.λs:any_status m t.λsp':word16.
626 opt_map … (match m return aux_set_typing_opt word16 with
627 [ HC05 ⇒ Some ? set_sp_reg_HC05
628 | HC08 ⇒ Some ? set_sp_reg_HC08
629 | HCS08 ⇒ Some ? set_sp_reg_HC08
631 (λf.Some ? (set_alu m t s (f (alu m t s) sp'))).
633 (* setter debole di SP *)
634 ndefinition setweak_sp_reg ≝
635 λm:mcu_type.λt:memory_impl.λs:any_status m t.λsp':word16.
636 match set_sp_reg m t s sp' with
637 [ None ⇒ s | Some s' ⇒ s' ].
641 (* setter specifico HC05 di PC, effettua PC∧mask *)
642 ndefinition set_pc_reg_HC05 ≝
645 (acc_low_reg_HC05 alu)
646 (indX_low_reg_HC05 alu)
650 (and_w16 pc' (pc_mask_HC05 alu))
659 (* setter specifico HC08/HCS08 di PC *)
660 ndefinition set_pc_reg_HC08 ≝
663 (acc_low_reg_HC08 alu)
664 (indX_low_reg_HC08 alu)
665 (indX_high_reg_HC08 alu)
676 (* setter specifico RS08 di PC, effettua PC∧mask *)
677 ndefinition set_pc_reg_RS08 ≝
680 (acc_low_reg_RS08 alu)
681 (and_w16 pc' (pc_mask_RS08 alu))
689 (* setter forte di PC *)
690 ndefinition set_pc_reg ≝
691 λm:mcu_type.λt:memory_impl.λs:any_status m t.λpc':word16.
693 (match m return aux_set_typing word16 with
694 [ HC05 ⇒ set_pc_reg_HC05
695 | HC08 ⇒ set_pc_reg_HC08
696 | HCS08 ⇒ set_pc_reg_HC08
697 | RS08 ⇒ set_pc_reg_RS08
702 (* setter specifico RS08 di SPC, effettua SPC∧mask *)
703 ndefinition set_spc_reg_RS08 ≝
706 (acc_low_reg_RS08 alu)
709 (and_w16 spc' (pc_mask_RS08 alu))
715 (* setter forte di SPC *)
716 ndefinition set_spc_reg ≝
717 λm:mcu_type.λt:memory_impl.λs:any_status m t.λspc':word16.
718 opt_map … (match m return aux_set_typing_opt word16 with
722 | RS08 ⇒ Some ? set_spc_reg_RS08 ])
723 (λf.Some ? (set_alu m t s (f (alu m t s) spc'))).
725 (* setter debole di SPC *)
726 ndefinition setweak_spc_reg ≝
727 λm:mcu_type.λt:memory_impl.λs:any_status m t.λspc':word16.
728 match set_spc_reg m t s spc' with
729 [ None ⇒ s | Some s' ⇒ s' ].
731 (* REGISTRO MEMORY MAPPED X *)
733 (* setter specifico RS08 di memory mapped X *)
734 ndefinition set_x_map_RS08 ≝
737 (acc_low_reg_RS08 alu)
746 (* setter forte di memory mapped X *)
747 ndefinition set_x_map ≝
748 λm:mcu_type.λt:memory_impl.λs:any_status m t.λxm':byte8.
749 opt_map … (match m return aux_set_typing_opt byte8 with
753 | RS08 ⇒ Some ? set_x_map_RS08 ])
754 (λf.Some ? (set_alu m t s (f (alu m t s) xm'))).
756 (* setter debole di memory mapped X *)
757 ndefinition setweak_x_map ≝
758 λm:mcu_type.λt:memory_impl.λs:any_status m t.λxm':byte8.
759 match set_x_map m t s xm' with
760 [ None ⇒ s | Some s' ⇒ s' ].
762 (* REGISTRO MEMORY MAPPED PS *)
764 (* setter specifico RS08 di memory mapped PS *)
765 ndefinition set_ps_map_RS08 ≝
768 (acc_low_reg_RS08 alu)
777 (* setter forte di memory mapped PS *)
778 ndefinition set_ps_map ≝
779 λm:mcu_type.λt:memory_impl.λs:any_status m t.λpsm':byte8.
780 opt_map … (match m return aux_set_typing_opt byte8 with
784 | RS08 ⇒ Some ? set_ps_map_RS08 ])
785 (λf.Some ? (set_alu m t s (f (alu m t s) psm'))).
787 (* setter debole di memory mapped PS *)
788 ndefinition setweak_ps_map ≝
789 λm:mcu_type.λt:memory_impl.λs:any_status m t.λpsm':byte8.
790 match set_ps_map m t s psm' with
791 [ None ⇒ s | Some s' ⇒ s' ].
795 (* setter specifico HC08/HCS08 di V *)
796 ndefinition set_v_flag_HC08 ≝
799 (acc_low_reg_HC08 alu)
800 (indX_low_reg_HC08 alu)
801 (indX_high_reg_HC08 alu)
812 (* setter forte di V *)
813 ndefinition set_v_flag ≝
814 λm:mcu_type.λt:memory_impl.λs:any_status m t.λvfl':bool.
815 opt_map … (match m return aux_set_typing_opt bool with
817 | HC08 ⇒ Some ? set_v_flag_HC08
818 | HCS08 ⇒ Some ? set_v_flag_HC08
820 (λf.Some ? (set_alu m t s (f (alu m t s) vfl'))).
822 (* setter debole di V *)
823 ndefinition setweak_v_flag ≝
824 λm:mcu_type.λt:memory_impl.λs:any_status m t.λvfl':bool.
825 match set_v_flag m t s vfl' with
826 [ None ⇒ s | Some s' ⇒ s' ].
830 (* setter specifico HC05 di H *)
831 ndefinition set_h_flag_HC05 ≝
834 (acc_low_reg_HC05 alu)
835 (indX_low_reg_HC05 alu)
848 (* setter specifico HC08/HCS08 di H *)
849 ndefinition set_h_flag_HC08 ≝
852 (acc_low_reg_HC08 alu)
853 (indX_low_reg_HC08 alu)
854 (indX_high_reg_HC08 alu)
865 (* setter forte di H *)
866 ndefinition set_h_flag ≝
867 λm:mcu_type.λt:memory_impl.λs:any_status m t.λhfl':bool.
868 opt_map … (match m return aux_set_typing_opt bool with
869 [ HC05 ⇒ Some ? set_h_flag_HC05
870 | HC08 ⇒ Some ? set_h_flag_HC08
871 | HCS08 ⇒ Some ? set_h_flag_HC08
873 (λf.Some ? (set_alu m t s (f (alu m t s) hfl'))).
875 (* setter debole di H *)
876 ndefinition setweak_h_flag ≝
877 λm:mcu_type.λt:memory_impl.λs:any_status m t.λhfl':bool.
878 match set_h_flag m t s hfl' with
879 [ None ⇒ s | Some s' ⇒ s' ].
883 (* setter specifico HC05 di I *)
884 ndefinition set_i_flag_HC05 ≝
887 (acc_low_reg_HC05 alu)
888 (indX_low_reg_HC05 alu)
901 (* setter specifico HC08/HCS08 di I *)
902 ndefinition set_i_flag_HC08 ≝
905 (acc_low_reg_HC08 alu)
906 (indX_low_reg_HC08 alu)
907 (indX_high_reg_HC08 alu)
918 (* setter forte di I *)
919 ndefinition set_i_flag ≝
920 λm:mcu_type.λt:memory_impl.λs:any_status m t.λifl':bool.
921 opt_map … (match m return aux_set_typing_opt bool with
922 [ HC05 ⇒ Some ? set_i_flag_HC05
923 | HC08 ⇒ Some ? set_i_flag_HC08
924 | HCS08 ⇒ Some ? set_i_flag_HC08
926 (λf.Some ? (set_alu m t s (f (alu m t s) ifl'))).
928 (* setter debole di I *)
929 ndefinition setweak_i_flag ≝
930 λm:mcu_type.λt:memory_impl.λs:any_status m t.λifl':bool.
931 match set_i_flag m t s ifl' with
932 [ None ⇒ s | Some s' ⇒ s' ].
936 (* setter specifico HC05 di N *)
937 ndefinition set_n_flag_HC05 ≝
940 (acc_low_reg_HC05 alu)
941 (indX_low_reg_HC05 alu)
954 (* setter specifico HC08/HCS08 di N *)
955 ndefinition set_n_flag_HC08 ≝
958 (acc_low_reg_HC08 alu)
959 (indX_low_reg_HC08 alu)
960 (indX_high_reg_HC08 alu)
971 (* setter forte di N *)
972 ndefinition set_n_flag ≝
973 λm:mcu_type.λt:memory_impl.λs:any_status m t.λnfl':bool.
974 opt_map … (match m return aux_set_typing_opt bool with
975 [ HC05 ⇒ Some ? set_n_flag_HC05
976 | HC08 ⇒ Some ? set_n_flag_HC08
977 | HCS08 ⇒ Some ? set_n_flag_HC08
979 (λf.Some ? (set_alu m t s (f (alu m t s) nfl'))).
981 (* setter debole di N *)
982 ndefinition setweak_n_flag ≝
983 λm:mcu_type.λt:memory_impl.λs:any_status m t.λnfl':bool.
984 match set_n_flag m t s nfl' with
985 [ None ⇒ s | Some s' ⇒ s' ].
989 (* setter specifico HC05 di Z *)
990 ndefinition set_z_flag_HC05 ≝
993 (acc_low_reg_HC05 alu)
994 (indX_low_reg_HC05 alu)
1005 (irq_flag_HC05 alu).
1007 (* setter specifico HC08/HCS08 di Z *)
1008 ndefinition set_z_flag_HC08 ≝
1011 (acc_low_reg_HC08 alu)
1012 (indX_low_reg_HC08 alu)
1013 (indX_high_reg_HC08 alu)
1022 (irq_flag_HC08 alu).
1024 (* setter sprcifico RS08 di Z *)
1025 ndefinition set_z_flag_RS08 ≝
1028 (acc_low_reg_RS08 alu)
1037 (* setter forte di Z *)
1038 ndefinition set_z_flag ≝
1039 λm:mcu_type.λt:memory_impl.λs:any_status m t.λzfl':bool.
1041 (match m return aux_set_typing bool with
1042 [ HC05 ⇒ set_z_flag_HC05
1043 | HC08 ⇒ set_z_flag_HC08
1044 | HCS08 ⇒ set_z_flag_HC08
1045 | RS08 ⇒ set_z_flag_RS08
1046 ] (alu m t s) zfl').
1050 (* setter specifico HC05 di C *)
1051 ndefinition set_c_flag_HC05 ≝
1054 (acc_low_reg_HC05 alu)
1055 (indX_low_reg_HC05 alu)
1066 (irq_flag_HC05 alu).
1068 (* setter specifico HC08/HCS08 di C *)
1069 ndefinition set_c_flag_HC08 ≝
1072 (acc_low_reg_HC08 alu)
1073 (indX_low_reg_HC08 alu)
1074 (indX_high_reg_HC08 alu)
1083 (irq_flag_HC08 alu).
1085 (* setter specifico RS08 di C *)
1086 ndefinition set_c_flag_RS08 ≝
1089 (acc_low_reg_RS08 alu)
1098 (* setter forte di C *)
1099 ndefinition set_c_flag ≝
1100 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcfl':bool.
1102 (match m return aux_set_typing bool with
1103 [ HC05 ⇒ set_c_flag_HC05
1104 | HC08 ⇒ set_c_flag_HC08
1105 | HCS08 ⇒ set_c_flag_HC08
1106 | RS08 ⇒ set_c_flag_RS08
1107 ] (alu m t s) cfl').
1111 (* setter specifico HC05 di IRQ *)
1112 ndefinition set_irq_flag_HC05 ≝
1115 (acc_low_reg_HC05 alu)
1116 (indX_low_reg_HC05 alu)
1129 (* setter specifico HC08/HCS08 di IRQ *)
1130 ndefinition set_irq_flag_HC08 ≝
1133 (acc_low_reg_HC08 alu)
1134 (indX_low_reg_HC08 alu)
1135 (indX_high_reg_HC08 alu)
1146 (* setter forte di IRQ *)
1147 ndefinition set_irq_flag ≝
1148 λm:mcu_type.λt:memory_impl.λs:any_status m t.λirqfl':bool.
1149 opt_map … (match m return aux_set_typing_opt bool with
1150 [ HC05 ⇒ Some ? set_irq_flag_HC05
1151 | HC08 ⇒ Some ? set_irq_flag_HC08
1152 | HCS08 ⇒ Some ? set_irq_flag_HC08
1154 (λf.Some ? (set_alu m t s (f (alu m t s) irqfl'))).
1156 (* setter debole di IRQ *)
1157 ndefinition setweak_irq_flag ≝
1158 λm:mcu_type.λt:memory_impl.λs:any_status m t.λirqfl':bool.
1159 match set_irq_flag m t s irqfl' with
1160 [ None ⇒ s | Some s' ⇒ s' ].
1162 (* ***************** *)
1163 (* CONFRONTO FRA ALU *)
1164 (* ***************** *)
1166 (* confronto registro per registro dell'HC05 *)
1167 ndefinition eq_aluHC05 ≝
1168 λalu1,alu2:alu_HC05.
1170 [ mk_alu_HC05 acclow1 indxlow1 sp1 spm1 spf1 pc1 pcm1 hfl1 ifl1 nfl1 zfl1 cfl1 irqfl1 ⇒
1172 [ mk_alu_HC05 acclow2 indxlow2 sp2 spm2 spf2 pc2 pcm2 hfl2 ifl2 nfl2 zfl2 cfl2 irqfl2 ⇒
1173 (eq_b8 acclow1 acclow2) ⊗
1174 (eq_b8 indxlow1 indxlow2) ⊗
1176 (eq_w16 spm1 spm2) ⊗
1177 (eq_w16 spf1 spf2) ⊗
1179 (eq_w16 pcm1 pcm2) ⊗
1180 (eq_bool hfl1 hfl2) ⊗
1181 (eq_bool ifl1 ifl2) ⊗
1182 (eq_bool nfl1 nfl2) ⊗
1183 (eq_bool zfl1 zfl2) ⊗
1184 (eq_bool cfl1 cfl2) ⊗
1185 (eq_bool irqfl1 irqfl2) ]].
1187 (* confronto registro per registro dell'HC08 *)
1188 ndefinition eq_aluHC08 ≝
1189 λalu1,alu2:alu_HC08.
1191 [ mk_alu_HC08 acclow1 indxlow1 indxhigh1 sp1 pc1 vfl1 hfl1 ifl1 nfl1 zfl1 cfl1 irqfl1 ⇒
1193 [ mk_alu_HC08 acclow2 indxlow2 indxhigh2 sp2 pc2 vfl2 hfl2 ifl2 nfl2 zfl2 cfl2 irqfl2 ⇒
1194 (eq_b8 acclow1 acclow2) ⊗
1195 (eq_b8 indxlow1 indxlow2) ⊗
1196 (eq_b8 indxhigh1 indxhigh2) ⊗
1199 (eq_bool vfl1 vfl2) ⊗
1200 (eq_bool hfl1 hfl2) ⊗
1201 (eq_bool ifl1 ifl2) ⊗
1202 (eq_bool nfl1 nfl2) ⊗
1203 (eq_bool zfl1 zfl2) ⊗
1204 (eq_bool cfl1 cfl2) ⊗
1205 (eq_bool irqfl1 irqfl2) ]].
1207 (* confronto registro per registro dell'RS08 *)
1208 ndefinition eq_aluRS08 ≝
1209 λalu1,alu2:alu_RS08.
1211 [ mk_alu_RS08 acclow1 pc1 pcm1 spc1 xm1 psm1 zfl1 cfl1 ⇒
1213 [ mk_alu_RS08 acclow2 pc2 pcm2 spc2 xm2 psm2 zfl2 cfl2 ⇒
1214 (eq_b8 acclow1 acclow2) ⊗
1216 (eq_w16 pcm1 pcm2) ⊗
1217 (eq_w16 spc1 spc2) ⊗
1220 (eq_bool zfl1 zfl2) ⊗
1221 (eq_bool cfl1 cfl2) ]].
1223 (* ******************** *)
1224 (* CONFRONTO FRA STATUS *)
1225 (* ******************** *)
1227 (* confronto di una regione di memoria [addr1 ; ... ; addrn] *)
1228 nlet rec forall_memory_ranged
1230 (chk1:aux_chk_type t) (chk2:aux_chk_type t)
1231 (mem1:aux_mem_type t) (mem2:aux_mem_type t)
1232 (addrl:list word16) on addrl ≝
1233 match addrl return λ_.bool with
1235 | cons hd tl ⇒ (eq_option byte8 (mem_read t mem1 chk1 hd)
1236 (mem_read t mem2 chk2 hd) eq_b8) ⊗
1237 (forall_memory_ranged t chk1 chk2 mem1 mem2 tl)
1240 (* il clk e' option (Prod5T byte8 (any_opcode m) (instr_mode) byte8 word16) *)
1241 ndefinition eq_clk ≝
1242 λm:mcu_type.λc1,c2:option (Prod5T byte8 (any_opcode m) (instr_mode) byte8 word16).
1244 [ None ⇒ match c2 with
1245 [ None ⇒ true | Some _ ⇒ false ]
1246 | Some c1' ⇒ match c2 with
1247 [ None ⇒ false | Some c2' ⇒ (eq_b8 (fst5T … c1') (fst5T … c2')) ⊗
1248 (eq_anyop m (snd5T … c1') (snd5T … c2')) ⊗
1249 (eq_im (thd5T … c1') (thd5T … c2')) ⊗
1250 (eq_b8 (frth5T … c1') (frth5T … c2')) ⊗
1251 (eq_w16 (ffth5T … c1') (ffth5T … c2')) ]
1254 (* generalizzazione del confronto fra stati *)
1255 ndefinition eq_anystatus ≝
1256 λm:mcu_type.λt:memory_impl.λs1,s2:any_status m t.λaddrl:list word16.
1257 match s1 with [ mk_any_status alu1 mem1 chk1 clk1 ⇒
1258 match s2 with [ mk_any_status alu2 mem2 chk2 clk2 ⇒
1260 (* 1) confronto della ALU *)
1261 (match m return λm:mcu_type.
1263 [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ] →
1265 [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ] →
1267 [ HC05 ⇒ eq_aluHC05 | HC08 ⇒ eq_aluHC08 | HCS08 ⇒ eq_aluHC08 | RS08 ⇒ eq_aluRS08 ]
1270 (* 2) confronto della memoria in [inf,inf+n] *)
1271 (forall_memory_ranged t chk1 chk2 mem1 mem2 addrl) ⊗
1273 (* 3) confronto del clik *)
1274 (eq_clk m clk1 clk2)