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 (mk_alu_HC05 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 (mk_alu_HC08 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 (mk_alu_RS08 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 (mk_any_status 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'.
401 mk_any_status m t alu' (get_mem_desc m t s) (get_chk_desc m t s) (get_clk_desc m t s).
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.
406 mk_any_status m t (get_alu m t s) mem' (get_chk_desc m t s) (get_clk_desc m t s).
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.
411 mk_any_status m t (get_alu m t s) (get_mem_desc m t s) chk' (get_clk_desc m t s).
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).
417 mk_any_status m t (get_alu m t s) (get_mem_desc m t s) (get_chk_desc m t s) clk'.
421 (* setter specifico HC05 di A *)
422 definition set_acc_8_low_reg_HC05 ≝
426 (indX_low_reg_HC05 alu)
439 (* setter specifico HC08/HCS08 di A *)
440 definition set_acc_8_low_reg_HC08 ≝
444 (indX_low_reg_HC08 alu)
445 (indX_high_reg_HC08 alu)
456 (* setter specifico RS08 di A *)
457 definition set_acc_8_low_reg_RS08 ≝
469 (* setter forte di A *)
470 definition set_acc_8_low_reg ≝
471 λm:mcu_type.λt:memory_impl.λs:any_status m t.λacclow':byte8.
473 (match m return aux_set_typing byte8 with
474 [ HC05 ⇒ set_acc_8_low_reg_HC05
475 | HC08 ⇒ set_acc_8_low_reg_HC08
476 | HCS08 ⇒ set_acc_8_low_reg_HC08
477 | RS08 ⇒ set_acc_8_low_reg_RS08
478 ] (alu m t s) acclow').
482 (* setter specifico HC05 di X *)
483 definition set_indX_8_low_reg_HC05 ≝
484 λalu.λindxlow':byte8.
486 (acc_low_reg_HC05 alu)
500 (* setter specifico HC08/HCS08 di X *)
501 definition set_indX_8_low_reg_HC08 ≝
502 λalu.λindxlow':byte8.
504 (acc_low_reg_HC08 alu)
506 (indX_high_reg_HC08 alu)
517 (* setter forte di X *)
518 definition set_indX_8_low_reg ≝
519 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindxlow':byte8.
520 opt_map ?? (match m return aux_set_typing_opt byte8 with
521 [ HC05 ⇒ Some ? set_indX_8_low_reg_HC05
522 | HC08 ⇒ Some ? set_indX_8_low_reg_HC08
523 | HCS08 ⇒ Some ? set_indX_8_low_reg_HC08
525 (λf.Some ? (set_alu m t s (f (alu m t s) indxlow'))).
527 (* setter debole di X *)
528 definition setweak_indX_8_low_reg ≝
529 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindxlow':byte8.
530 match set_indX_8_low_reg m t s indxlow' with
531 [ None ⇒ s | Some s' ⇒ s' ].
535 (* setter specifico HC08/HCS08 di H *)
536 definition set_indX_8_high_reg_HC08 ≝
537 λalu.λindxhigh':byte8.
539 (acc_low_reg_HC08 alu)
540 (indX_low_reg_HC08 alu)
552 (* setter forte di H *)
553 definition set_indX_8_high_reg ≝
554 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindxhigh':byte8.
555 opt_map ?? (match m return aux_set_typing_opt byte8 with
557 | HC08 ⇒ Some ? set_indX_8_high_reg_HC08
558 | HCS08 ⇒ Some ? set_indX_8_high_reg_HC08
560 (λf.Some ? (set_alu m t s (f (alu m t s) indxhigh'))).
562 (* setter debole di H *)
563 definition setweak_indX_8_high_reg ≝
564 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindxhigh':byte8.
565 match set_indX_8_high_reg m t s indxhigh' with
566 [ None ⇒ s | Some s' ⇒ s' ].
570 (* setter specifico HC08/HCS08 di H:X *)
571 definition set_indX_16_reg_HC08 ≝
574 (acc_low_reg_HC08 alu)
587 (* setter forte di H:X *)
588 definition set_indX_16_reg ≝
589 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindx16:word16.
590 opt_map ?? (match m return aux_set_typing_opt word16 with
592 | HC08 ⇒ Some ? set_indX_16_reg_HC08
593 | HCS08 ⇒ Some ? set_indX_16_reg_HC08
595 (λf.Some ? (set_alu m t s (f (alu m t s) indx16))).
597 (* setter debole di H:X *)
598 definition setweak_indX_16_reg ≝
599 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindx16:word16.
600 match set_indX_16_reg m t s indx16 with
601 [ None ⇒ s | Some s' ⇒ s' ].
605 (* setter specifico HC05 di SP, effettua (SP∧mask)∨fix *)
606 definition set_sp_reg_HC05 ≝
609 (acc_low_reg_HC05 alu)
610 (indX_low_reg_HC05 alu)
611 (or_w16 (and_w16 sp' (sp_mask_HC05 alu)) (sp_fix_HC05 alu))
623 (* setter specifico HC08/HCS08 di SP *)
624 definition set_sp_reg_HC08 ≝
627 (acc_low_reg_HC08 alu)
628 (indX_low_reg_HC08 alu)
629 (indX_high_reg_HC08 alu)
640 (* setter forte di SP *)
641 definition set_sp_reg ≝
642 λm:mcu_type.λt:memory_impl.λs:any_status m t.λsp':word16.
643 opt_map ?? (match m return aux_set_typing_opt word16 with
644 [ HC05 ⇒ Some ? set_sp_reg_HC05
645 | HC08 ⇒ Some ? set_sp_reg_HC08
646 | HCS08 ⇒ Some ? set_sp_reg_HC08
648 (λf.Some ? (set_alu m t s (f (alu m t s) sp'))).
650 (* setter debole di SP *)
651 definition setweak_sp_reg ≝
652 λm:mcu_type.λt:memory_impl.λs:any_status m t.λsp':word16.
653 match set_sp_reg m t s sp' with
654 [ None ⇒ s | Some s' ⇒ s' ].
658 (* setter specifico HC05 di PC, effettua PC∧mask *)
659 definition set_pc_reg_HC05 ≝
662 (acc_low_reg_HC05 alu)
663 (indX_low_reg_HC05 alu)
667 (and_w16 pc' (pc_mask_HC05 alu))
676 (* setter specifico HC08/HCS08 di PC *)
677 definition set_pc_reg_HC08 ≝
680 (acc_low_reg_HC08 alu)
681 (indX_low_reg_HC08 alu)
682 (indX_high_reg_HC08 alu)
693 (* setter specifico RS08 di PC, effettua PC∧mask *)
694 definition set_pc_reg_RS08 ≝
697 (acc_low_reg_RS08 alu)
698 (and_w16 pc' (pc_mask_RS08 alu))
706 (* setter forte di PC *)
707 definition set_pc_reg ≝
708 λm:mcu_type.λt:memory_impl.λs:any_status m t.λpc':word16.
710 (match m return aux_set_typing word16 with
711 [ HC05 ⇒ set_pc_reg_HC05
712 | HC08 ⇒ set_pc_reg_HC08
713 | HCS08 ⇒ set_pc_reg_HC08
714 | RS08 ⇒ set_pc_reg_RS08
719 (* setter specifico RS08 di SPC, effettua SPC∧mask *)
720 definition set_spc_reg_RS08 ≝
723 (acc_low_reg_RS08 alu)
726 (and_w16 spc' (pc_mask_RS08 alu))
732 (* setter forte di SPC *)
733 definition set_spc_reg ≝
734 λm:mcu_type.λt:memory_impl.λs:any_status m t.λspc':word16.
735 opt_map ?? (match m return aux_set_typing_opt word16 with
739 | RS08 ⇒ Some ? set_spc_reg_RS08 ])
740 (λf.Some ? (set_alu m t s (f (alu m t s) spc'))).
742 (* setter debole di SPC *)
743 definition setweak_spc_reg ≝
744 λm:mcu_type.λt:memory_impl.λs:any_status m t.λspc':word16.
745 match set_spc_reg m t s spc' with
746 [ None ⇒ s | Some s' ⇒ s' ].
748 (* REGISTRO MEMORY MAPPED X *)
750 (* setter specifico RS08 di memory mapped X *)
751 definition set_x_map_RS08 ≝
754 (acc_low_reg_RS08 alu)
763 (* setter forte di memory mapped X *)
764 definition set_x_map ≝
765 λm:mcu_type.λt:memory_impl.λs:any_status m t.λxm':byte8.
766 opt_map ?? (match m return aux_set_typing_opt byte8 with
770 | RS08 ⇒ Some ? set_x_map_RS08 ])
771 (λf.Some ? (set_alu m t s (f (alu m t s) xm'))).
773 (* setter debole di memory mapped X *)
774 definition setweak_x_map ≝
775 λm:mcu_type.λt:memory_impl.λs:any_status m t.λxm':byte8.
776 match set_x_map m t s xm' with
777 [ None ⇒ s | Some s' ⇒ s' ].
779 (* REGISTRO MEMORY MAPPED PS *)
781 (* setter specifico RS08 di memory mapped PS *)
782 definition set_ps_map_RS08 ≝
785 (acc_low_reg_RS08 alu)
794 (* setter forte di memory mapped PS *)
795 definition set_ps_map ≝
796 λm:mcu_type.λt:memory_impl.λs:any_status m t.λpsm':byte8.
797 opt_map ?? (match m return aux_set_typing_opt byte8 with
801 | RS08 ⇒ Some ? set_ps_map_RS08 ])
802 (λf.Some ? (set_alu m t s (f (alu m t s) psm'))).
804 (* setter debole di memory mapped PS *)
805 definition setweak_ps_map ≝
806 λm:mcu_type.λt:memory_impl.λs:any_status m t.λpsm':byte8.
807 match set_ps_map m t s psm' with
808 [ None ⇒ s | Some s' ⇒ s' ].
812 (* setter specifico HC08/HCS08 di V *)
813 definition set_v_flag_HC08 ≝
816 (acc_low_reg_HC08 alu)
817 (indX_low_reg_HC08 alu)
818 (indX_high_reg_HC08 alu)
829 (* setter forte di V *)
830 definition set_v_flag ≝
831 λm:mcu_type.λt:memory_impl.λs:any_status m t.λvfl':bool.
832 opt_map ?? (match m return aux_set_typing_opt bool with
834 | HC08 ⇒ Some ? set_v_flag_HC08
835 | HCS08 ⇒ Some ? set_v_flag_HC08
837 (λf.Some ? (set_alu m t s (f (alu m t s) vfl'))).
839 (* setter debole di V *)
840 definition setweak_v_flag ≝
841 λm:mcu_type.λt:memory_impl.λs:any_status m t.λvfl':bool.
842 match set_v_flag m t s vfl' with
843 [ None ⇒ s | Some s' ⇒ s' ].
847 (* setter specifico HC05 di H *)
848 definition set_h_flag_HC05 ≝
851 (acc_low_reg_HC05 alu)
852 (indX_low_reg_HC05 alu)
865 (* setter specifico HC08/HCS08 di H *)
866 definition set_h_flag_HC08 ≝
869 (acc_low_reg_HC08 alu)
870 (indX_low_reg_HC08 alu)
871 (indX_high_reg_HC08 alu)
882 (* setter forte di H *)
883 definition set_h_flag ≝
884 λm:mcu_type.λt:memory_impl.λs:any_status m t.λhfl':bool.
885 opt_map ?? (match m return aux_set_typing_opt bool with
886 [ HC05 ⇒ Some ? set_h_flag_HC05
887 | HC08 ⇒ Some ? set_h_flag_HC08
888 | HCS08 ⇒ Some ? set_h_flag_HC08
890 (λf.Some ? (set_alu m t s (f (alu m t s) hfl'))).
892 (* setter debole di H *)
893 definition setweak_h_flag ≝
894 λm:mcu_type.λt:memory_impl.λs:any_status m t.λhfl':bool.
895 match set_h_flag m t s hfl' with
896 [ None ⇒ s | Some s' ⇒ s' ].
900 (* setter specifico HC05 di I *)
901 definition set_i_flag_HC05 ≝
904 (acc_low_reg_HC05 alu)
905 (indX_low_reg_HC05 alu)
918 (* setter specifico HC08/HCS08 di I *)
919 definition set_i_flag_HC08 ≝
922 (acc_low_reg_HC08 alu)
923 (indX_low_reg_HC08 alu)
924 (indX_high_reg_HC08 alu)
935 (* setter forte di I *)
936 definition set_i_flag ≝
937 λm:mcu_type.λt:memory_impl.λs:any_status m t.λifl':bool.
938 opt_map ?? (match m return aux_set_typing_opt bool with
939 [ HC05 ⇒ Some ? set_i_flag_HC05
940 | HC08 ⇒ Some ? set_i_flag_HC08
941 | HCS08 ⇒ Some ? set_i_flag_HC08
943 (λf.Some ? (set_alu m t s (f (alu m t s) ifl'))).
945 (* setter debole di I *)
946 definition setweak_i_flag ≝
947 λm:mcu_type.λt:memory_impl.λs:any_status m t.λifl':bool.
948 match set_i_flag m t s ifl' with
949 [ None ⇒ s | Some s' ⇒ s' ].
953 (* setter specifico HC05 di N *)
954 definition set_n_flag_HC05 ≝
957 (acc_low_reg_HC05 alu)
958 (indX_low_reg_HC05 alu)
971 (* setter specifico HC08/HCS08 di N *)
972 definition set_n_flag_HC08 ≝
975 (acc_low_reg_HC08 alu)
976 (indX_low_reg_HC08 alu)
977 (indX_high_reg_HC08 alu)
988 (* setter forte di N *)
989 definition set_n_flag ≝
990 λm:mcu_type.λt:memory_impl.λs:any_status m t.λnfl':bool.
991 opt_map ?? (match m return aux_set_typing_opt bool with
992 [ HC05 ⇒ Some ? set_n_flag_HC05
993 | HC08 ⇒ Some ? set_n_flag_HC08
994 | HCS08 ⇒ Some ? set_n_flag_HC08
996 (λf.Some ? (set_alu m t s (f (alu m t s) nfl'))).
998 (* setter debole di N *)
999 definition setweak_n_flag ≝
1000 λm:mcu_type.λt:memory_impl.λs:any_status m t.λnfl':bool.
1001 match set_n_flag m t s nfl' with
1002 [ None ⇒ s | Some s' ⇒ s' ].
1006 (* setter specifico HC05 di Z *)
1007 definition set_z_flag_HC05 ≝
1010 (acc_low_reg_HC05 alu)
1011 (indX_low_reg_HC05 alu)
1022 (irq_flag_HC05 alu).
1024 (* setter specifico HC08/HCS08 di Z *)
1025 definition set_z_flag_HC08 ≝
1028 (acc_low_reg_HC08 alu)
1029 (indX_low_reg_HC08 alu)
1030 (indX_high_reg_HC08 alu)
1039 (irq_flag_HC08 alu).
1041 (* setter sprcifico RS08 di Z *)
1042 definition set_z_flag_RS08 ≝
1045 (acc_low_reg_RS08 alu)
1054 (* setter forte di Z *)
1055 definition set_z_flag ≝
1056 λm:mcu_type.λt:memory_impl.λs:any_status m t.λzfl':bool.
1058 (match m return aux_set_typing bool with
1059 [ HC05 ⇒ set_z_flag_HC05
1060 | HC08 ⇒ set_z_flag_HC08
1061 | HCS08 ⇒ set_z_flag_HC08
1062 | RS08 ⇒ set_z_flag_RS08
1063 ] (alu m t s) zfl').
1067 (* setter specifico HC05 di C *)
1068 definition set_c_flag_HC05 ≝
1071 (acc_low_reg_HC05 alu)
1072 (indX_low_reg_HC05 alu)
1083 (irq_flag_HC05 alu).
1085 (* setter specifico HC08/HCS08 di C *)
1086 definition set_c_flag_HC08 ≝
1089 (acc_low_reg_HC08 alu)
1090 (indX_low_reg_HC08 alu)
1091 (indX_high_reg_HC08 alu)
1100 (irq_flag_HC08 alu).
1102 (* setter specifico RS08 di C *)
1103 definition set_c_flag_RS08 ≝
1106 (acc_low_reg_RS08 alu)
1115 (* setter forte di C *)
1116 definition set_c_flag ≝
1117 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcfl':bool.
1119 (match m return aux_set_typing bool with
1120 [ HC05 ⇒ set_c_flag_HC05
1121 | HC08 ⇒ set_c_flag_HC08
1122 | HCS08 ⇒ set_c_flag_HC08
1123 | RS08 ⇒ set_c_flag_RS08
1124 ] (alu m t s) cfl').
1128 (* setter specifico HC05 di IRQ *)
1129 definition set_irq_flag_HC05 ≝
1132 (acc_low_reg_HC05 alu)
1133 (indX_low_reg_HC05 alu)
1146 (* setter specifico HC08/HCS08 di IRQ *)
1147 definition set_irq_flag_HC08 ≝
1150 (acc_low_reg_HC08 alu)
1151 (indX_low_reg_HC08 alu)
1152 (indX_high_reg_HC08 alu)
1163 (* setter forte di IRQ *)
1164 definition set_irq_flag ≝
1165 λm:mcu_type.λt:memory_impl.λs:any_status m t.λirqfl':bool.
1166 opt_map ?? (match m return aux_set_typing_opt bool with
1167 [ HC05 ⇒ Some ? set_irq_flag_HC05
1168 | HC08 ⇒ Some ? set_irq_flag_HC08
1169 | HCS08 ⇒ Some ? set_irq_flag_HC08
1171 (λf.Some ? (set_alu m t s (f (alu m t s) irqfl'))).
1173 (* setter debole di IRQ *)
1174 definition setweak_irq_flag ≝
1175 λm:mcu_type.λt:memory_impl.λs:any_status m t.λirqfl':bool.
1176 match set_irq_flag m t s irqfl' with
1177 [ None ⇒ s | Some s' ⇒ s' ].
1179 (* ***************** *)
1180 (* CONFRONTO FRA ALU *)
1181 (* ***************** *)
1183 (* confronto registro per registro dell'HC05 *)
1184 definition eq_alu_HC05 ≝
1185 λalu1,alu2:alu_HC05.
1187 [ mk_alu_HC05 acclow1 indxlow1 sp1 spm1 spf1 pc1 pcm1 hfl1 ifl1 nfl1 zfl1 cfl1 irqfl1 ⇒
1189 [ mk_alu_HC05 acclow2 indxlow2 sp2 spm2 spf2 pc2 pcm2 hfl2 ifl2 nfl2 zfl2 cfl2 irqfl2 ⇒
1190 (eq_b8 acclow1 acclow2) ⊗
1191 (eq_b8 indxlow1 indxlow2) ⊗
1193 (eq_w16 spm1 spm2) ⊗
1194 (eq_w16 spf1 spf2) ⊗
1196 (eq_w16 pcm1 pcm2) ⊗
1197 (eq_bool hfl1 hfl2) ⊗
1198 (eq_bool ifl1 ifl2) ⊗
1199 (eq_bool nfl1 nfl2) ⊗
1200 (eq_bool zfl1 zfl2) ⊗
1201 (eq_bool cfl1 cfl2) ⊗
1202 (eq_bool irqfl1 irqfl2) ]].
1204 (* confronto registro per registro dell'HC08 *)
1205 definition eq_alu_HC08 ≝
1206 λalu1,alu2:alu_HC08.
1208 [ mk_alu_HC08 acclow1 indxlow1 indxhigh1 sp1 pc1 vfl1 hfl1 ifl1 nfl1 zfl1 cfl1 irqfl1 ⇒
1210 [ mk_alu_HC08 acclow2 indxlow2 indxhigh2 sp2 pc2 vfl2 hfl2 ifl2 nfl2 zfl2 cfl2 irqfl2 ⇒
1211 (eq_b8 acclow1 acclow2) ⊗
1212 (eq_b8 indxlow1 indxlow2) ⊗
1213 (eq_b8 indxhigh1 indxhigh2) ⊗
1216 (eq_bool vfl1 vfl2) ⊗
1217 (eq_bool hfl1 hfl2) ⊗
1218 (eq_bool ifl1 ifl2) ⊗
1219 (eq_bool nfl1 nfl2) ⊗
1220 (eq_bool zfl1 zfl2) ⊗
1221 (eq_bool cfl1 cfl2) ⊗
1222 (eq_bool irqfl1 irqfl2) ]].
1224 (* confronto registro per registro dell'RS08 *)
1225 definition eq_alu_RS08 ≝
1226 λalu1,alu2:alu_RS08.
1228 [ mk_alu_RS08 acclow1 pc1 pcm1 spc1 xm1 psm1 zfl1 cfl1 ⇒
1230 [ mk_alu_RS08 acclow2 pc2 pcm2 spc2 xm2 psm2 zfl2 cfl2 ⇒
1231 (eq_b8 acclow1 acclow2) ⊗
1233 (eq_w16 pcm1 pcm2) ⊗
1234 (eq_w16 spc1 spc2) ⊗
1237 (eq_bool zfl1 zfl2) ⊗
1238 (eq_bool cfl1 cfl2) ]].
1240 (* ******************** *)
1241 (* CONFRONTO FRA STATUS *)
1242 (* ******************** *)
1244 (* la lettura da memoria ritorna un option byte8, quindi bisogna poterli confrontare *)
1245 definition eq_b8_opt ≝
1246 λb1,b2:option byte8.
1248 [ None ⇒ match b2 with
1249 [ None ⇒ true | Some _ ⇒ false ]
1250 | Some b1' ⇒ match b2 with
1251 [ None ⇒ false | Some b2' ⇒ eq_b8 b1' b2' ]
1254 (* confronto di una regione di memoria [inf,inf+n] *)
1255 let rec forall_memory_ranged
1257 (chk1:aux_chk_type t) (chk2:aux_chk_type t)
1258 (mem1:aux_mem_type t) (mem2:aux_mem_type t)
1259 (inf:word16) (n:nat) on n ≝
1260 match n return λ_.bool with
1261 [ O ⇒ eq_b8_opt (mem_read t mem1 chk1 inf) (mem_read t mem2 chk2 inf)
1262 | S n' ⇒ (eq_b8_opt (mem_read t mem1 chk1 (plus_w16nc inf (word16_of_nat n)))
1263 (mem_read t mem2 chk2 (plus_w16nc inf (word16_of_nat n)))) ⊗
1264 (forall_memory_ranged t chk1 chk2 mem1 mem2 inf n')
1267 (* il clk e' option (Prod5T byte8 (any_opcode m) (instr_mode) byte8 word16) *)
1269 λm:mcu_type.λc1,c2:option (Prod5T byte8 (any_opcode m) (instr_mode) byte8 word16).
1271 [ None ⇒ match c2 with
1272 [ None ⇒ true | Some _ ⇒ false ]
1273 | Some c1' ⇒ match c2 with
1274 [ None ⇒ false | Some c2' ⇒ (eq_b8 (fst5T ????? c1') (fst5T ????? c2')) ⊗
1275 (eqop m (snd5T ????? c1') (snd5T ????? c2')) ⊗
1276 (eqim (thd5T ????? c1') (thd5T ????? c2')) ⊗
1277 (eq_b8 (frth5T ????? c1') (frth5T ????? c2')) ⊗
1278 (eq_w16 (ffth5T ????? c1') (ffth5T ????? c2')) ]
1281 (* generalizzazione del confronto fra stati *)
1282 definition eq_status ≝
1283 λm:mcu_type.λt:memory_impl.λs1,s2:any_status m t.λinf:word16.λn:nat.
1284 match s1 with [ mk_any_status alu1 mem1 chk1 clk1 ⇒
1285 match s2 with [ mk_any_status alu2 mem2 chk2 clk2 ⇒
1287 (* 1) confronto della ALU *)
1288 (match m return λm:mcu_type.
1290 [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ] →
1292 [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ] →
1294 [ HC05 ⇒ eq_alu_HC05 | HC08 ⇒ eq_alu_HC08 | HCS08 ⇒ eq_alu_HC08 | RS08 ⇒ eq_alu_RS08 ]
1297 (* 2) confronto della memoria in [inf,inf+n] *)
1298 (forall_memory_ranged t chk1 chk2 mem1 mem2 inf n) ⊗
1300 (* 3) confronto del clik *)
1301 (eq_clk m clk1 clk2)
1304 (* assioma da applicare per l'uguaglianza degli stati *)
1305 axiom eq_status_axiom :
1306 ∀inf:word16.∀n:nat.∀m:mcu_type.∀t:memory_impl.∀s1,s2:any_status m t.
1307 (eq_status m t s1 s2 inf n = true) →