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".
28 include "freescale/opcode_base.ma".
29 include "freescale/prod.ma".
31 (* *********************************** *)
32 (* STATUS INTERNO DEL PROCESSORE (ALU) *)
33 (* *********************************** *)
36 nrecord alu_HC05: Type ≝
38 (* A: registo accumulatore *)
39 acc_low_reg_HC05 : byte8;
40 (* X: registro indice *)
41 indX_low_reg_HC05 : byte8;
42 (* SP: registo stack pointer *)
44 (* modificatori di SP: per esempio e' definito come 0000000011xxxxxxb *)
45 (* la logica della sua costruzione e' quindi (SP∧mask)∨fix *)
46 (* totalmente racchiusa nella ALU, bastera' fare get(set(SP)) *)
47 sp_mask_HC05 : word16;
49 (* PC: registro program counter *)
51 (* modificatore di PC: per esempio e' definito come 00xxxxxxxxxxxxxxb *)
52 (* la logica della sua costruzione e' quindi (PC∧mask) *)
53 (* totalmente racchiusa nella ALU, bastera' fare get(set(PC)) *)
54 pc_mask_HC05 : word16;
56 (* H: flag semi-carry (somma nibble basso) *)
58 (* I: flag mascheramento degli interrupt mascherabili: 1=mascherati *)
60 (* N: flag segno/negativita' *)
67 (* IRQ: flag che simula il pin esterno IRQ *)
71 ndefinition alu_HC05_ind :
72 ΠP:alu_HC05 → Prop.(Πb,b1,w,w1,w2,w3,w4,b2,b3,b4,b5,b6,b7.P (mk_alu_HC05 b b1 w w1 w2 w3 w4 b2 b3 b4 b5 b6 b7)) → Πa:alu_HC05.P a ≝
73 λP:alu_HC05 → Prop.λf:Πb,b1,w,w1,w2,w3,w4,b2,b3,b4,b5,b6,b7.P (mk_alu_HC05 b b1 w w1 w2 w3 w4 b2 b3 b4 b5 b6 b7).λa:alu_HC05.
74 match a with [ mk_alu_HC05 b b1 w w1 w2 w3 w4 b2 b3 b4 b5 b6 b7 ⇒ f b b1 w w1 w2 w3 w4 b2 b3 b4 b5 b6 b7 ].
76 ndefinition alu_HC05_rec :
77 ΠP:alu_HC05 → Set.(Πb,b1,w,w1,w2,w3,w4,b2,b3,b4,b5,b6,b7.P (mk_alu_HC05 b b1 w w1 w2 w3 w4 b2 b3 b4 b5 b6 b7)) → Πa:alu_HC05.P a ≝
78 λP:alu_HC05 → Set.λf:Πb,b1,w,w1,w2,w3,w4,b2,b3,b4,b5,b6,b7.P (mk_alu_HC05 b b1 w w1 w2 w3 w4 b2 b3 b4 b5 b6 b7).λa:alu_HC05.
79 match a with [ mk_alu_HC05 b b1 w w1 w2 w3 w4 b2 b3 b4 b5 b6 b7 ⇒ f b b1 w w1 w2 w3 w4 b2 b3 b4 b5 b6 b7 ].
81 ndefinition alu_HC05_rect :
82 ΠP:alu_HC05 → Type.(Πb,b1,w,w1,w2,w3,w4,b2,b3,b4,b5,b6,b7.P (mk_alu_HC05 b b1 w w1 w2 w3 w4 b2 b3 b4 b5 b6 b7)) → Πa:alu_HC05.P a ≝
83 λP:alu_HC05 → Type.λf:Πb,b1,w,w1,w2,w3,w4,b2,b3,b4,b5,b6,b7.P (mk_alu_HC05 b b1 w w1 w2 w3 w4 b2 b3 b4 b5 b6 b7).λa:alu_HC05.
84 match a with [ mk_alu_HC05 b b1 w w1 w2 w3 w4 b2 b3 b4 b5 b6 b7 ⇒ f b b1 w w1 w2 w3 w4 b2 b3 b4 b5 b6 b7 ].
86 ndefinition acc_low_reg_HC05 ≝ λalu.match alu with [ mk_alu_HC05 x _ _ _ _ _ _ _ _ _ _ _ _ ⇒ x ].
87 ndefinition indX_low_reg_HC05 ≝ λalu.match alu with [ mk_alu_HC05 _ x _ _ _ _ _ _ _ _ _ _ _ ⇒ x ].
88 ndefinition sp_reg_HC05 ≝ λalu.match alu with [ mk_alu_HC05 _ _ x _ _ _ _ _ _ _ _ _ _ ⇒ x ].
89 ndefinition sp_mask_HC05 ≝ λalu.match alu with [ mk_alu_HC05 _ _ _ x _ _ _ _ _ _ _ _ _ ⇒ x ].
90 ndefinition sp_fix_HC05 ≝ λalu.match alu with [ mk_alu_HC05 _ _ _ _ x _ _ _ _ _ _ _ _ ⇒ x ].
91 ndefinition pc_reg_HC05 ≝ λalu.match alu with [ mk_alu_HC05 _ _ _ _ _ x _ _ _ _ _ _ _ ⇒ x ].
92 ndefinition pc_mask_HC05 ≝ λalu.match alu with [ mk_alu_HC05 _ _ _ _ _ _ x _ _ _ _ _ _ ⇒ x ].
93 ndefinition h_flag_HC05 ≝ λalu.match alu with [ mk_alu_HC05 _ _ _ _ _ _ _ x _ _ _ _ _ ⇒ x ].
94 ndefinition i_flag_HC05 ≝ λalu.match alu with [ mk_alu_HC05 _ _ _ _ _ _ _ _ x _ _ _ _ ⇒ x ].
95 ndefinition n_flag_HC05 ≝ λalu.match alu with [ mk_alu_HC05 _ _ _ _ _ _ _ _ _ x _ _ _ ⇒ x ].
96 ndefinition z_flag_HC05 ≝ λalu.match alu with [ mk_alu_HC05 _ _ _ _ _ _ _ _ _ _ x _ _ ⇒ x ].
97 ndefinition c_flag_HC05 ≝ λalu.match alu with [ mk_alu_HC05 _ _ _ _ _ _ _ _ _ _ _ x _ ⇒ x ].
98 ndefinition irq_flag_HC05 ≝ λalu.match alu with [ mk_alu_HC05 _ _ _ _ _ _ _ _ _ _ _ _ x ⇒ x ].
100 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)}"
101 non associative with precedence 80 for
102 @{ 'mk_alu_HC05 $acclow $indxlow $sp $spm $spf $pc $pcm $hfl $ifl $nfl $zfl $cfl $irqfl }.
103 interpretation "mk_alu_HC05" 'mk_alu_HC05 acclow indxlow sp spm spf pc pcm hfl ifl nfl zfl cfl irqfl =
104 (mk_alu_HC05 acclow indxlow sp spm spf pc pcm hfl ifl nfl zfl cfl irqfl).
106 (* ALU dell'HC08/HCS08 *)
107 nrecord alu_HC08: Type ≝
109 (* A: registo accumulatore *)
110 acc_low_reg_HC08 : byte8;
111 (* X: registro indice parte bassa *)
112 indX_low_reg_HC08 : byte8;
113 (* H: registro indice parte alta *)
114 indX_high_reg_HC08 : byte8;
115 (* SP: registo stack pointer *)
116 sp_reg_HC08 : word16;
117 (* PC: registro program counter *)
118 pc_reg_HC08 : word16;
120 (* V: flag overflow *)
122 (* H: flag semi-carry (somma nibble basso) *)
124 (* I: flag mascheramento degli interrupt mascherabili: 1=mascherati *)
126 (* N: flag segno/negativita' *)
133 (* IRQ: flag che simula il pin esterno IRQ *)
137 ndefinition alu_HC08_ind :
138 ΠP:alu_HC08 → Prop.(Πb,b1,b2,w,w1,b3,b4,b5,b6,b7,b8,b9.P (mk_alu_HC08 b b1 b2 w w1 b3 b4 b5 b6 b7 b8 b9)) → Πa:alu_HC08.P a ≝
139 λP:alu_HC08 → Prop.λf:Πb,b1,b2,w,w1,b3,b4,b5,b6,b7,b8,b9.P (mk_alu_HC08 b b1 b2 w w1 b3 b4 b5 b6 b7 b8 b9).λa:alu_HC08.
140 match a with [ mk_alu_HC08 b b1 b2 w w1 b3 b4 b5 b6 b7 b8 b9 ⇒ f b b1 b2 w w1 b3 b4 b5 b6 b7 b8 b9 ].
142 ndefinition alu_HC08_rec :
143 ΠP:alu_HC08 → Set.(Πb,b1,b2,w,w1,b3,b4,b5,b6,b7,b8,b9.P (mk_alu_HC08 b b1 b2 w w1 b3 b4 b5 b6 b7 b8 b9)) → Πa:alu_HC08.P a ≝
144 λP:alu_HC08 → Set.λf:Πb,b1,b2,w,w1,b3,b4,b5,b6,b7,b8,b9.P (mk_alu_HC08 b b1 b2 w w1 b3 b4 b5 b6 b7 b8 b9).λa:alu_HC08.
145 match a with [ mk_alu_HC08 b b1 b2 w w1 b3 b4 b5 b6 b7 b8 b9 ⇒ f b b1 b2 w w1 b3 b4 b5 b6 b7 b8 b9 ].
147 ndefinition alu_HC08_rect :
148 ΠP:alu_HC08 → Type.(Πb,b1,b2,w,w1,b3,b4,b5,b6,b7,b8,b9.P (mk_alu_HC08 b b1 b2 w w1 b3 b4 b5 b6 b7 b8 b9)) → Πa:alu_HC08.P a ≝
149 λP:alu_HC08 → Type.λf:Πb,b1,b2,w,w1,b3,b4,b5,b6,b7,b8,b9.P (mk_alu_HC08 b b1 b2 w w1 b3 b4 b5 b6 b7 b8 b9).λa:alu_HC08.
150 match a with [ mk_alu_HC08 b b1 b2 w w1 b3 b4 b5 b6 b7 b8 b9 ⇒ f b b1 b2 w w1 b3 b4 b5 b6 b7 b8 b9 ].
152 ndefinition acc_low_reg_HC08 ≝ λalu.match alu with [ mk_alu_HC08 x _ _ _ _ _ _ _ _ _ _ _ ⇒ x ].
153 ndefinition indX_low_reg_HC08 ≝ λalu.match alu with [ mk_alu_HC08 _ x _ _ _ _ _ _ _ _ _ _ ⇒ x ].
154 ndefinition indX_high_reg_HC08 ≝ λalu.match alu with [ mk_alu_HC08 _ _ x _ _ _ _ _ _ _ _ _ ⇒ x ].
155 ndefinition sp_reg_HC08 ≝ λalu.match alu with [ mk_alu_HC08 _ _ _ x _ _ _ _ _ _ _ _ ⇒ x ].
156 ndefinition pc_reg_HC08 ≝ λalu.match alu with [ mk_alu_HC08 _ _ _ _ x _ _ _ _ _ _ _ ⇒ x ].
157 ndefinition v_flag_HC08 ≝ λalu.match alu with [ mk_alu_HC08 _ _ _ _ _ x _ _ _ _ _ _ ⇒ x ].
158 ndefinition h_flag_HC08 ≝ λalu.match alu with [ mk_alu_HC08 _ _ _ _ _ _ x _ _ _ _ _ ⇒ x ].
159 ndefinition i_flag_HC08 ≝ λalu.match alu with [ mk_alu_HC08 _ _ _ _ _ _ _ x _ _ _ _ ⇒ x ].
160 ndefinition n_flag_HC08 ≝ λalu.match alu with [ mk_alu_HC08 _ _ _ _ _ _ _ _ x _ _ _ ⇒ x ].
161 ndefinition z_flag_HC08 ≝ λalu.match alu with [ mk_alu_HC08 _ _ _ _ _ _ _ _ _ x _ _ ⇒ x ].
162 ndefinition c_flag_HC08 ≝ λalu.match alu with [ mk_alu_HC08 _ _ _ _ _ _ _ _ _ _ x _ ⇒ x ].
163 ndefinition irq_flag_HC08 ≝ λalu.match alu with [ mk_alu_HC08 _ _ _ _ _ _ _ _ _ _ _ x ⇒ x ].
165 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)}"
166 non associative with precedence 80 for
167 @{ 'mk_alu_HC08 $acclow $indxlow $indxhigh $sp $pc $vfl $hfl $ifl $nfl $zfl $cfl $irqfl }.
168 interpretation "mk_alu_HC08" 'mk_alu_HC08 acclow indxlow indxhigh sp pc vfl hfl ifl nfl zfl cfl irqfl =
169 (mk_alu_HC08 acclow indxlow indxhigh sp pc vfl hfl ifl nfl zfl cfl irqfl).
172 nrecord alu_RS08: Type ≝
174 (* A: registo accumulatore *)
175 acc_low_reg_RS08 : byte8;
176 (* PC: registro program counter *)
177 pc_reg_RS08 : word16;
178 (* modificatore di PC: per esempio e' definito come 00xxxxxxxxxxxxxxb *)
179 (* la logica della sua costruzione e' quindi (PC∧mask) *)
180 (* totalmente racchiusa nella ALU, bastera' fare get(set(PC)) *)
181 pc_mask_RS08 : word16;
182 (* SPC: registro shadow program counter *)
183 (* NB: il suo modificatore e' lo stesso di PC *)
184 spc_reg_RS08 : word16;
186 (* X: registro indice parte bassa *)
187 (* NB: in realta' e' mappato in memoria e non risiede nella ALU *)
188 (* la lettura/scrittura avviene tramite la locazione [0x000F] *)
189 (* la funzione memory_filter_read/write si occupera' di intercettare *)
190 (* e deviare sul registro le letture/scritture (modulo load_write) *)
192 (* PS: registro selezione di pagina *)
193 (* serve a indirizzare la finestra RAM di 64b [0x00C0-0x00FF] *)
194 (* su tutta la memoria installata [0x0000-0x3FFF]: [00pp pppp ppxx xxxx] *)
195 (* NB: in realta' e' mappato in memoria e non risiede nella ALU *)
196 (* la lettura/scrittura avviene tramite la locazione [0x001F] *)
197 (* la funzione memory_filter_read/write si occupera' di intercettare *)
198 (* e deviare sul registro le letture/scritture (modulo load_write) *)
207 ndefinition alu_RS08_ind :
208 ΠP:alu_RS08 → Prop.(Πb,w,w1,w2,b1,b2,b3,b4.P (mk_alu_RS08 b w w1 w2 b1 b2 b3 b4)) → Πa:alu_RS08.P a ≝
209 λP:alu_RS08 → Prop.λf:Πb,w,w1,w2,b1,b2,b3,b4.P (mk_alu_RS08 b w w1 w2 b1 b2 b3 b4).λa:alu_RS08.
210 match a with [ mk_alu_RS08 b w w1 w2 b1 b2 b3 b4 ⇒ f b w w1 w2 b1 b2 b3 b4 ].
212 ndefinition alu_RS08_rec :
213 ΠP:alu_RS08 → Set.(Πb,w,w1,w2,b1,b2,b3,b4.P (mk_alu_RS08 b w w1 w2 b1 b2 b3 b4)) → Πa:alu_RS08.P a ≝
214 λP:alu_RS08 → Set.λf:Πb,w,w1,w2,b1,b2,b3,b4.P (mk_alu_RS08 b w w1 w2 b1 b2 b3 b4).λa:alu_RS08.
215 match a with [ mk_alu_RS08 b w w1 w2 b1 b2 b3 b4 ⇒ f b w w1 w2 b1 b2 b3 b4 ].
217 ndefinition alu_RS08_rect :
218 ΠP:alu_RS08 → Type.(Πb,w,w1,w2,b1,b2,b3,b4.P (mk_alu_RS08 b w w1 w2 b1 b2 b3 b4)) → Πa:alu_RS08.P a ≝
219 λP:alu_RS08 → Type.λf:Πb,w,w1,w2,b1,b2,b3,b4.P (mk_alu_RS08 b w w1 w2 b1 b2 b3 b4).λa:alu_RS08.
220 match a with [ mk_alu_RS08 b w w1 w2 b1 b2 b3 b4 ⇒ f b w w1 w2 b1 b2 b3 b4 ].
222 ndefinition acc_low_reg_RS08 ≝ λalu.match alu with [ mk_alu_RS08 x _ _ _ _ _ _ _ ⇒ x ].
223 ndefinition pc_reg_RS08 ≝ λalu.match alu with [ mk_alu_RS08 _ x _ _ _ _ _ _ ⇒ x ].
224 ndefinition pc_mask_RS08 ≝ λalu.match alu with [ mk_alu_RS08 _ _ x _ _ _ _ _ ⇒ x ].
225 ndefinition spc_reg_RS08 ≝ λalu.match alu with [ mk_alu_RS08 _ _ _ x _ _ _ _ ⇒ x ].
226 ndefinition x_map_RS08 ≝ λalu.match alu with [ mk_alu_RS08 _ _ _ _ x _ _ _ ⇒ x ].
227 ndefinition ps_map_RS08 ≝ λalu.match alu with [ mk_alu_RS08 _ _ _ _ _ x _ _ ⇒ x ].
228 ndefinition z_flag_RS08 ≝ λalu.match alu with [ mk_alu_RS08 _ _ _ _ _ _ x _ ⇒ x ].
229 ndefinition c_flag_RS08 ≝ λalu.match alu with [ mk_alu_RS08 _ _ _ _ _ _ _ x ⇒ x ].
231 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)}"
232 non associative with precedence 80 for
233 @{ 'mk_alu_RS08 $acclow $pc $pcm $spc $xm $psm $zfl $cfl }.
234 interpretation "mk_alu_RS08" 'mk_alu_RS08 acclow pc pcm spc xm psm zfl cfl =
235 (mk_alu_RS08 acclow pc pcm spc xm psm zfl cfl).
237 (* tipo processore dipendente dalla mcu, varia solo la ALU *)
238 nrecord any_status (mcu:mcu_type) (t:memory_impl): Type ≝
241 [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ];
243 (* descritore della memoria *)
244 mem_desc : aux_mem_type t;
245 (* descrittore del tipo di memoria installata *)
246 chk_desc : aux_chk_type t;
247 (* descrittore del click = stato di avanzamento dell'esecuzione+cur_pc conseguente a fetch *)
248 (* 1) None = istruzione eseguita, attesa del fetch *)
249 (* 2) Some cur_clk,pseudo,mode,clks,cur_pc = fetch eseguito, countup a esecuzione *)
250 clk_desc : option (Prod5T byte8 (any_opcode mcu) (instr_mode) byte8 word16)
253 ndefinition any_status_ind :
254 Πmcu.Πt.ΠP:any_status mcu t → Prop.
255 (Πx:match mcu with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ].
256 Πn,n1,n2.P (mk_any_status mcu t x n n1 n2)) → Πa:any_status mcu t.P a ≝
257 λmcu.λt.λP:any_status mcu t → Prop.
258 λf:Πx:match mcu with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ].
259 Πn,n1,n2.P (mk_any_status mcu t x n n1 n2).λa:any_status mcu t.
260 match a with [ mk_any_status x n n1 n2 ⇒ f x n n1 n2 ].
262 ndefinition any_status_rec :
263 Πmcu.Πt.ΠP:any_status mcu t → Set.
264 (Πx:match mcu with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ].
265 Πn,n1,n2.P (mk_any_status mcu t x n n1 n2)) → Πa:any_status mcu t.P a ≝
266 λmcu.λt.λP:any_status mcu t → Set.
267 λf:Πx:match mcu with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ].
268 Πn,n1,n2.P (mk_any_status mcu t x n n1 n2).λa:any_status mcu t.
269 match a with [ mk_any_status x n n1 n2 ⇒ f x n n1 n2 ].
271 ndefinition any_status_rect :
272 Πmcu.Πt.ΠP:any_status mcu t → Type.
273 (Πx:match mcu with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ].
274 Πn,n1,n2.P (mk_any_status mcu t x n n1 n2)) → Πa:any_status mcu t.P a ≝
275 λmcu.λt.λP:any_status mcu t → Type.
276 λf:Πx:match mcu with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ].
277 Πn,n1,n2.P (mk_any_status mcu t x n n1 n2).λa:any_status mcu t.
278 match a with [ mk_any_status x n n1 n2 ⇒ f x n n1 n2 ].
280 ndefinition alu ≝ λmcu.λt.λw:any_status mcu t.match w with [ mk_any_status (x:match mcu with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ]) _ _ _ ⇒ x ].
281 ndefinition mem_desc ≝ λmcu.λt.λw:any_status mcu t.match w with [ mk_any_status _ x _ _ ⇒ x ].
282 ndefinition chk_desc ≝ λmcu.λt.λw:any_status mcu t.match w with [ mk_any_status _ _ x _ ⇒ x ].
283 ndefinition clk_desc ≝ λmcu.λt.λw:any_status mcu t.match w with [ mk_any_status _ _ _ x ⇒ x ].
285 (* evitare di mostrare la memoria/descrittore che impalla il visualizzatore *)
286 notation > "{hvbox('Alu' ≝ alu ; break 'Clk' ≝ clk)}" non associative with precedence 80
287 for @{ 'mk_any_status $alu $mem $chk $clk }.
288 interpretation "mk_any_status" 'mk_any_status alu mem chk clk =
289 (mk_any_status alu mem chk clk).
291 (* **************** *)
292 (* GETTER SPECIFICI *)
293 (* **************** *)
295 (* funzione ausiliaria per il tipaggio dei getter *)
296 ndefinition aux_get_typing ≝ λx:Type.λm:mcu_type.match m with
297 [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ] → x.
301 (* getter di A, esiste sempre *)
302 ndefinition get_acc_8_low_reg ≝
303 λm:mcu_type.λt:memory_impl.λs:any_status m t.
305 return aux_get_typing byte8 with
306 [ HC05 ⇒ acc_low_reg_HC05
307 | HC08 ⇒ acc_low_reg_HC08
308 | HCS08 ⇒ acc_low_reg_HC08
309 | RS08 ⇒ acc_low_reg_RS08 ]
312 (* getter di X, non esiste sempre *)
313 ndefinition get_indX_8_low_reg ≝
314 λm:mcu_type.λt:memory_impl.λs:any_status m t.
316 return aux_get_typing (option byte8) with
317 [ HC05 ⇒ λalu.Some ? (indX_low_reg_HC05 alu)
318 | HC08 ⇒ λalu.Some ? (indX_low_reg_HC08 alu)
319 | HCS08 ⇒ λalu.Some ? (indX_low_reg_HC08 alu)
320 | RS08 ⇒ λalu.None ? ]
323 (* getter di H, non esiste sempre *)
324 ndefinition get_indX_8_high_reg ≝
325 λm:mcu_type.λt:memory_impl.λs:any_status m t.
327 return aux_get_typing (option byte8) with
329 | HC08 ⇒ λalu.Some ? (indX_high_reg_HC08 alu)
330 | HCS08 ⇒ λalu.Some ? (indX_high_reg_HC08 alu)
331 | RS08 ⇒ λalu.None ? ]
334 (* getter di H:X, non esiste sempre *)
335 ndefinition get_indX_16_reg ≝
336 λm:mcu_type.λt:memory_impl.λs:any_status m t.
338 return aux_get_typing (option word16) with
340 | HC08 ⇒ λalu.Some ? (mk_word16 (indX_high_reg_HC08 alu) (indX_low_reg_HC08 alu))
341 | HCS08 ⇒ λalu.Some ? (mk_word16 (indX_high_reg_HC08 alu) (indX_low_reg_HC08 alu))
342 | RS08 ⇒ λalu.None ? ]
345 (* getter di SP, non esiste sempre *)
346 ndefinition get_sp_reg ≝
347 λm:mcu_type.λt:memory_impl.λs:any_status m t.
349 return aux_get_typing (option word16) with
350 [ HC05 ⇒ λalu.Some ? (sp_reg_HC05 alu)
351 | HC08 ⇒ λalu.Some ? (sp_reg_HC08 alu)
352 | HCS08 ⇒ λalu.Some ? (sp_reg_HC08 alu)
353 | RS08 ⇒ λalu.None ? ]
356 (* getter di PC, esiste sempre *)
357 ndefinition get_pc_reg ≝
358 λm:mcu_type.λt:memory_impl.λs:any_status m t.
360 return aux_get_typing word16 with
363 | HCS08 ⇒ pc_reg_HC08
364 | RS08 ⇒ pc_reg_RS08 ]
367 (* getter di SPC, non esiste sempre *)
368 ndefinition get_spc_reg ≝
369 λm:mcu_type.λt:memory_impl.λs:any_status m t.
371 return aux_get_typing (option word16) with
374 | HCS08 ⇒ λalu.None ?
375 | RS08 ⇒ λalu.Some ? (spc_reg_RS08 alu) ]
378 (* REGISTRI MEMORY MAPPED *)
380 (* getter di memory mapped X, non esiste sempre *)
381 ndefinition get_x_map ≝
382 λm:mcu_type.λt:memory_impl.λs:any_status m t.
384 return aux_get_typing (option byte8) with
387 | HCS08 ⇒ λalu.None ?
388 | RS08 ⇒ λalu.Some ? (x_map_RS08 alu) ]
391 (* getter di memory mapped PS, non esiste sempre *)
392 ndefinition get_ps_map ≝
393 λm:mcu_type.λt:memory_impl.λs:any_status m t.
395 return aux_get_typing (option byte8) with
398 | HCS08 ⇒ λalu.None ?
399 | RS08 ⇒ λalu.Some ? (ps_map_RS08 alu) ]
404 (* getter di V, non esiste sempre *)
405 ndefinition get_v_flag ≝
406 λm:mcu_type.λt:memory_impl.λs:any_status m t.
408 return aux_get_typing (option bool) with
410 | HC08 ⇒ λalu.Some ? (v_flag_HC08 alu)
411 | HCS08 ⇒ λalu.Some ? (v_flag_HC08 alu)
412 | RS08 ⇒ λalu.None ? ]
415 (* getter di H, non esiste sempre *)
416 ndefinition get_h_flag ≝
417 λm:mcu_type.λt:memory_impl.λs:any_status m t.
419 return aux_get_typing (option bool) with
420 [ HC05 ⇒ λalu.Some ? (h_flag_HC05 alu)
421 | HC08 ⇒ λalu.Some ? (h_flag_HC08 alu)
422 | HCS08 ⇒ λalu.Some ? (h_flag_HC08 alu)
423 | RS08 ⇒ λalu.None ? ]
426 (* getter di I, non esiste sempre *)
427 ndefinition get_i_flag ≝
428 λm:mcu_type.λt:memory_impl.λs:any_status m t.
430 return aux_get_typing (option bool) with
431 [ HC05 ⇒ λalu.Some ? (i_flag_HC05 alu)
432 | HC08 ⇒ λalu.Some ? (i_flag_HC08 alu)
433 | HCS08 ⇒ λalu.Some ? (i_flag_HC08 alu)
434 | RS08 ⇒ λalu.None ? ]
437 (* getter di N, non esiste sempre *)
438 ndefinition get_n_flag ≝
439 λm:mcu_type.λt:memory_impl.λs:any_status m t.
441 return aux_get_typing (option bool) with
442 [ HC05 ⇒ λalu.Some ? (n_flag_HC05 alu)
443 | HC08 ⇒ λalu.Some ? (n_flag_HC08 alu)
444 | HCS08 ⇒ λalu.Some ? (n_flag_HC08 alu)
445 | RS08 ⇒ λalu.None ? ]
448 (* getter di Z, esiste sempre *)
449 ndefinition get_z_flag ≝
450 λm:mcu_type.λt:memory_impl.λs:any_status m t.
452 return aux_get_typing bool with
455 | HCS08 ⇒ z_flag_HC08
456 | RS08 ⇒ z_flag_RS08 ]
459 (* getter di C, esiste sempre *)
460 ndefinition get_c_flag ≝
461 λm:mcu_type.λt:memory_impl.λs:any_status m t.
463 return aux_get_typing bool with
466 | HCS08 ⇒ c_flag_HC08
467 | RS08 ⇒ c_flag_RS08 ]
470 (* getter di IRQ, non esiste sempre *)
471 ndefinition get_irq_flag ≝
472 λm:mcu_type.λt:memory_impl.λs:any_status m t.
474 return aux_get_typing (option bool) with
475 [ HC05 ⇒ λalu.Some ? (irq_flag_HC05 alu)
476 | HC08 ⇒ λalu.Some ? (irq_flag_HC08 alu)
477 | HCS08 ⇒ λalu.Some ? (irq_flag_HC08 alu)
478 | RS08 ⇒ λalu.None ? ]
481 (* DESCRITTORI ESTERNI ALLA ALU *)
483 (* getter della ALU, esiste sempre *)
484 ndefinition get_alu ≝ λm:mcu_type.λt:memory_impl.λs:any_status m t.alu m t s.
486 (* getter della memoria, esiste sempre *)
487 ndefinition get_mem_desc ≝ λm:mcu_type.λt:memory_impl.λs:any_status m t.mem_desc m t s.
489 (* getter del descrittore, esiste sempre *)
490 ndefinition get_chk_desc ≝ λm:mcu_type.λt:memory_impl.λs:any_status m t.chk_desc m t s.
492 (* getter del clik, esiste sempre *)
493 ndefinition get_clk_desc ≝ λm:mcu_type.λt:memory_impl.λs:any_status m t.clk_desc m t s.
495 (* ***************************** *)
496 (* SETTER SPECIFICI FORTI/DEBOLI *)
497 (* ***************************** *)
499 (* funzione ausiliaria per il tipaggio dei setter forti *)
500 ndefinition aux_set_typing ≝ λx:Type.λm:mcu_type.
501 match m with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ]
503 match m with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ].
505 (* funzione ausiliaria per il tipaggio dei setter deboli *)
506 ndefinition aux_set_typing_opt ≝ λx:Type.λm:mcu_type.option
507 (match m with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ]
509 match m with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ]).
511 (* DESCRITTORI ESTERNI ALLA ALU *)
513 (* setter forte della ALU *)
514 ndefinition set_alu ≝
515 λm:mcu_type.λt:memory_impl.λs:any_status m t.λalu'.
516 mk_any_status m t alu' (get_mem_desc m t s) (get_chk_desc m t s) (get_clk_desc m t s).
518 (* setter forte della memoria *)
519 ndefinition set_mem_desc ≝
520 λm:mcu_type.λt:memory_impl.λs:any_status m t.λmem':aux_mem_type t.
521 mk_any_status m t (get_alu m t s) mem' (get_chk_desc m t s) (get_clk_desc m t s).
523 (* setter forte del descrittore *)
524 ndefinition set_chk_desc ≝
525 λm:mcu_type.λt:memory_impl.λs:any_status m t.λchk':aux_chk_type t.
526 mk_any_status m t (get_alu m t s) (get_mem_desc m t s) chk' (get_clk_desc m t s).
528 (* setter forte del clik *)
529 ndefinition set_clk_desc ≝
530 λm:mcu_type.λt:memory_impl.λs:any_status m t.
531 λclk':option (Prod5T byte8 (any_opcode m) (instr_mode) byte8 word16).
532 mk_any_status m t (get_alu m t s) (get_mem_desc m t s) (get_chk_desc m t s) clk'.
536 (* setter specifico HC05 di A *)
537 ndefinition set_acc_8_low_reg_HC05 ≝
541 (indX_low_reg_HC05 alu)
554 (* setter specifico HC08/HCS08 di A *)
555 ndefinition set_acc_8_low_reg_HC08 ≝
559 (indX_low_reg_HC08 alu)
560 (indX_high_reg_HC08 alu)
571 (* setter specifico RS08 di A *)
572 ndefinition set_acc_8_low_reg_RS08 ≝
584 (* setter forte di A *)
585 ndefinition set_acc_8_low_reg ≝
586 λm:mcu_type.λt:memory_impl.λs:any_status m t.λacclow':byte8.
588 (match m return aux_set_typing byte8 with
589 [ HC05 ⇒ set_acc_8_low_reg_HC05
590 | HC08 ⇒ set_acc_8_low_reg_HC08
591 | HCS08 ⇒ set_acc_8_low_reg_HC08
592 | RS08 ⇒ set_acc_8_low_reg_RS08
593 ] (alu m t s) acclow').
597 (* setter specifico HC05 di X *)
598 ndefinition set_indX_8_low_reg_HC05 ≝
599 λalu.λindxlow':byte8.
601 (acc_low_reg_HC05 alu)
615 (* setter specifico HC08/HCS08 di X *)
616 ndefinition set_indX_8_low_reg_HC08 ≝
617 λalu.λindxlow':byte8.
619 (acc_low_reg_HC08 alu)
621 (indX_high_reg_HC08 alu)
632 (* setter forte di X *)
633 ndefinition set_indX_8_low_reg ≝
634 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindxlow':byte8.
635 opt_map ?? (match m return aux_set_typing_opt byte8 with
636 [ HC05 ⇒ Some ? set_indX_8_low_reg_HC05
637 | HC08 ⇒ Some ? set_indX_8_low_reg_HC08
638 | HCS08 ⇒ Some ? set_indX_8_low_reg_HC08
640 (λf.Some ? (set_alu m t s (f (alu m t s) indxlow'))).
642 (* setter debole di X *)
643 ndefinition setweak_indX_8_low_reg ≝
644 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindxlow':byte8.
645 match set_indX_8_low_reg m t s indxlow' with
646 [ None ⇒ s | Some s' ⇒ s' ].
650 (* setter specifico HC08/HCS08 di H *)
651 ndefinition set_indX_8_high_reg_HC08 ≝
652 λalu.λindxhigh':byte8.
654 (acc_low_reg_HC08 alu)
655 (indX_low_reg_HC08 alu)
667 (* setter forte di H *)
668 ndefinition set_indX_8_high_reg ≝
669 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindxhigh':byte8.
670 opt_map ?? (match m return aux_set_typing_opt byte8 with
672 | HC08 ⇒ Some ? set_indX_8_high_reg_HC08
673 | HCS08 ⇒ Some ? set_indX_8_high_reg_HC08
675 (λf.Some ? (set_alu m t s (f (alu m t s) indxhigh'))).
677 (* setter debole di H *)
678 ndefinition setweak_indX_8_high_reg ≝
679 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindxhigh':byte8.
680 match set_indX_8_high_reg m t s indxhigh' with
681 [ None ⇒ s | Some s' ⇒ s' ].
685 (* setter specifico HC08/HCS08 di H:X *)
686 ndefinition set_indX_16_reg_HC08 ≝
689 (acc_low_reg_HC08 alu)
702 (* setter forte di H:X *)
703 ndefinition set_indX_16_reg ≝
704 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindx16:word16.
705 opt_map ?? (match m return aux_set_typing_opt word16 with
707 | HC08 ⇒ Some ? set_indX_16_reg_HC08
708 | HCS08 ⇒ Some ? set_indX_16_reg_HC08
710 (λf.Some ? (set_alu m t s (f (alu m t s) indx16))).
712 (* setter debole di H:X *)
713 ndefinition setweak_indX_16_reg ≝
714 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindx16:word16.
715 match set_indX_16_reg m t s indx16 with
716 [ None ⇒ s | Some s' ⇒ s' ].
720 (* setter specifico HC05 di SP, effettua (SP∧mask)∨fix *)
721 ndefinition set_sp_reg_HC05 ≝
724 (acc_low_reg_HC05 alu)
725 (indX_low_reg_HC05 alu)
726 (or_w16 (and_w16 sp' (sp_mask_HC05 alu)) (sp_fix_HC05 alu))
738 (* setter specifico HC08/HCS08 di SP *)
739 ndefinition set_sp_reg_HC08 ≝
742 (acc_low_reg_HC08 alu)
743 (indX_low_reg_HC08 alu)
744 (indX_high_reg_HC08 alu)
755 (* setter forte di SP *)
756 ndefinition set_sp_reg ≝
757 λm:mcu_type.λt:memory_impl.λs:any_status m t.λsp':word16.
758 opt_map ?? (match m return aux_set_typing_opt word16 with
759 [ HC05 ⇒ Some ? set_sp_reg_HC05
760 | HC08 ⇒ Some ? set_sp_reg_HC08
761 | HCS08 ⇒ Some ? set_sp_reg_HC08
763 (λf.Some ? (set_alu m t s (f (alu m t s) sp'))).
765 (* setter debole di SP *)
766 ndefinition setweak_sp_reg ≝
767 λm:mcu_type.λt:memory_impl.λs:any_status m t.λsp':word16.
768 match set_sp_reg m t s sp' with
769 [ None ⇒ s | Some s' ⇒ s' ].
773 (* setter specifico HC05 di PC, effettua PC∧mask *)
774 ndefinition set_pc_reg_HC05 ≝
777 (acc_low_reg_HC05 alu)
778 (indX_low_reg_HC05 alu)
782 (and_w16 pc' (pc_mask_HC05 alu))
791 (* setter specifico HC08/HCS08 di PC *)
792 ndefinition set_pc_reg_HC08 ≝
795 (acc_low_reg_HC08 alu)
796 (indX_low_reg_HC08 alu)
797 (indX_high_reg_HC08 alu)
808 (* setter specifico RS08 di PC, effettua PC∧mask *)
809 ndefinition set_pc_reg_RS08 ≝
812 (acc_low_reg_RS08 alu)
813 (and_w16 pc' (pc_mask_RS08 alu))
821 (* setter forte di PC *)
822 ndefinition set_pc_reg ≝
823 λm:mcu_type.λt:memory_impl.λs:any_status m t.λpc':word16.
825 (match m return aux_set_typing word16 with
826 [ HC05 ⇒ set_pc_reg_HC05
827 | HC08 ⇒ set_pc_reg_HC08
828 | HCS08 ⇒ set_pc_reg_HC08
829 | RS08 ⇒ set_pc_reg_RS08
834 (* setter specifico RS08 di SPC, effettua SPC∧mask *)
835 ndefinition set_spc_reg_RS08 ≝
838 (acc_low_reg_RS08 alu)
841 (and_w16 spc' (pc_mask_RS08 alu))
847 (* setter forte di SPC *)
848 ndefinition set_spc_reg ≝
849 λm:mcu_type.λt:memory_impl.λs:any_status m t.λspc':word16.
850 opt_map ?? (match m return aux_set_typing_opt word16 with
854 | RS08 ⇒ Some ? set_spc_reg_RS08 ])
855 (λf.Some ? (set_alu m t s (f (alu m t s) spc'))).
857 (* setter debole di SPC *)
858 ndefinition setweak_spc_reg ≝
859 λm:mcu_type.λt:memory_impl.λs:any_status m t.λspc':word16.
860 match set_spc_reg m t s spc' with
861 [ None ⇒ s | Some s' ⇒ s' ].
863 (* REGISTRO MEMORY MAPPED X *)
865 (* setter specifico RS08 di memory mapped X *)
866 ndefinition set_x_map_RS08 ≝
869 (acc_low_reg_RS08 alu)
878 (* setter forte di memory mapped X *)
879 ndefinition set_x_map ≝
880 λm:mcu_type.λt:memory_impl.λs:any_status m t.λxm':byte8.
881 opt_map ?? (match m return aux_set_typing_opt byte8 with
885 | RS08 ⇒ Some ? set_x_map_RS08 ])
886 (λf.Some ? (set_alu m t s (f (alu m t s) xm'))).
888 (* setter debole di memory mapped X *)
889 ndefinition setweak_x_map ≝
890 λm:mcu_type.λt:memory_impl.λs:any_status m t.λxm':byte8.
891 match set_x_map m t s xm' with
892 [ None ⇒ s | Some s' ⇒ s' ].
894 (* REGISTRO MEMORY MAPPED PS *)
896 (* setter specifico RS08 di memory mapped PS *)
897 ndefinition set_ps_map_RS08 ≝
900 (acc_low_reg_RS08 alu)
909 (* setter forte di memory mapped PS *)
910 ndefinition set_ps_map ≝
911 λm:mcu_type.λt:memory_impl.λs:any_status m t.λpsm':byte8.
912 opt_map ?? (match m return aux_set_typing_opt byte8 with
916 | RS08 ⇒ Some ? set_ps_map_RS08 ])
917 (λf.Some ? (set_alu m t s (f (alu m t s) psm'))).
919 (* setter debole di memory mapped PS *)
920 ndefinition setweak_ps_map ≝
921 λm:mcu_type.λt:memory_impl.λs:any_status m t.λpsm':byte8.
922 match set_ps_map m t s psm' with
923 [ None ⇒ s | Some s' ⇒ s' ].
927 (* setter specifico HC08/HCS08 di V *)
928 ndefinition set_v_flag_HC08 ≝
931 (acc_low_reg_HC08 alu)
932 (indX_low_reg_HC08 alu)
933 (indX_high_reg_HC08 alu)
944 (* setter forte di V *)
945 ndefinition set_v_flag ≝
946 λm:mcu_type.λt:memory_impl.λs:any_status m t.λvfl':bool.
947 opt_map ?? (match m return aux_set_typing_opt bool with
949 | HC08 ⇒ Some ? set_v_flag_HC08
950 | HCS08 ⇒ Some ? set_v_flag_HC08
952 (λf.Some ? (set_alu m t s (f (alu m t s) vfl'))).
954 (* setter debole di V *)
955 ndefinition setweak_v_flag ≝
956 λm:mcu_type.λt:memory_impl.λs:any_status m t.λvfl':bool.
957 match set_v_flag m t s vfl' with
958 [ None ⇒ s | Some s' ⇒ s' ].
962 (* setter specifico HC05 di H *)
963 ndefinition set_h_flag_HC05 ≝
966 (acc_low_reg_HC05 alu)
967 (indX_low_reg_HC05 alu)
980 (* setter specifico HC08/HCS08 di H *)
981 ndefinition set_h_flag_HC08 ≝
984 (acc_low_reg_HC08 alu)
985 (indX_low_reg_HC08 alu)
986 (indX_high_reg_HC08 alu)
997 (* setter forte di H *)
998 ndefinition set_h_flag ≝
999 λm:mcu_type.λt:memory_impl.λs:any_status m t.λhfl':bool.
1000 opt_map ?? (match m return aux_set_typing_opt bool with
1001 [ HC05 ⇒ Some ? set_h_flag_HC05
1002 | HC08 ⇒ Some ? set_h_flag_HC08
1003 | HCS08 ⇒ Some ? set_h_flag_HC08
1005 (λf.Some ? (set_alu m t s (f (alu m t s) hfl'))).
1007 (* setter debole di H *)
1008 ndefinition setweak_h_flag ≝
1009 λm:mcu_type.λt:memory_impl.λs:any_status m t.λhfl':bool.
1010 match set_h_flag m t s hfl' with
1011 [ None ⇒ s | Some s' ⇒ s' ].
1015 (* setter specifico HC05 di I *)
1016 ndefinition set_i_flag_HC05 ≝
1019 (acc_low_reg_HC05 alu)
1020 (indX_low_reg_HC05 alu)
1031 (irq_flag_HC05 alu).
1033 (* setter specifico HC08/HCS08 di I *)
1034 ndefinition set_i_flag_HC08 ≝
1037 (acc_low_reg_HC08 alu)
1038 (indX_low_reg_HC08 alu)
1039 (indX_high_reg_HC08 alu)
1048 (irq_flag_HC08 alu).
1050 (* setter forte di I *)
1051 ndefinition set_i_flag ≝
1052 λm:mcu_type.λt:memory_impl.λs:any_status m t.λifl':bool.
1053 opt_map ?? (match m return aux_set_typing_opt bool with
1054 [ HC05 ⇒ Some ? set_i_flag_HC05
1055 | HC08 ⇒ Some ? set_i_flag_HC08
1056 | HCS08 ⇒ Some ? set_i_flag_HC08
1058 (λf.Some ? (set_alu m t s (f (alu m t s) ifl'))).
1060 (* setter debole di I *)
1061 ndefinition setweak_i_flag ≝
1062 λm:mcu_type.λt:memory_impl.λs:any_status m t.λifl':bool.
1063 match set_i_flag m t s ifl' with
1064 [ None ⇒ s | Some s' ⇒ s' ].
1068 (* setter specifico HC05 di N *)
1069 ndefinition set_n_flag_HC05 ≝
1072 (acc_low_reg_HC05 alu)
1073 (indX_low_reg_HC05 alu)
1084 (irq_flag_HC05 alu).
1086 (* setter specifico HC08/HCS08 di N *)
1087 ndefinition set_n_flag_HC08 ≝
1090 (acc_low_reg_HC08 alu)
1091 (indX_low_reg_HC08 alu)
1092 (indX_high_reg_HC08 alu)
1101 (irq_flag_HC08 alu).
1103 (* setter forte di N *)
1104 ndefinition set_n_flag ≝
1105 λm:mcu_type.λt:memory_impl.λs:any_status m t.λnfl':bool.
1106 opt_map ?? (match m return aux_set_typing_opt bool with
1107 [ HC05 ⇒ Some ? set_n_flag_HC05
1108 | HC08 ⇒ Some ? set_n_flag_HC08
1109 | HCS08 ⇒ Some ? set_n_flag_HC08
1111 (λf.Some ? (set_alu m t s (f (alu m t s) nfl'))).
1113 (* setter debole di N *)
1114 ndefinition setweak_n_flag ≝
1115 λm:mcu_type.λt:memory_impl.λs:any_status m t.λnfl':bool.
1116 match set_n_flag m t s nfl' with
1117 [ None ⇒ s | Some s' ⇒ s' ].
1121 (* setter specifico HC05 di Z *)
1122 ndefinition set_z_flag_HC05 ≝
1125 (acc_low_reg_HC05 alu)
1126 (indX_low_reg_HC05 alu)
1137 (irq_flag_HC05 alu).
1139 (* setter specifico HC08/HCS08 di Z *)
1140 ndefinition set_z_flag_HC08 ≝
1143 (acc_low_reg_HC08 alu)
1144 (indX_low_reg_HC08 alu)
1145 (indX_high_reg_HC08 alu)
1154 (irq_flag_HC08 alu).
1156 (* setter sprcifico RS08 di Z *)
1157 ndefinition set_z_flag_RS08 ≝
1160 (acc_low_reg_RS08 alu)
1169 (* setter forte di Z *)
1170 ndefinition set_z_flag ≝
1171 λm:mcu_type.λt:memory_impl.λs:any_status m t.λzfl':bool.
1173 (match m return aux_set_typing bool with
1174 [ HC05 ⇒ set_z_flag_HC05
1175 | HC08 ⇒ set_z_flag_HC08
1176 | HCS08 ⇒ set_z_flag_HC08
1177 | RS08 ⇒ set_z_flag_RS08
1178 ] (alu m t s) zfl').
1182 (* setter specifico HC05 di C *)
1183 ndefinition set_c_flag_HC05 ≝
1186 (acc_low_reg_HC05 alu)
1187 (indX_low_reg_HC05 alu)
1198 (irq_flag_HC05 alu).
1200 (* setter specifico HC08/HCS08 di C *)
1201 ndefinition set_c_flag_HC08 ≝
1204 (acc_low_reg_HC08 alu)
1205 (indX_low_reg_HC08 alu)
1206 (indX_high_reg_HC08 alu)
1215 (irq_flag_HC08 alu).
1217 (* setter specifico RS08 di C *)
1218 ndefinition set_c_flag_RS08 ≝
1221 (acc_low_reg_RS08 alu)
1230 (* setter forte di C *)
1231 ndefinition set_c_flag ≝
1232 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcfl':bool.
1234 (match m return aux_set_typing bool with
1235 [ HC05 ⇒ set_c_flag_HC05
1236 | HC08 ⇒ set_c_flag_HC08
1237 | HCS08 ⇒ set_c_flag_HC08
1238 | RS08 ⇒ set_c_flag_RS08
1239 ] (alu m t s) cfl').
1243 (* setter specifico HC05 di IRQ *)
1244 ndefinition set_irq_flag_HC05 ≝
1247 (acc_low_reg_HC05 alu)
1248 (indX_low_reg_HC05 alu)
1261 (* setter specifico HC08/HCS08 di IRQ *)
1262 ndefinition set_irq_flag_HC08 ≝
1265 (acc_low_reg_HC08 alu)
1266 (indX_low_reg_HC08 alu)
1267 (indX_high_reg_HC08 alu)
1278 (* setter forte di IRQ *)
1279 ndefinition set_irq_flag ≝
1280 λm:mcu_type.λt:memory_impl.λs:any_status m t.λirqfl':bool.
1281 opt_map ?? (match m return aux_set_typing_opt bool with
1282 [ HC05 ⇒ Some ? set_irq_flag_HC05
1283 | HC08 ⇒ Some ? set_irq_flag_HC08
1284 | HCS08 ⇒ Some ? set_irq_flag_HC08
1286 (λf.Some ? (set_alu m t s (f (alu m t s) irqfl'))).
1288 (* setter debole di IRQ *)
1289 ndefinition setweak_irq_flag ≝
1290 λm:mcu_type.λt:memory_impl.λs:any_status m t.λirqfl':bool.
1291 match set_irq_flag m t s irqfl' with
1292 [ None ⇒ s | Some s' ⇒ s' ].
1294 (* ***************** *)
1295 (* CONFRONTO FRA ALU *)
1296 (* ***************** *)
1298 (* confronto registro per registro dell'HC05 *)
1299 ndefinition eq_alu_HC05 ≝
1300 λalu1,alu2:alu_HC05.
1302 [ mk_alu_HC05 acclow1 indxlow1 sp1 spm1 spf1 pc1 pcm1 hfl1 ifl1 nfl1 zfl1 cfl1 irqfl1 ⇒
1304 [ mk_alu_HC05 acclow2 indxlow2 sp2 spm2 spf2 pc2 pcm2 hfl2 ifl2 nfl2 zfl2 cfl2 irqfl2 ⇒
1305 (eq_b8 acclow1 acclow2) ⊗
1306 (eq_b8 indxlow1 indxlow2) ⊗
1308 (eq_w16 spm1 spm2) ⊗
1309 (eq_w16 spf1 spf2) ⊗
1311 (eq_w16 pcm1 pcm2) ⊗
1312 (eq_bool hfl1 hfl2) ⊗
1313 (eq_bool ifl1 ifl2) ⊗
1314 (eq_bool nfl1 nfl2) ⊗
1315 (eq_bool zfl1 zfl2) ⊗
1316 (eq_bool cfl1 cfl2) ⊗
1317 (eq_bool irqfl1 irqfl2) ]].
1319 (* confronto registro per registro dell'HC08 *)
1320 ndefinition eq_alu_HC08 ≝
1321 λalu1,alu2:alu_HC08.
1323 [ mk_alu_HC08 acclow1 indxlow1 indxhigh1 sp1 pc1 vfl1 hfl1 ifl1 nfl1 zfl1 cfl1 irqfl1 ⇒
1325 [ mk_alu_HC08 acclow2 indxlow2 indxhigh2 sp2 pc2 vfl2 hfl2 ifl2 nfl2 zfl2 cfl2 irqfl2 ⇒
1326 (eq_b8 acclow1 acclow2) ⊗
1327 (eq_b8 indxlow1 indxlow2) ⊗
1328 (eq_b8 indxhigh1 indxhigh2) ⊗
1331 (eq_bool vfl1 vfl2) ⊗
1332 (eq_bool hfl1 hfl2) ⊗
1333 (eq_bool ifl1 ifl2) ⊗
1334 (eq_bool nfl1 nfl2) ⊗
1335 (eq_bool zfl1 zfl2) ⊗
1336 (eq_bool cfl1 cfl2) ⊗
1337 (eq_bool irqfl1 irqfl2) ]].
1339 (* confronto registro per registro dell'RS08 *)
1340 ndefinition eq_alu_RS08 ≝
1341 λalu1,alu2:alu_RS08.
1343 [ mk_alu_RS08 acclow1 pc1 pcm1 spc1 xm1 psm1 zfl1 cfl1 ⇒
1345 [ mk_alu_RS08 acclow2 pc2 pcm2 spc2 xm2 psm2 zfl2 cfl2 ⇒
1346 (eq_b8 acclow1 acclow2) ⊗
1348 (eq_w16 pcm1 pcm2) ⊗
1349 (eq_w16 spc1 spc2) ⊗
1352 (eq_bool zfl1 zfl2) ⊗
1353 (eq_bool cfl1 cfl2) ]].
1355 (* ******************** *)
1356 (* CONFRONTO FRA STATUS *)
1357 (* ******************** *)
1359 (* confronto di una regione di memoria [addr1 ; ... ; addrn] *)
1360 nlet rec forall_memory_ranged
1362 (chk1:aux_chk_type t) (chk2:aux_chk_type t)
1363 (mem1:aux_mem_type t) (mem2:aux_mem_type t)
1364 (addrl:list word16) on addrl ≝
1365 match addrl return λ_.bool with
1367 | cons hd tl ⇒ (eq_option byte8 (mem_read t mem1 chk1 hd)
1368 (mem_read t mem2 chk2 hd) eq_b8) ⊗
1369 (forall_memory_ranged t chk1 chk2 mem1 mem2 tl)
1372 (* il clk e' option (Prod5T byte8 (any_opcode m) (instr_mode) byte8 word16) *)
1373 ndefinition eq_clk ≝
1374 λm:mcu_type.λc1,c2:option (Prod5T byte8 (any_opcode m) (instr_mode) byte8 word16).
1376 [ None ⇒ match c2 with
1377 [ None ⇒ true | Some _ ⇒ false ]
1378 | Some c1' ⇒ match c2 with
1379 [ None ⇒ false | Some c2' ⇒ (eq_b8 (fst5T ????? c1') (fst5T ????? c2')) ⊗
1380 (eq_anyop m (snd5T ????? c1') (snd5T ????? c2')) ⊗
1381 (eq_instrmode (thd5T ????? c1') (thd5T ????? c2')) ⊗
1382 (eq_b8 (frth5T ????? c1') (frth5T ????? c2')) ⊗
1383 (eq_w16 (ffth5T ????? c1') (ffth5T ????? c2')) ]
1386 (* generalizzazione del confronto fra stati *)
1387 ndefinition eq_status ≝
1388 λm:mcu_type.λt:memory_impl.λs1,s2:any_status m t.λaddrl:list word16.
1389 match s1 with [ mk_any_status alu1 mem1 chk1 clk1 ⇒
1390 match s2 with [ mk_any_status alu2 mem2 chk2 clk2 ⇒
1392 (* 1) confronto della ALU *)
1393 (match m return λm:mcu_type.
1395 [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ] →
1397 [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ] →
1399 [ HC05 ⇒ eq_alu_HC05 | HC08 ⇒ eq_alu_HC08 | HCS08 ⇒ eq_alu_HC08 | RS08 ⇒ eq_alu_RS08 ]
1402 (* 2) confronto della memoria in [inf,inf+n] *)
1403 (forall_memory_ranged t chk1 chk2 mem1 mem2 addrl) ⊗
1405 (* 3) confronto del clik *)
1406 (eq_clk m clk1 clk2)