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 (* Sviluppo: 2008-2010 *)
21 (* ********************************************************************** *)
23 include "emulator/memory/memory_abs.ma".
24 include "emulator/status/HC05_status.ma".
25 include "emulator/status/HC08_status.ma".
26 include "emulator/status/RS08_status.ma".
27 include "emulator/status/IP2022_status.ma".
28 include "emulator/opcodes/pseudo.ma".
30 (* *********************************** *)
31 (* STATUS INTERNO DEL PROCESSORE (ALU) *)
32 (* *********************************** *)
34 (* descrittore del click = stato di avanzamento dell'esecuzione *)
35 (* 1) None = istruzione eseguita, attesa del fetch *)
36 (* 2) Some cur_clk,pseudo,mode,clks,cur_pc = fetch eseguito *)
37 ndefinition aux_clk_type ≝ λm:mcu_type.Prod5T byte8 (aux_pseudo_type m) (aux_im_type m) byte8 word16.
39 (* tipo processore dipendente dalla mcu, varia solo la ALU *)
40 nrecord any_status (mcu:mcu_type) (t:memory_impl): Type ≝
43 [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08
44 | IP2022 ⇒ alu_IP2022 ];
46 (* descritore della memoria *)
47 mem_desc : aux_mem_type t;
48 (* descrittore del tipo di memoria installata *)
49 chk_desc : aux_chk_type t;
50 (* descrittore del clik *)
51 clk_desc : option (aux_clk_type mcu)
54 (* evitare di mostrare la memoria/descrittore che impalla il visualizzatore *)
55 notation > "{hvbox('Alu' ≝ alu ; break 'Clk' ≝ clk)}" non associative with precedence 80
56 for @{ 'mk_any_status $alu $mem $chk $clk }.
57 interpretation "mk_any_status" 'mk_any_status alu mem chk clk =
58 (mk_any_status alu mem chk clk).
60 (* ******************** *)
61 (* CONFRONTO FRA STATUS *)
62 (* ******************** *)
69 [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08
70 | IP2022 ⇒ alu_IP2022 ] →
72 [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08
73 | IP2022 ⇒ alu_IP2022 ] →
80 | IP2022 ⇒ eq_IP2022_alu
83 (* confronto di una regione di memoria [addr1 ; ... ; addrn] *)
84 nlet rec forall_memory_ranged
86 (chk1:aux_chk_type t) (chk2:aux_chk_type t)
87 (mem1:aux_mem_type t) (mem2:aux_mem_type t)
88 (addrl:list word32) on addrl ≝
89 match addrl return λ_.bool with
91 | cons hd tl ⇒ (eq_option byte8 eq_b8 (mem_read t mem1 chk1 hd)
92 (mem_read t mem2 chk2 hd)) ⊗
93 (forall_memory_ranged t chk1 chk2 mem1 mem2 tl)
96 ndefinition eq_clk ≝ λm.eq_option … (eq_quintuple … eq_b8 (eq_pseudo m) (eq_im m) eq_b8 eq_w16).
98 (* generalizzazione del confronto fra stati *)
99 ndefinition eq_anystatus ≝
100 λm:mcu_type.λt:memory_impl.λs1,s2:any_status m t.λaddrl:list word32.
101 (* 1) confronto della ALU *)
102 (eq_alu m (alu m t s1) (alu m t s2)) ⊗
103 (* 2) confronto della memoria in [inf,inf+n] *)
104 (forall_memory_ranged t (chk_desc m t s1) (chk_desc m t s2)
105 (mem_desc m t s1) (mem_desc m t s2) addrl) ⊗
106 (* 3) confronto del clik *)
107 (eq_clk m (clk_desc m t s1) (clk_desc m t s2)).