1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* ********************************************************************** *)
16 (* Progetto FreeScale *)
18 (* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *)
19 (* Cosimo Oliboni, oliboni@cs.unibo.it *)
21 (* ********************************************************************** *)
23 include "freescale/memory_abs.ma".
24 include "freescale/opcode_base.ma".
25 include "freescale/prod.ma".
27 (* *********************************** *)
28 (* STATUS INTERNO DEL PROCESSORE (ALU) *)
29 (* *********************************** *)
32 nrecord alu_HC05: Type ≝
34 (* A: registo accumulatore *)
35 acc_low_reg_HC05 : byte8;
36 (* X: registro indice *)
37 indX_low_reg_HC05 : byte8;
38 (* SP: registo stack pointer *)
40 (* modificatori di SP: per esempio e' definito come 0000000011xxxxxxb *)
41 (* la logica della sua costruzione e' quindi (SP∧mask)∨fix *)
42 (* totalmente racchiusa nella ALU, bastera' fare get(set(SP)) *)
43 sp_mask_HC05 : word16;
45 (* PC: registro program counter *)
47 (* modificatore di PC: per esempio e' definito come 00xxxxxxxxxxxxxxb *)
48 (* la logica della sua costruzione e' quindi (PC∧mask) *)
49 (* totalmente racchiusa nella ALU, bastera' fare get(set(PC)) *)
50 pc_mask_HC05 : word16;
52 (* H: flag semi-carry (somma nibble basso) *)
54 (* I: flag mascheramento degli interrupt mascherabili: 1=mascherati *)
56 (* N: flag segno/negativita' *)
63 (* IRQ: flag che simula il pin esterno IRQ *)
67 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)}"
68 non associative with precedence 80 for
69 @{ 'mk_alu_HC05 $acclow $indxlow $sp $spm $spf $pc $pcm $hfl $ifl $nfl $zfl $cfl $irqfl }.
70 interpretation "mk_alu_HC05" 'mk_alu_HC05 acclow indxlow sp spm spf pc pcm hfl ifl nfl zfl cfl irqfl =
71 (mk_alu_HC05 acclow indxlow sp spm spf pc pcm hfl ifl nfl zfl cfl irqfl).
73 (* ALU dell'HC08/HCS08 *)
74 nrecord alu_HC08: Type ≝
76 (* A: registo accumulatore *)
77 acc_low_reg_HC08 : byte8;
78 (* X: registro indice parte bassa *)
79 indX_low_reg_HC08 : byte8;
80 (* H: registro indice parte alta *)
81 indX_high_reg_HC08 : byte8;
82 (* SP: registo stack pointer *)
84 (* PC: registro program counter *)
87 (* V: flag overflow *)
89 (* H: flag semi-carry (somma nibble basso) *)
91 (* I: flag mascheramento degli interrupt mascherabili: 1=mascherati *)
93 (* N: flag segno/negativita' *)
100 (* IRQ: flag che simula il pin esterno IRQ *)
104 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)}"
105 non associative with precedence 80 for
106 @{ 'mk_alu_HC08 $acclow $indxlow $indxhigh $sp $pc $vfl $hfl $ifl $nfl $zfl $cfl $irqfl }.
107 interpretation "mk_alu_HC08" 'mk_alu_HC08 acclow indxlow indxhigh sp pc vfl hfl ifl nfl zfl cfl irqfl =
108 (mk_alu_HC08 acclow indxlow indxhigh sp pc vfl hfl ifl nfl zfl cfl irqfl).
111 nrecord alu_RS08: Type ≝
113 (* A: registo accumulatore *)
114 acc_low_reg_RS08 : byte8;
115 (* PC: registro program counter *)
116 pc_reg_RS08 : word16;
117 (* modificatore di PC: per esempio e' definito come 00xxxxxxxxxxxxxxb *)
118 (* la logica della sua costruzione e' quindi (PC∧mask) *)
119 (* totalmente racchiusa nella ALU, bastera' fare get(set(PC)) *)
120 pc_mask_RS08 : word16;
121 (* SPC: registro shadow program counter *)
122 (* NB: il suo modificatore e' lo stesso di PC *)
123 spc_reg_RS08 : word16;
125 (* X: registro indice parte bassa *)
126 (* NB: in realta' e' mappato in memoria e non risiede nella ALU *)
127 (* la lettura/scrittura avviene tramite la locazione [0x000F] *)
128 (* la funzione memory_filter_read/write si occupera' di intercettare *)
129 (* e deviare sul registro le letture/scritture (modulo load_write) *)
131 (* PS: registro selezione di pagina *)
132 (* serve a indirizzare la finestra RAM di 64b [0x00C0-0x00FF] *)
133 (* su tutta la memoria installata [0x0000-0x3FFF]: [00pp pppp ppxx xxxx] *)
134 (* NB: in realta' e' mappato in memoria e non risiede nella ALU *)
135 (* la lettura/scrittura avviene tramite la locazione [0x001F] *)
136 (* la funzione memory_filter_read/write si occupera' di intercettare *)
137 (* e deviare sul registro le letture/scritture (modulo load_write) *)
146 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)}"
147 non associative with precedence 80 for
148 @{ 'mk_alu_RS08 $acclow $pc $pcm $spc $xm $psm $zfl $cfl }.
149 interpretation "mk_alu_RS08" 'mk_alu_RS08 acclow pc pcm spc xm psm zfl cfl =
150 (mk_alu_RS08 acclow pc pcm spc xm psm zfl cfl).
152 (* tipo processore dipendente dalla mcu, varia solo la ALU *)
153 nrecord any_status (mcu:mcu_type) (t:memory_impl): Type ≝
156 [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ];
158 (* descritore della memoria *)
159 mem_desc : aux_mem_type t;
160 (* descrittore del tipo di memoria installata *)
161 chk_desc : aux_chk_type t;
162 (* descrittore del click = stato di avanzamento dell'esecuzione+cur_pc conseguente a fetch *)
163 (* 1) None = istruzione eseguita, attesa del fetch *)
164 (* 2) Some cur_clk,pseudo,mode,clks,cur_pc = fetch eseguito, countup a esecuzione *)
165 clk_desc : option (Prod5T byte8 (any_opcode mcu) (instr_mode) byte8 word16)
168 (* evitare di mostrare la memoria/descrittore che impalla il visualizzatore *)
169 notation > "{hvbox('Alu' ≝ alu ; break 'Clk' ≝ clk)}" non associative with precedence 80
170 for @{ 'mk_any_status $alu $mem $chk $clk }.
171 interpretation "mk_any_status" 'mk_any_status alu mem chk clk =
172 (mk_any_status alu mem chk clk).
174 (* **************** *)
175 (* GETTER SPECIFICI *)
176 (* **************** *)
178 (* funzione ausiliaria per il tipaggio dei getter *)
179 ndefinition aux_get_typing ≝ λx:Type.λm:mcu_type.match m with
180 [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ] → x.
184 (* getter di A, esiste sempre *)
185 ndefinition get_acc_8_low_reg ≝
186 λm:mcu_type.λt:memory_impl.λs:any_status m t.
188 return aux_get_typing byte8 with
189 [ HC05 ⇒ acc_low_reg_HC05
190 | HC08 ⇒ acc_low_reg_HC08
191 | HCS08 ⇒ acc_low_reg_HC08
192 | RS08 ⇒ acc_low_reg_RS08 ]
195 (* getter di X, non esiste sempre *)
196 ndefinition get_indX_8_low_reg ≝
197 λm:mcu_type.λt:memory_impl.λs:any_status m t.
199 return aux_get_typing (option byte8) with
200 [ HC05 ⇒ λalu.Some ? (indX_low_reg_HC05 alu)
201 | HC08 ⇒ λalu.Some ? (indX_low_reg_HC08 alu)
202 | HCS08 ⇒ λalu.Some ? (indX_low_reg_HC08 alu)
203 | RS08 ⇒ λalu.None ? ]
206 (* getter di H, non esiste sempre *)
207 ndefinition get_indX_8_high_reg ≝
208 λm:mcu_type.λt:memory_impl.λs:any_status m t.
210 return aux_get_typing (option byte8) with
212 | HC08 ⇒ λalu.Some ? (indX_high_reg_HC08 alu)
213 | HCS08 ⇒ λalu.Some ? (indX_high_reg_HC08 alu)
214 | RS08 ⇒ λalu.None ? ]
217 (* getter di H:X, non esiste sempre *)
218 ndefinition get_indX_16_reg ≝
219 λm:mcu_type.λt:memory_impl.λs:any_status m t.
221 return aux_get_typing (option word16) with
223 | HC08 ⇒ λalu.Some ? (mk_word16 (indX_high_reg_HC08 alu) (indX_low_reg_HC08 alu))
224 | HCS08 ⇒ λalu.Some ? (mk_word16 (indX_high_reg_HC08 alu) (indX_low_reg_HC08 alu))
225 | RS08 ⇒ λalu.None ? ]
228 (* getter di SP, non esiste sempre *)
229 ndefinition get_sp_reg ≝
230 λm:mcu_type.λt:memory_impl.λs:any_status m t.
232 return aux_get_typing (option word16) with
233 [ HC05 ⇒ λalu.Some ? (sp_reg_HC05 alu)
234 | HC08 ⇒ λalu.Some ? (sp_reg_HC08 alu)
235 | HCS08 ⇒ λalu.Some ? (sp_reg_HC08 alu)
236 | RS08 ⇒ λalu.None ? ]
239 (* getter di PC, esiste sempre *)
240 ndefinition get_pc_reg ≝
241 λm:mcu_type.λt:memory_impl.λs:any_status m t.
243 return aux_get_typing word16 with
246 | HCS08 ⇒ pc_reg_HC08
247 | RS08 ⇒ pc_reg_RS08 ]
250 (* getter di SPC, non esiste sempre *)
251 ndefinition get_spc_reg ≝
252 λm:mcu_type.λt:memory_impl.λs:any_status m t.
254 return aux_get_typing (option word16) with
257 | HCS08 ⇒ λalu.None ?
258 | RS08 ⇒ λalu.Some ? (spc_reg_RS08 alu) ]
261 (* REGISTRI MEMORY MAPPED *)
263 (* getter di memory mapped X, non esiste sempre *)
264 ndefinition get_x_map ≝
265 λm:mcu_type.λt:memory_impl.λs:any_status m t.
267 return aux_get_typing (option byte8) with
270 | HCS08 ⇒ λalu.None ?
271 | RS08 ⇒ λalu.Some ? (x_map_RS08 alu) ]
274 (* getter di memory mapped PS, non esiste sempre *)
275 ndefinition get_ps_map ≝
276 λm:mcu_type.λt:memory_impl.λs:any_status m t.
278 return aux_get_typing (option byte8) with
281 | HCS08 ⇒ λalu.None ?
282 | RS08 ⇒ λalu.Some ? (ps_map_RS08 alu) ]
287 (* getter di V, non esiste sempre *)
288 ndefinition get_v_flag ≝
289 λm:mcu_type.λt:memory_impl.λs:any_status m t.
291 return aux_get_typing (option bool) with
293 | HC08 ⇒ λalu.Some ? (v_flag_HC08 alu)
294 | HCS08 ⇒ λalu.Some ? (v_flag_HC08 alu)
295 | RS08 ⇒ λalu.None ? ]
298 (* getter di H, non esiste sempre *)
299 ndefinition get_h_flag ≝
300 λm:mcu_type.λt:memory_impl.λs:any_status m t.
302 return aux_get_typing (option bool) with
303 [ HC05 ⇒ λalu.Some ? (h_flag_HC05 alu)
304 | HC08 ⇒ λalu.Some ? (h_flag_HC08 alu)
305 | HCS08 ⇒ λalu.Some ? (h_flag_HC08 alu)
306 | RS08 ⇒ λalu.None ? ]
309 (* getter di I, non esiste sempre *)
310 ndefinition get_i_flag ≝
311 λm:mcu_type.λt:memory_impl.λs:any_status m t.
313 return aux_get_typing (option bool) with
314 [ HC05 ⇒ λalu.Some ? (i_flag_HC05 alu)
315 | HC08 ⇒ λalu.Some ? (i_flag_HC08 alu)
316 | HCS08 ⇒ λalu.Some ? (i_flag_HC08 alu)
317 | RS08 ⇒ λalu.None ? ]
320 (* getter di N, non esiste sempre *)
321 ndefinition get_n_flag ≝
322 λm:mcu_type.λt:memory_impl.λs:any_status m t.
324 return aux_get_typing (option bool) with
325 [ HC05 ⇒ λalu.Some ? (n_flag_HC05 alu)
326 | HC08 ⇒ λalu.Some ? (n_flag_HC08 alu)
327 | HCS08 ⇒ λalu.Some ? (n_flag_HC08 alu)
328 | RS08 ⇒ λalu.None ? ]
331 (* getter di Z, esiste sempre *)
332 ndefinition get_z_flag ≝
333 λm:mcu_type.λt:memory_impl.λs:any_status m t.
335 return aux_get_typing bool with
338 | HCS08 ⇒ z_flag_HC08
339 | RS08 ⇒ z_flag_RS08 ]
342 (* getter di C, esiste sempre *)
343 ndefinition get_c_flag ≝
344 λm:mcu_type.λt:memory_impl.λs:any_status m t.
346 return aux_get_typing bool with
349 | HCS08 ⇒ c_flag_HC08
350 | RS08 ⇒ c_flag_RS08 ]
353 (* getter di IRQ, non esiste sempre *)
354 ndefinition get_irq_flag ≝
355 λm:mcu_type.λt:memory_impl.λs:any_status m t.
357 return aux_get_typing (option bool) with
358 [ HC05 ⇒ λalu.Some ? (irq_flag_HC05 alu)
359 | HC08 ⇒ λalu.Some ? (irq_flag_HC08 alu)
360 | HCS08 ⇒ λalu.Some ? (irq_flag_HC08 alu)
361 | RS08 ⇒ λalu.None ? ]
364 (* ***************************** *)
365 (* SETTER SPECIFICI FORTI/DEBOLI *)
366 (* ***************************** *)
368 (* funzione ausiliaria per il tipaggio dei setter forti *)
369 ndefinition aux_set_typing ≝ λx:Type.λm:mcu_type.
370 match m with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ]
372 match m with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ].
374 (* funzione ausiliaria per il tipaggio dei setter deboli *)
375 ndefinition aux_set_typing_opt ≝ λx:Type.λm:mcu_type.option
376 (match m with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ]
378 match m with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ]).
380 (* DESCRITTORI ESTERNI ALLA ALU *)
382 (* setter forte della ALU *)
383 ndefinition set_alu ≝
384 λm:mcu_type.λt:memory_impl.λs:any_status m t.λalu'.
385 mk_any_status m t alu' (mem_desc m t s) (chk_desc m t s) (clk_desc m t s).
387 (* setter forte della memoria *)
388 ndefinition set_mem_desc ≝
389 λm:mcu_type.λt:memory_impl.λs:any_status m t.λmem':aux_mem_type t.
390 mk_any_status m t (alu m t s) mem' (chk_desc m t s) (clk_desc m t s).
392 (* setter forte del descrittore *)
393 ndefinition set_chk_desc ≝
394 λm:mcu_type.λt:memory_impl.λs:any_status m t.λchk':aux_chk_type t.
395 mk_any_status m t (alu m t s) (mem_desc m t s) chk' (clk_desc m t s).
397 (* setter forte del clik *)
398 ndefinition set_clk_desc ≝
399 λm:mcu_type.λt:memory_impl.λs:any_status m t.
400 λclk':option (Prod5T byte8 (any_opcode m) (instr_mode) byte8 word16).
401 mk_any_status m t (alu m t s) (mem_desc m t s) (chk_desc m t s) clk'.
405 (* setter specifico HC05 di A *)
406 ndefinition set_acc_8_low_reg_HC05 ≝
410 (indX_low_reg_HC05 alu)
423 (* setter specifico HC08/HCS08 di A *)
424 ndefinition set_acc_8_low_reg_HC08 ≝
428 (indX_low_reg_HC08 alu)
429 (indX_high_reg_HC08 alu)
440 (* setter specifico RS08 di A *)
441 ndefinition set_acc_8_low_reg_RS08 ≝
453 (* setter forte di A *)
454 ndefinition set_acc_8_low_reg ≝
455 λm:mcu_type.λt:memory_impl.λs:any_status m t.λacclow':byte8.
457 (match m return aux_set_typing byte8 with
458 [ HC05 ⇒ set_acc_8_low_reg_HC05
459 | HC08 ⇒ set_acc_8_low_reg_HC08
460 | HCS08 ⇒ set_acc_8_low_reg_HC08
461 | RS08 ⇒ set_acc_8_low_reg_RS08
462 ] (alu m t s) acclow').
466 (* setter specifico HC05 di X *)
467 ndefinition set_indX_8_low_reg_HC05 ≝
468 λalu.λindxlow':byte8.
470 (acc_low_reg_HC05 alu)
484 (* setter specifico HC08/HCS08 di X *)
485 ndefinition set_indX_8_low_reg_HC08 ≝
486 λalu.λindxlow':byte8.
488 (acc_low_reg_HC08 alu)
490 (indX_high_reg_HC08 alu)
501 (* setter forte di X *)
502 ndefinition set_indX_8_low_reg ≝
503 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindxlow':byte8.
504 opt_map … (match m return aux_set_typing_opt byte8 with
505 [ HC05 ⇒ Some ? set_indX_8_low_reg_HC05
506 | HC08 ⇒ Some ? set_indX_8_low_reg_HC08
507 | HCS08 ⇒ Some ? set_indX_8_low_reg_HC08
509 (λf.Some ? (set_alu m t s (f (alu m t s) indxlow'))).
511 (* setter debole di X *)
512 ndefinition setweak_indX_8_low_reg ≝
513 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindxlow':byte8.
514 match set_indX_8_low_reg m t s indxlow' with
515 [ None ⇒ s | Some s' ⇒ s' ].
519 (* setter specifico HC08/HCS08 di H *)
520 ndefinition set_indX_8_high_reg_HC08 ≝
521 λalu.λindxhigh':byte8.
523 (acc_low_reg_HC08 alu)
524 (indX_low_reg_HC08 alu)
536 (* setter forte di H *)
537 ndefinition set_indX_8_high_reg ≝
538 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindxhigh':byte8.
539 opt_map … (match m return aux_set_typing_opt byte8 with
541 | HC08 ⇒ Some ? set_indX_8_high_reg_HC08
542 | HCS08 ⇒ Some ? set_indX_8_high_reg_HC08
544 (λf.Some ? (set_alu m t s (f (alu m t s) indxhigh'))).
546 (* setter debole di H *)
547 ndefinition setweak_indX_8_high_reg ≝
548 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindxhigh':byte8.
549 match set_indX_8_high_reg m t s indxhigh' with
550 [ None ⇒ s | Some s' ⇒ s' ].
554 (* setter specifico HC08/HCS08 di H:X *)
555 ndefinition set_indX_16_reg_HC08 ≝
558 (acc_low_reg_HC08 alu)
571 (* setter forte di H:X *)
572 ndefinition set_indX_16_reg ≝
573 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindx16:word16.
574 opt_map … (match m return aux_set_typing_opt word16 with
576 | HC08 ⇒ Some ? set_indX_16_reg_HC08
577 | HCS08 ⇒ Some ? set_indX_16_reg_HC08
579 (λf.Some ? (set_alu m t s (f (alu m t s) indx16))).
581 (* setter debole di H:X *)
582 ndefinition setweak_indX_16_reg ≝
583 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindx16:word16.
584 match set_indX_16_reg m t s indx16 with
585 [ None ⇒ s | Some s' ⇒ s' ].
589 (* setter specifico HC05 di SP, effettua (SP∧mask)∨fix *)
590 ndefinition set_sp_reg_HC05 ≝
593 (acc_low_reg_HC05 alu)
594 (indX_low_reg_HC05 alu)
595 (or_w16 (and_w16 sp' (sp_mask_HC05 alu)) (sp_fix_HC05 alu))
607 (* setter specifico HC08/HCS08 di SP *)
608 ndefinition set_sp_reg_HC08 ≝
611 (acc_low_reg_HC08 alu)
612 (indX_low_reg_HC08 alu)
613 (indX_high_reg_HC08 alu)
624 (* setter forte di SP *)
625 ndefinition set_sp_reg ≝
626 λm:mcu_type.λt:memory_impl.λs:any_status m t.λsp':word16.
627 opt_map … (match m return aux_set_typing_opt word16 with
628 [ HC05 ⇒ Some ? set_sp_reg_HC05
629 | HC08 ⇒ Some ? set_sp_reg_HC08
630 | HCS08 ⇒ Some ? set_sp_reg_HC08
632 (λf.Some ? (set_alu m t s (f (alu m t s) sp'))).
634 (* setter debole di SP *)
635 ndefinition setweak_sp_reg ≝
636 λm:mcu_type.λt:memory_impl.λs:any_status m t.λsp':word16.
637 match set_sp_reg m t s sp' with
638 [ None ⇒ s | Some s' ⇒ s' ].
642 (* setter specifico HC05 di PC, effettua PC∧mask *)
643 ndefinition set_pc_reg_HC05 ≝
646 (acc_low_reg_HC05 alu)
647 (indX_low_reg_HC05 alu)
651 (and_w16 pc' (pc_mask_HC05 alu))
660 (* setter specifico HC08/HCS08 di PC *)
661 ndefinition set_pc_reg_HC08 ≝
664 (acc_low_reg_HC08 alu)
665 (indX_low_reg_HC08 alu)
666 (indX_high_reg_HC08 alu)
677 (* setter specifico RS08 di PC, effettua PC∧mask *)
678 ndefinition set_pc_reg_RS08 ≝
681 (acc_low_reg_RS08 alu)
682 (and_w16 pc' (pc_mask_RS08 alu))
690 (* setter forte di PC *)
691 ndefinition set_pc_reg ≝
692 λm:mcu_type.λt:memory_impl.λs:any_status m t.λpc':word16.
694 (match m return aux_set_typing word16 with
695 [ HC05 ⇒ set_pc_reg_HC05
696 | HC08 ⇒ set_pc_reg_HC08
697 | HCS08 ⇒ set_pc_reg_HC08
698 | RS08 ⇒ set_pc_reg_RS08
703 (* setter specifico RS08 di SPC, effettua SPC∧mask *)
704 ndefinition set_spc_reg_RS08 ≝
707 (acc_low_reg_RS08 alu)
710 (and_w16 spc' (pc_mask_RS08 alu))
716 (* setter forte di SPC *)
717 ndefinition set_spc_reg ≝
718 λm:mcu_type.λt:memory_impl.λs:any_status m t.λspc':word16.
719 opt_map … (match m return aux_set_typing_opt word16 with
723 | RS08 ⇒ Some ? set_spc_reg_RS08 ])
724 (λf.Some ? (set_alu m t s (f (alu m t s) spc'))).
726 (* setter debole di SPC *)
727 ndefinition setweak_spc_reg ≝
728 λm:mcu_type.λt:memory_impl.λs:any_status m t.λspc':word16.
729 match set_spc_reg m t s spc' with
730 [ None ⇒ s | Some s' ⇒ s' ].
732 (* REGISTRO MEMORY MAPPED X *)
734 (* setter specifico RS08 di memory mapped X *)
735 ndefinition set_x_map_RS08 ≝
738 (acc_low_reg_RS08 alu)
747 (* setter forte di memory mapped X *)
748 ndefinition set_x_map ≝
749 λm:mcu_type.λt:memory_impl.λs:any_status m t.λxm':byte8.
750 opt_map … (match m return aux_set_typing_opt byte8 with
754 | RS08 ⇒ Some ? set_x_map_RS08 ])
755 (λf.Some ? (set_alu m t s (f (alu m t s) xm'))).
757 (* setter debole di memory mapped X *)
758 ndefinition setweak_x_map ≝
759 λm:mcu_type.λt:memory_impl.λs:any_status m t.λxm':byte8.
760 match set_x_map m t s xm' with
761 [ None ⇒ s | Some s' ⇒ s' ].
763 (* REGISTRO MEMORY MAPPED PS *)
765 (* setter specifico RS08 di memory mapped PS *)
766 ndefinition set_ps_map_RS08 ≝
769 (acc_low_reg_RS08 alu)
778 (* setter forte di memory mapped PS *)
779 ndefinition set_ps_map ≝
780 λm:mcu_type.λt:memory_impl.λs:any_status m t.λpsm':byte8.
781 opt_map … (match m return aux_set_typing_opt byte8 with
785 | RS08 ⇒ Some ? set_ps_map_RS08 ])
786 (λf.Some ? (set_alu m t s (f (alu m t s) psm'))).
788 (* setter debole di memory mapped PS *)
789 ndefinition setweak_ps_map ≝
790 λm:mcu_type.λt:memory_impl.λs:any_status m t.λpsm':byte8.
791 match set_ps_map m t s psm' with
792 [ None ⇒ s | Some s' ⇒ s' ].
796 (* setter specifico HC08/HCS08 di V *)
797 ndefinition set_v_flag_HC08 ≝
800 (acc_low_reg_HC08 alu)
801 (indX_low_reg_HC08 alu)
802 (indX_high_reg_HC08 alu)
813 (* setter forte di V *)
814 ndefinition set_v_flag ≝
815 λm:mcu_type.λt:memory_impl.λs:any_status m t.λvfl':bool.
816 opt_map … (match m return aux_set_typing_opt bool with
818 | HC08 ⇒ Some ? set_v_flag_HC08
819 | HCS08 ⇒ Some ? set_v_flag_HC08
821 (λf.Some ? (set_alu m t s (f (alu m t s) vfl'))).
823 (* setter debole di V *)
824 ndefinition setweak_v_flag ≝
825 λm:mcu_type.λt:memory_impl.λs:any_status m t.λvfl':bool.
826 match set_v_flag m t s vfl' with
827 [ None ⇒ s | Some s' ⇒ s' ].
831 (* setter specifico HC05 di H *)
832 ndefinition set_h_flag_HC05 ≝
835 (acc_low_reg_HC05 alu)
836 (indX_low_reg_HC05 alu)
849 (* setter specifico HC08/HCS08 di H *)
850 ndefinition set_h_flag_HC08 ≝
853 (acc_low_reg_HC08 alu)
854 (indX_low_reg_HC08 alu)
855 (indX_high_reg_HC08 alu)
866 (* setter forte di H *)
867 ndefinition set_h_flag ≝
868 λm:mcu_type.λt:memory_impl.λs:any_status m t.λhfl':bool.
869 opt_map … (match m return aux_set_typing_opt bool with
870 [ HC05 ⇒ Some ? set_h_flag_HC05
871 | HC08 ⇒ Some ? set_h_flag_HC08
872 | HCS08 ⇒ Some ? set_h_flag_HC08
874 (λf.Some ? (set_alu m t s (f (alu m t s) hfl'))).
876 (* setter debole di H *)
877 ndefinition setweak_h_flag ≝
878 λm:mcu_type.λt:memory_impl.λs:any_status m t.λhfl':bool.
879 match set_h_flag m t s hfl' with
880 [ None ⇒ s | Some s' ⇒ s' ].
884 (* setter specifico HC05 di I *)
885 ndefinition set_i_flag_HC05 ≝
888 (acc_low_reg_HC05 alu)
889 (indX_low_reg_HC05 alu)
902 (* setter specifico HC08/HCS08 di I *)
903 ndefinition set_i_flag_HC08 ≝
906 (acc_low_reg_HC08 alu)
907 (indX_low_reg_HC08 alu)
908 (indX_high_reg_HC08 alu)
919 (* setter forte di I *)
920 ndefinition set_i_flag ≝
921 λm:mcu_type.λt:memory_impl.λs:any_status m t.λifl':bool.
922 opt_map … (match m return aux_set_typing_opt bool with
923 [ HC05 ⇒ Some ? set_i_flag_HC05
924 | HC08 ⇒ Some ? set_i_flag_HC08
925 | HCS08 ⇒ Some ? set_i_flag_HC08
927 (λf.Some ? (set_alu m t s (f (alu m t s) ifl'))).
929 (* setter debole di I *)
930 ndefinition setweak_i_flag ≝
931 λm:mcu_type.λt:memory_impl.λs:any_status m t.λifl':bool.
932 match set_i_flag m t s ifl' with
933 [ None ⇒ s | Some s' ⇒ s' ].
937 (* setter specifico HC05 di N *)
938 ndefinition set_n_flag_HC05 ≝
941 (acc_low_reg_HC05 alu)
942 (indX_low_reg_HC05 alu)
955 (* setter specifico HC08/HCS08 di N *)
956 ndefinition set_n_flag_HC08 ≝
959 (acc_low_reg_HC08 alu)
960 (indX_low_reg_HC08 alu)
961 (indX_high_reg_HC08 alu)
972 (* setter forte di N *)
973 ndefinition set_n_flag ≝
974 λm:mcu_type.λt:memory_impl.λs:any_status m t.λnfl':bool.
975 opt_map … (match m return aux_set_typing_opt bool with
976 [ HC05 ⇒ Some ? set_n_flag_HC05
977 | HC08 ⇒ Some ? set_n_flag_HC08
978 | HCS08 ⇒ Some ? set_n_flag_HC08
980 (λf.Some ? (set_alu m t s (f (alu m t s) nfl'))).
982 (* setter debole di N *)
983 ndefinition setweak_n_flag ≝
984 λm:mcu_type.λt:memory_impl.λs:any_status m t.λnfl':bool.
985 match set_n_flag m t s nfl' with
986 [ None ⇒ s | Some s' ⇒ s' ].
990 (* setter specifico HC05 di Z *)
991 ndefinition set_z_flag_HC05 ≝
994 (acc_low_reg_HC05 alu)
995 (indX_low_reg_HC05 alu)
1006 (irq_flag_HC05 alu).
1008 (* setter specifico HC08/HCS08 di Z *)
1009 ndefinition set_z_flag_HC08 ≝
1012 (acc_low_reg_HC08 alu)
1013 (indX_low_reg_HC08 alu)
1014 (indX_high_reg_HC08 alu)
1023 (irq_flag_HC08 alu).
1025 (* setter sprcifico RS08 di Z *)
1026 ndefinition set_z_flag_RS08 ≝
1029 (acc_low_reg_RS08 alu)
1038 (* setter forte di Z *)
1039 ndefinition set_z_flag ≝
1040 λm:mcu_type.λt:memory_impl.λs:any_status m t.λzfl':bool.
1042 (match m return aux_set_typing bool with
1043 [ HC05 ⇒ set_z_flag_HC05
1044 | HC08 ⇒ set_z_flag_HC08
1045 | HCS08 ⇒ set_z_flag_HC08
1046 | RS08 ⇒ set_z_flag_RS08
1047 ] (alu m t s) zfl').
1051 (* setter specifico HC05 di C *)
1052 ndefinition set_c_flag_HC05 ≝
1055 (acc_low_reg_HC05 alu)
1056 (indX_low_reg_HC05 alu)
1067 (irq_flag_HC05 alu).
1069 (* setter specifico HC08/HCS08 di C *)
1070 ndefinition set_c_flag_HC08 ≝
1073 (acc_low_reg_HC08 alu)
1074 (indX_low_reg_HC08 alu)
1075 (indX_high_reg_HC08 alu)
1084 (irq_flag_HC08 alu).
1086 (* setter specifico RS08 di C *)
1087 ndefinition set_c_flag_RS08 ≝
1090 (acc_low_reg_RS08 alu)
1099 (* setter forte di C *)
1100 ndefinition set_c_flag ≝
1101 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcfl':bool.
1103 (match m return aux_set_typing bool with
1104 [ HC05 ⇒ set_c_flag_HC05
1105 | HC08 ⇒ set_c_flag_HC08
1106 | HCS08 ⇒ set_c_flag_HC08
1107 | RS08 ⇒ set_c_flag_RS08
1108 ] (alu m t s) cfl').
1112 (* setter specifico HC05 di IRQ *)
1113 ndefinition set_irq_flag_HC05 ≝
1116 (acc_low_reg_HC05 alu)
1117 (indX_low_reg_HC05 alu)
1130 (* setter specifico HC08/HCS08 di IRQ *)
1131 ndefinition set_irq_flag_HC08 ≝
1134 (acc_low_reg_HC08 alu)
1135 (indX_low_reg_HC08 alu)
1136 (indX_high_reg_HC08 alu)
1147 (* setter forte di IRQ *)
1148 ndefinition set_irq_flag ≝
1149 λm:mcu_type.λt:memory_impl.λs:any_status m t.λirqfl':bool.
1150 opt_map … (match m return aux_set_typing_opt bool with
1151 [ HC05 ⇒ Some ? set_irq_flag_HC05
1152 | HC08 ⇒ Some ? set_irq_flag_HC08
1153 | HCS08 ⇒ Some ? set_irq_flag_HC08
1155 (λf.Some ? (set_alu m t s (f (alu m t s) irqfl'))).
1157 (* setter debole di IRQ *)
1158 ndefinition setweak_irq_flag ≝
1159 λm:mcu_type.λt:memory_impl.λs:any_status m t.λirqfl':bool.
1160 match set_irq_flag m t s irqfl' with
1161 [ None ⇒ s | Some s' ⇒ s' ].
1163 (* ***************** *)
1164 (* CONFRONTO FRA ALU *)
1165 (* ***************** *)
1167 (* confronto registro per registro dell'HC05 *)
1168 ndefinition eq_alu_HC05 ≝
1169 λalu1,alu2:alu_HC05.
1171 [ mk_alu_HC05 acclow1 indxlow1 sp1 spm1 spf1 pc1 pcm1 hfl1 ifl1 nfl1 zfl1 cfl1 irqfl1 ⇒
1173 [ mk_alu_HC05 acclow2 indxlow2 sp2 spm2 spf2 pc2 pcm2 hfl2 ifl2 nfl2 zfl2 cfl2 irqfl2 ⇒
1174 (eq_b8 acclow1 acclow2) ⊗
1175 (eq_b8 indxlow1 indxlow2) ⊗
1177 (eq_w16 spm1 spm2) ⊗
1178 (eq_w16 spf1 spf2) ⊗
1180 (eq_w16 pcm1 pcm2) ⊗
1181 (eq_bool hfl1 hfl2) ⊗
1182 (eq_bool ifl1 ifl2) ⊗
1183 (eq_bool nfl1 nfl2) ⊗
1184 (eq_bool zfl1 zfl2) ⊗
1185 (eq_bool cfl1 cfl2) ⊗
1186 (eq_bool irqfl1 irqfl2) ]].
1188 (* confronto registro per registro dell'HC08 *)
1189 ndefinition eq_alu_HC08 ≝
1190 λalu1,alu2:alu_HC08.
1192 [ mk_alu_HC08 acclow1 indxlow1 indxhigh1 sp1 pc1 vfl1 hfl1 ifl1 nfl1 zfl1 cfl1 irqfl1 ⇒
1194 [ mk_alu_HC08 acclow2 indxlow2 indxhigh2 sp2 pc2 vfl2 hfl2 ifl2 nfl2 zfl2 cfl2 irqfl2 ⇒
1195 (eq_b8 acclow1 acclow2) ⊗
1196 (eq_b8 indxlow1 indxlow2) ⊗
1197 (eq_b8 indxhigh1 indxhigh2) ⊗
1200 (eq_bool vfl1 vfl2) ⊗
1201 (eq_bool hfl1 hfl2) ⊗
1202 (eq_bool ifl1 ifl2) ⊗
1203 (eq_bool nfl1 nfl2) ⊗
1204 (eq_bool zfl1 zfl2) ⊗
1205 (eq_bool cfl1 cfl2) ⊗
1206 (eq_bool irqfl1 irqfl2) ]].
1208 (* confronto registro per registro dell'RS08 *)
1209 ndefinition eq_alu_RS08 ≝
1210 λalu1,alu2:alu_RS08.
1212 [ mk_alu_RS08 acclow1 pc1 pcm1 spc1 xm1 psm1 zfl1 cfl1 ⇒
1214 [ mk_alu_RS08 acclow2 pc2 pcm2 spc2 xm2 psm2 zfl2 cfl2 ⇒
1215 (eq_b8 acclow1 acclow2) ⊗
1217 (eq_w16 pcm1 pcm2) ⊗
1218 (eq_w16 spc1 spc2) ⊗
1221 (eq_bool zfl1 zfl2) ⊗
1222 (eq_bool cfl1 cfl2) ]].
1224 (* ******************** *)
1225 (* CONFRONTO FRA STATUS *)
1226 (* ******************** *)
1228 (* confronto di una regione di memoria [addr1 ; ... ; addrn] *)
1229 nlet rec forall_memory_ranged
1231 (chk1:aux_chk_type t) (chk2:aux_chk_type t)
1232 (mem1:aux_mem_type t) (mem2:aux_mem_type t)
1233 (addrl:list word16) on addrl ≝
1234 match addrl return λ_.bool with
1236 | cons hd tl ⇒ (eq_option byte8 (mem_read t mem1 chk1 hd)
1237 (mem_read t mem2 chk2 hd) eq_b8) ⊗
1238 (forall_memory_ranged t chk1 chk2 mem1 mem2 tl)
1241 (* il clk e' option (Prod5T byte8 (any_opcode m) (instr_mode) byte8 word16) *)
1242 ndefinition eq_clk ≝
1243 λm:mcu_type.λc1,c2:option (Prod5T byte8 (any_opcode m) (instr_mode) byte8 word16).
1245 [ None ⇒ match c2 with
1246 [ None ⇒ true | Some _ ⇒ false ]
1247 | Some c1' ⇒ match c2 with
1248 [ None ⇒ false | Some c2' ⇒ (eq_b8 (fst5T … c1') (fst5T … c2')) ⊗
1249 (eq_anyop m (snd5T … c1') (snd5T … c2')) ⊗
1250 (eq_instrmode (thd5T … c1') (thd5T … c2')) ⊗
1251 (eq_b8 (frth5T … c1') (frth5T … c2')) ⊗
1252 (eq_w16 (ffth5T … c1') (ffth5T … c2')) ]
1255 (* generalizzazione del confronto fra stati *)
1256 ndefinition eq_status ≝
1257 λm:mcu_type.λt:memory_impl.λs1,s2:any_status m t.λaddrl:list word16.
1258 match s1 with [ mk_any_status alu1 mem1 chk1 clk1 ⇒
1259 match s2 with [ mk_any_status alu2 mem2 chk2 clk2 ⇒
1261 (* 1) confronto della ALU *)
1262 (match m return λm:mcu_type.
1264 [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ] →
1266 [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ] →
1268 [ HC05 ⇒ eq_alu_HC05 | HC08 ⇒ eq_alu_HC08 | HCS08 ⇒ eq_alu_HC08 | RS08 ⇒ eq_alu_RS08 ]
1271 (* 2) confronto della memoria in [inf,inf+n] *)
1272 (forall_memory_ranged t chk1 chk2 mem1 mem2 addrl) ⊗
1274 (* 3) confronto del clik *)
1275 (eq_clk m clk1 clk2)