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,clks,pseudo,mode,cur_pc = fetch eseguito *)
37 ndefinition aux_clk_type ≝ λm:mcu_type.Prod5T nat nat (aux_pseudo_type m) (aux_im_type m) word16.
39 nlemma clk_is_comparable : mcu_type → comparable.
40 #m; @ (aux_clk_type m)
41 ##[ napply (zeroc (quintuple_is_comparable nat_is_comparable nat_is_comparable (pseudo_is_comparable m) (im_is_comparable m) word16_is_comparable))
42 ##| napply (forallc (quintuple_is_comparable nat_is_comparable nat_is_comparable (pseudo_is_comparable m) (im_is_comparable m) word16_is_comparable))
43 ##| napply (eqc (quintuple_is_comparable nat_is_comparable nat_is_comparable (pseudo_is_comparable m) (im_is_comparable m) word16_is_comparable))
44 ##| napply (eqc_to_eq (quintuple_is_comparable nat_is_comparable nat_is_comparable (pseudo_is_comparable m) (im_is_comparable m) word16_is_comparable))
45 ##| napply (eq_to_eqc (quintuple_is_comparable nat_is_comparable nat_is_comparable (pseudo_is_comparable m) (im_is_comparable m) word16_is_comparable))
46 ##| napply (neqc_to_neq (quintuple_is_comparable nat_is_comparable nat_is_comparable (pseudo_is_comparable m) (im_is_comparable m) word16_is_comparable))
47 ##| napply (neq_to_neqc (quintuple_is_comparable nat_is_comparable nat_is_comparable (pseudo_is_comparable m) (im_is_comparable m) word16_is_comparable))
48 ##| napply (decidable_c (quintuple_is_comparable nat_is_comparable nat_is_comparable (pseudo_is_comparable m) (im_is_comparable m) word16_is_comparable))
49 ##| napply (symmetric_eqc (quintuple_is_comparable nat_is_comparable nat_is_comparable (pseudo_is_comparable m) (im_is_comparable m) word16_is_comparable))
53 unification hint 0 ≔ M:mcu_type ⊢ carr (clk_is_comparable M) ≡ aux_clk_type M.
55 (* descritture della alu *)
56 ndefinition aux_alu_type ≝
65 nlemma alu_is_comparable : mcu_type → comparable.
66 #m; @ (aux_alu_type m)
68 ##[ napply (zeroc aluHC05_is_comparable)
69 ##| napply (zeroc aluHC08_is_comparable)
70 ##| napply (zeroc aluHC08_is_comparable)
71 ##| napply (zeroc aluRS08_is_comparable)
72 ##| napply (zeroc aluIP2022_is_comparable) ##]
74 ##[ napply (forallc aluHC05_is_comparable)
75 ##| napply (forallc aluHC08_is_comparable)
76 ##| napply (forallc aluHC08_is_comparable)
77 ##| napply (forallc aluRS08_is_comparable)
78 ##| napply (forallc aluIP2022_is_comparable) ##]
80 ##[ napply (eqc aluHC05_is_comparable)
81 ##| napply (eqc aluHC08_is_comparable)
82 ##| napply (eqc aluHC08_is_comparable)
83 ##| napply (eqc aluRS08_is_comparable)
84 ##| napply (eqc aluIP2022_is_comparable) ##]
86 ##[ napply (eqc_to_eq aluHC05_is_comparable)
87 ##| napply (eqc_to_eq aluHC08_is_comparable)
88 ##| napply (eqc_to_eq aluHC08_is_comparable)
89 ##| napply (eqc_to_eq aluRS08_is_comparable)
90 ##| napply (eqc_to_eq aluIP2022_is_comparable) ##]
92 ##[ napply (eq_to_eqc aluHC05_is_comparable)
93 ##| napply (eq_to_eqc aluHC08_is_comparable)
94 ##| napply (eq_to_eqc aluHC08_is_comparable)
95 ##| napply (eq_to_eqc aluRS08_is_comparable)
96 ##| napply (eq_to_eqc aluIP2022_is_comparable) ##]
98 ##[ napply (neqc_to_neq aluHC05_is_comparable)
99 ##| napply (neqc_to_neq aluHC08_is_comparable)
100 ##| napply (neqc_to_neq aluHC08_is_comparable)
101 ##| napply (neqc_to_neq aluRS08_is_comparable)
102 ##| napply (neqc_to_neq aluIP2022_is_comparable) ##]
104 ##[ napply (neq_to_neqc aluHC05_is_comparable)
105 ##| napply (neq_to_neqc aluHC08_is_comparable)
106 ##| napply (neq_to_neqc aluHC08_is_comparable)
107 ##| napply (neq_to_neqc aluRS08_is_comparable)
108 ##| napply (neq_to_neqc aluIP2022_is_comparable) ##]
110 ##[ napply (decidable_c aluHC05_is_comparable)
111 ##| napply (decidable_c aluHC08_is_comparable)
112 ##| napply (decidable_c aluHC08_is_comparable)
113 ##| napply (decidable_c aluRS08_is_comparable)
114 ##| napply (decidable_c aluIP2022_is_comparable) ##]
116 ##[ napply (symmetric_eqc aluHC05_is_comparable)
117 ##| napply (symmetric_eqc aluHC08_is_comparable)
118 ##| napply (symmetric_eqc aluHC08_is_comparable)
119 ##| napply (symmetric_eqc aluRS08_is_comparable)
120 ##| napply (symmetric_eqc aluIP2022_is_comparable) ##]
124 unification hint 0 ≔ M:mcu_type ⊢ carr (alu_is_comparable M) ≡ aux_alu_type M.
126 (* tipo processore dipendente dalla mcu, varia solo la ALU *)
127 nrecord any_status (mcu:mcu_type) (t:memory_impl): Type ≝
129 (* descrittore della alu *)
130 alu : aux_alu_type mcu;
131 (* descritore della memoria *)
132 mem_desc : aux_mem_type t;
133 (* descrittore del tipo di memoria installata *)
134 chk_desc : aux_chk_type t;
135 (* descrittore del clik *)
136 clk_desc : option (aux_clk_type mcu)
139 (* evitare di mostrare la memoria/descrittore che impalla il visualizzatore *)
140 notation > "{hvbox('Alu' ≝ alu ; break 'Clk' ≝ clk)}" non associative with precedence 80
141 for @{ 'mk_any_status $alu $mem $chk $clk }.
142 interpretation "mk_any_status" 'mk_any_status alu mem chk clk =
143 (mk_any_status alu mem chk clk).
145 (* ******************** *)
146 (* CONFRONTO FRA STATUS *)
147 (* ******************** *)
149 ndefinition eq_anystatus ≝
150 λm,t.λs1,s2:any_status m t.
151 (eqc ? (alu … s1) (alu … s2)) ⊗
152 (eqc ? (mem_desc … s1) (mem_desc … s2)) ⊗
153 (eqc ? (chk_desc … s1) (chk_desc … s2)) ⊗
154 (eqc ? (clk_desc … s1) (clk_desc … s2)).
156 ndefinition forall_anystatus ≝ λm,t.λP:any_status m t → bool.
157 forallc ? (λr1.forallc ? (λr2.
158 forallc ? (λr3.forallc ? (λr4.
159 P (mk_any_status m t r1 r2 r3 r4))))).
161 (* confronto di una regione di memoria [addr1 ; ... ; addrn] *)
162 nlet rec forall_memory_ranged
164 (chk1:aux_chk_type t) (chk2:aux_chk_type t)
165 (mem1:aux_mem_type t) (mem2:aux_mem_type t)
166 (sel:oct) (addrl:list word16) on addrl ≝
167 match addrl return λ_.bool with
169 | cons hd tl ⇒ (eqc ? (mem_read t mem1 chk1 sel hd) (mem_read t mem2 chk2 sel hd)) ⊗
170 (forall_memory_ranged t chk1 chk2 mem1 mem2 sel tl)