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 (* Ultima modifica: 05/08/2009 *)
21 (* ********************************************************************** *)
23 include "freescale/load_write.ma".
25 (* ************************************************ *)
26 (* LOGICHE AUSILIARE CHE ACCOMUNANO PIU' OPERAZIONI *)
27 (* ************************************************ *)
29 (* NB: dentro il codice i commenti cercano di spiegare la logica
30 secondo quanto riportato dalle specifiche delle mcu *)
32 (* NB: notare che tranne nei casi in cui PC viene modificato esplicitamente
33 il suo avanzamento viene delegato totalmente agli strati inferiori
34 I) avanzamento dovuto al decode degli op (fetch)
35 II) avanzamento dovuto al caricamento degli argomenti (multi_mode_load/write)
36 la modifica effettiva avviene poi centralizzata in tick *)
38 (* A = [true] fAMC(A,M,C), [false] A *)
39 (* cioe' in caso di false l'operazione viene eseguita ma modifica solo i flag *)
40 (* fAMC e' la logica da applicare: somma con/senza carry *)
41 ndefinition execute_ADC_ADD_aux ≝
42 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.λsetflag:bool.
43 λfAMC:byte8 → byte8 → bool → ProdT byte8 bool.
44 opt_map … (multi_mode_load true m t s cur_pc i)
45 (λS_M_PC.match S_M_PC with
46 [ triple s_tmp1 M_op new_pc ⇒
47 let A_op ≝ get_acc_8_low_reg m t s_tmp1 in
48 match fAMC A_op M_op (get_c_flag m t s_tmp1) with
50 let A7 ≝ MSB_b8 A_op in let M7 ≝ MSB_b8 M_op in let R7 ≝ MSB_b8 R_op in
51 let A3 ≝ MSB_ex (b8l A_op) in let M3 ≝ MSB_ex (b8l M_op) in let R3 ≝ MSB_ex (b8l R_op) in
52 (* A = [true] fAMC(A,M,C), [false] A *)
53 let s_tmp2 ≝ match setflag with [ true ⇒ set_acc_8_low_reg m t s_tmp1 R_op | false ⇒ s_tmp1 ] in
54 (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
55 let s_tmp3 ≝ set_z_flag m t s_tmp2 (eq_b8 R_op 〈x0,x0〉) in
56 (* C = A7&M7 | M7&nR7 | nR7&A7 *)
57 let s_tmp4 ≝ set_c_flag m t s_tmp3 ((A7⊗M7) ⊕ (M7⊗(⊖R7)) ⊕ ((⊖R7)⊗A7)) in
59 let s_tmp5 ≝ setweak_n_flag m t s_tmp4 R7 in
60 (* H = A3&M3 | M3&nR3 | nR3&A3 *)
61 let s_tmp6 ≝ setweak_h_flag m t s_tmp5 ((A3⊗M3) ⊕ (M3⊗(⊖R3)) ⊕ ((⊖R3)⊗A3)) in
62 (* V = A7&M7&nR7 | nA7&nM7&R7 *)
63 let s_tmp7 ≝ setweak_v_flag m t s_tmp6 ((A7⊗M7⊗(⊖R7)) ⊕ ((⊖A7)⊗(⊖M7)⊗R7)) in
65 Some ? (pair … s_tmp7 new_pc) ]]).
67 (* A = [true] fAM(A,M), [false] A *)
68 (* cioe' in caso di false l'operazione viene eseguita ma modifica solo i flag *)
69 (* fAM e' la logica da applicare: and/xor/or *)
70 ndefinition execute_AND_BIT_EOR_ORA_aux ≝
71 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.λsetflag:bool.
72 λfAM:byte8 → byte8 → byte8.
73 opt_map … (multi_mode_load true m t s cur_pc i)
74 (λS_M_PC.match S_M_PC with
75 [ triple s_tmp1 M_op new_pc ⇒
76 let R_op ≝ fAM (get_acc_8_low_reg m t s_tmp1) M_op in
77 (* A = [true] fAM(A,M), [false] A *)
78 let s_tmp2 ≝ match setflag with [ true ⇒ set_acc_8_low_reg m t s_tmp1 R_op | false ⇒ s_tmp1 ] in
79 (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
80 let s_tmp3 ≝ set_z_flag m t s_tmp2 (eq_b8 R_op 〈x0,x0〉) in
82 let s_tmp4 ≝ setweak_n_flag m t s_tmp3 (MSB_b8 R_op) in
84 let s_tmp5 ≝ setweak_v_flag m t s_tmp4 false in
86 Some ? (pair … s_tmp5 new_pc) ]).
89 (* fMC e' la logica da applicare: rc_/ro_/sh_ *)
90 ndefinition execute_ASL_ASR_LSR_ROL_ROR_aux ≝
91 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
92 λfMC:byte8 → bool → ProdT byte8 bool.
93 opt_map … (multi_mode_load true m t s cur_pc i)
94 (λS_M_PC.match S_M_PC with
95 [ triple s_tmp1 M_op _ ⇒
96 match fMC M_op (get_c_flag m t s_tmp1) with [ pair R_op carry ⇒
98 opt_map … (multi_mode_write true m t s_tmp1 cur_pc i R_op)
99 (λS_PC.match S_PC with
100 [ pair s_tmp2 new_pc ⇒
102 let s_tmp3 ≝ set_c_flag m t s_tmp2 carry in
103 (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
104 let s_tmp4 ≝ set_z_flag m t s_tmp3 (eq_b8 R_op 〈x0,x0〉) in
106 let s_tmp5 ≝ setweak_n_flag m t s_tmp4 (MSB_b8 R_op) in
108 let s_tmp6 ≝ setweak_v_flag m t s_tmp5 ((MSB_b8 R_op) ⊙ carry) in
110 Some ? (pair … s_tmp6 new_pc) ])]]).
112 (* estensione del segno byte → word *)
113 ndefinition byte_extension ≝
114 λb:byte8.〈match MSB_b8 b with [ true ⇒ 〈xF,xF〉 | false ⇒ 〈x0,x0〉 ]:b〉.
116 (* branch con byte+estensione segno *)
117 ndefinition branched_pc ≝
118 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λb:byte8.
119 get_pc_reg m t (set_pc_reg m t s (plus_w16_d_d cur_pc (byte_extension b))).
121 (* if COND=1 branch *)
122 (* tutti i branch calcoleranno la condizione e la passeranno qui *)
123 ndefinition execute_any_BRANCH ≝
124 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.λfCOND:bool.
125 opt_map … (multi_mode_load true m t s cur_pc i)
126 (λS_M_PC.match S_M_PC with
127 [ triple s_tmp1 M_op new_pc ⇒
128 (* if true, branch *)
130 (* newpc = nextpc + rel *)
131 [ true ⇒ Some ? (pair … s_tmp1 (branched_pc m t s_tmp1 new_pc M_op))
133 | false ⇒ Some ? (pair … s_tmp1 new_pc) ]]).
135 (* Mn = filtered optval *)
136 (* il chiamante passa 0x00 per azzerare, 0xFF per impostare il bit di M *)
137 ndefinition execute_BCLRn_BSETn_aux ≝
138 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.λoptval:byte8.
139 (* Mn = filtered optval *)
140 opt_map … (multi_mode_write true m t s cur_pc i optval)
141 (λS_PC.match S_PC with
143 [ pair s_tmp1 new_pc ⇒ Some ? (pair … s_tmp1 new_pc) ]).
145 (* if COND(Mn) branch *)
146 (* il chiamante passa la logica da testare (0x00,¬0x00) e poi si salta *)
147 ndefinition execute_BRCLRn_BRSETn_aux ≝
148 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.λfCOND:byte8 → bool.
149 opt_map … (multi_mode_load false m t s cur_pc i)
150 (λS_M_PC.match S_M_PC with
151 [ triple s_tmp1 M_op new_pc ⇒ match M_op with
152 [ mk_word16 MH_op ML_op ⇒
153 (* if COND(Mn) branch *)
154 match fCOND MH_op with
155 (* newpc = nextpc + rel *)
156 [ true ⇒ Some ? (pair … s_tmp1 (branched_pc m t s_tmp1 new_pc ML_op))
158 | false ⇒ Some ? (pair … s_tmp1 new_pc) ]]]).
161 (* fM e' la logica da applicare: not/neg/++/-- *)
162 ndefinition execute_COM_DEC_INC_NEG_aux ≝
163 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
164 λfM:byte8 → byte8.λfV:bool → bool → bool.λfC:bool → byte8 → bool.
165 opt_map … (multi_mode_load true m t s cur_pc i)
166 (λS_M_PC.match S_M_PC with
167 [ triple s_tmp1 M_op _ ⇒
168 let R_op ≝ fM M_op in
170 opt_map … (multi_mode_write true m t s_tmp1 cur_pc i R_op)
171 (λS_PC.match S_PC with
172 [ pair s_tmp2 new_pc ⇒
174 let s_tmp3 ≝ set_c_flag m t s_tmp2 (fC (get_c_flag m t s_tmp2) R_op) in
175 (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
176 let s_tmp4 ≝ set_z_flag m t s_tmp3 (eq_b8 R_op 〈x0,x0〉) in
178 let s_tmp5 ≝ setweak_n_flag m t s_tmp4 (MSB_b8 R_op) in
180 let s_tmp6 ≝ setweak_v_flag m t s_tmp5 (fV (MSB_b8 M_op) (MSB_b8 R_op)) in
182 Some ? (pair … s_tmp6 new_pc) ])]).
184 (* A = [true] fAMC(A,M,C), [false] A *)
185 (* cioe' in caso di false l'operazione viene eseguita ma modifica solo i flag *)
186 (* fAMC e' la logica da applicare: sottrazione con/senza carry *)
187 ndefinition execute_SBC_SUB_aux ≝
188 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.λsetflag:bool.
189 λfAMC:byte8 → byte8 → bool → ProdT byte8 bool.
190 opt_map … (multi_mode_load true m t s cur_pc i)
191 (λS_M_PC.match S_M_PC with
192 [ triple s_tmp1 M_op new_pc ⇒
193 let A_op ≝ get_acc_8_low_reg m t s_tmp1 in
194 match fAMC A_op M_op (get_c_flag m t s_tmp1) with
196 let A7 ≝ MSB_b8 A_op in let M7 ≝ MSB_b8 M_op in let R7 ≝ MSB_b8 R_op in
197 (* A = [true] fAMC(A,M,C), [false] A *)
198 let s_tmp2 ≝ match setflag with [ true ⇒ set_acc_8_low_reg m t s_tmp1 R_op | false ⇒ s_tmp1 ] in
199 (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
200 let s_tmp3 ≝ set_z_flag m t s_tmp2 (eq_b8 R_op 〈x0,x0〉) in
201 (* C = nA7&M7 | M7&R7 | R7&nA7 *)
202 let s_tmp4 ≝ set_c_flag m t s_tmp3 (((⊖A7)⊗M7) ⊕ (M7⊗R7) ⊕ (R7⊗(⊖A7))) in
204 let s_tmp5 ≝ setweak_n_flag m t s_tmp4 R7 in
205 (* V = A7&nM7&nR7 | nA7&M7&R7 *)
206 let s_tmp6 ≝ setweak_v_flag m t s_tmp5 ((A7⊗(⊖M7)⊗(⊖R7)) ⊕ ((⊖A7)⊗M7⊗R7)) in
208 Some ? (pair … s_tmp6 new_pc) ]]).
210 (* il classico push *)
211 ndefinition aux_push ≝
212 λm:mcu_type.λt:memory_impl.λs:any_status m t.λval:byte8.
213 opt_map … (get_sp_reg m t s)
215 (λSP_op.opt_map … (memory_filter_write m t s SP_op val)
217 (λs_tmp1.opt_map … (set_sp_reg m t s_tmp1 (pred_w16 SP_op))
218 (λs_tmp2.Some ? s_tmp2))).
220 (* il classico pop *)
221 (* NB: l'incremento di SP deve essere filtrato dalla ALU, quindi get(set(SP)) *)
222 ndefinition aux_pop ≝
223 λm:mcu_type.λt:memory_impl.λs:any_status m t.
224 opt_map … (get_sp_reg m t s)
226 (λSP_op.opt_map … (set_sp_reg m t s (succ_w16 SP_op))
227 (λs_tmp1.opt_map … (get_sp_reg m t s_tmp1)
229 (λSP_op'.opt_map … (memory_filter_read m t s_tmp1 SP_op')
230 (λval.Some ? (pair … s_tmp1 val))))).
232 (* CCR corrisponde a V11HINZC e cmq 1 se un flag non esiste *)
233 (* i flag mantengono posizione costante nelle varie ALU, e se non sono
234 implementati corrispondono a 1 *)
235 ndefinition aux_get_CCR ≝
236 λm:mcu_type.λt:memory_impl.λs:any_status m t.
237 let V_comp ≝ match get_v_flag m t s with
238 [ None ⇒ 〈x8,x0〉 | Some V_val ⇒ match V_val with [ true ⇒ 〈x8,x0〉 | false ⇒ 〈x0,x0〉 ]] in
239 let H_comp ≝ match get_h_flag m t s with
240 [ None ⇒ 〈x1,x0〉 | Some H_val ⇒ match H_val with [ true ⇒ 〈x1,x0〉 | false ⇒ 〈x0,x0〉 ]] in
241 let I_comp ≝ match get_i_flag m t s with
242 [ None ⇒ 〈x0,x8〉 | Some I_val ⇒ match I_val with [ true ⇒ 〈x0,x8〉 | false ⇒ 〈x0,x0〉 ]] in
243 let N_comp ≝ match get_n_flag m t s with
244 [ None ⇒ 〈x0,x4〉 | Some N_val ⇒ match N_val with [ true ⇒ 〈x0,x4〉 | false ⇒ 〈x0,x0〉 ]] in
245 let Z_comp ≝ match get_z_flag m t s with
246 [ true ⇒ 〈x0,x2〉 | false ⇒ 〈x0,x0〉 ] in
247 let C_comp ≝ match get_c_flag m t s with
248 [ true ⇒ 〈x0,x1〉 | false ⇒ 〈x0,x0〉 ] in
249 or_b8 〈x6,x0〉 (or_b8 V_comp (or_b8 H_comp (or_b8 I_comp (or_b8 N_comp (or_b8 Z_comp C_comp))))).
251 (* CCR corrisponde a V11HINZC *)
252 (* i flag mantengono posizione costante nelle varie ALU, e se non sono
253 implementati si puo' usare tranquillamente setweak *)
254 ndefinition aux_set_CCR ≝
255 λm:mcu_type.λt:memory_impl.λs:any_status m t.λCCR:byte8.
256 let s_tmp1 ≝ set_c_flag m t s (eq_b8 〈x0,x1〉 (and_b8 〈x0,x1〉 CCR)) in
257 let s_tmp2 ≝ set_z_flag m t s_tmp1 (eq_b8 〈x0,x2〉 (and_b8 〈x0,x2〉 CCR)) in
258 let s_tmp3 ≝ setweak_n_flag m t s_tmp2 (eq_b8 〈x0,x4〉 (and_b8 〈x0,x4〉 CCR)) in
259 let s_tmp4 ≝ setweak_i_flag m t s_tmp3 (eq_b8 〈x0,x8〉 (and_b8 〈x0,x8〉 CCR)) in
260 let s_tmp5 ≝ setweak_h_flag m t s_tmp4 (eq_b8 〈x1,x0〉 (and_b8 〈x1,x0〉 CCR)) in
261 let s_tmp6 ≝ setweak_v_flag m t s_tmp5 (eq_b8 〈x8,x0〉 (and_b8 〈x8,x0〉 CCR)) in
264 (* **************** *)
265 (* LOGICA DELLA ALU *)
266 (* **************** *)
269 ndefinition execute_ADC ≝
270 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
271 execute_ADC_ADD_aux m t s i cur_pc true (λA_op.λM_op.λC_op.plus_b8_dc_dc A_op M_op C_op).
274 ndefinition execute_ADD ≝
275 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
276 execute_ADC_ADD_aux m t s i cur_pc true (λA_op.λM_op.λC_op.plus_b8_dc_dc A_op M_op false).
278 (* SP += extended M *)
279 ndefinition execute_AIS ≝
280 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
281 opt_map … (multi_mode_load true m t s cur_pc i)
282 (λS_M_PC.match S_M_PC with
283 [ triple s_tmp1 M_op new_pc ⇒
284 opt_map … (get_sp_reg m t s_tmp1)
285 (* SP += extended M *)
286 (λSP_op.opt_map … (set_sp_reg m t s_tmp1 (plus_w16_d_d SP_op (byte_extension M_op)))
287 (λs_tmp2.Some ? (pair … s_tmp2 new_pc))) ]).
289 (* H:X += extended M *)
290 ndefinition execute_AIX ≝
291 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
292 opt_map … (multi_mode_load true m t s cur_pc i)
293 (λS_M_PC.match S_M_PC with
294 [ triple s_tmp1 M_op new_pc ⇒
295 opt_map … (get_indX_16_reg m t s_tmp1)
296 (* H:X += extended M *)
297 (λHX_op.opt_map … (set_indX_16_reg m t s_tmp1 (plus_w16_d_d HX_op (byte_extension M_op)))
298 (λs_tmp2.Some ? (pair … s_tmp2 new_pc))) ]).
301 ndefinition execute_AND ≝
302 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
303 execute_AND_BIT_EOR_ORA_aux m t s i cur_pc true and_b8.
305 (* M = C' <- rcl M <- 0 *)
306 ndefinition execute_ASL ≝
307 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
308 execute_ASL_ASR_LSR_ROL_ROR_aux m t s i cur_pc (λM_op.λC_op.rcl_b8 M_op false).
310 (* M = M7 -> rcr M -> C' *)
311 ndefinition execute_ASR ≝
312 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
313 execute_ASL_ASR_LSR_ROL_ROR_aux m t s i cur_pc (λM_op.λC_op.rcr_b8 M_op (MSB_b8 M_op)).
316 ndefinition execute_BCC ≝
317 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
318 execute_any_BRANCH m t s i cur_pc (⊖(get_c_flag m t s)).
321 ndefinition execute_BCLRn ≝
322 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
323 execute_BCLRn_BSETn_aux m t s i cur_pc 〈x0,x0〉.
326 ndefinition execute_BCS ≝
327 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
328 execute_any_BRANCH m t s i cur_pc (get_c_flag m t s).
331 ndefinition execute_BEQ ≝
332 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
333 execute_any_BRANCH m t s i cur_pc (get_z_flag m t s).
335 (* if N⊙V=0, branch *)
336 ndefinition execute_BGE ≝
337 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
338 opt_map … (get_n_flag m t s)
339 (λN_op.opt_map … (get_v_flag m t s)
340 (λV_op.execute_any_BRANCH m t s i cur_pc (⊖(N_op ⊙ V_op)))).
343 ndefinition execute_BGND ≝
344 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
345 Some ? (pair … s cur_pc).
347 (* if Z|N⊙V=0, branch *)
348 ndefinition execute_BGT ≝
349 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
350 opt_map … (get_n_flag m t s)
351 (λN_op.opt_map … (get_v_flag m t s)
352 (λV_op.execute_any_BRANCH m t s i cur_pc (⊖((get_z_flag m t s) ⊕ (N_op ⊙ V_op))))).
355 ndefinition execute_BHCC ≝
356 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
357 opt_map … (get_h_flag m t s)
358 (λH_op.execute_any_BRANCH m t s i cur_pc (⊖H_op)).
361 ndefinition execute_BHCS ≝
362 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
363 opt_map … (get_h_flag m t s)
364 (λH_op.execute_any_BRANCH m t s i cur_pc H_op).
366 (* if C|Z=0, branch *)
367 ndefinition execute_BHI ≝
368 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
369 execute_any_BRANCH m t s i cur_pc (⊖((get_c_flag m t s) ⊕ (get_z_flag m t s))).
371 (* if nIRQ=1, branch NB: irqflag e' un negato del pin *)
372 ndefinition execute_BIH ≝
373 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
374 opt_map … (get_irq_flag m t s)
375 (λIRQ_op.execute_any_BRANCH m t s i cur_pc (⊖IRQ_op)).
377 (* if nIRQ=0, branch NB: irqflag e' un negato del pin *)
378 ndefinition execute_BIL ≝
379 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
380 opt_map … (get_irq_flag m t s)
381 (λIRQ_op.execute_any_BRANCH m t s i cur_pc IRQ_op).
384 ndefinition execute_BIT ≝
385 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
386 execute_AND_BIT_EOR_ORA_aux m t s i cur_pc false and_b8.
388 (* if Z|N⊙V=1, branch *)
389 ndefinition execute_BLE ≝
390 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
391 opt_map … (get_n_flag m t s)
392 (λN_op.opt_map … (get_v_flag m t s)
393 (λV_op.execute_any_BRANCH m t s i cur_pc ((get_z_flag m t s) ⊕ (N_op ⊙ V_op)))).
395 (* if C|Z=1, branch *)
396 ndefinition execute_BLS ≝
397 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
398 execute_any_BRANCH m t s i cur_pc ((get_c_flag m t s) ⊕ (get_z_flag m t s)).
400 (* if N⊙V=1, branch *)
401 ndefinition execute_BLT ≝
402 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
403 opt_map … (get_n_flag m t s)
404 (λN_op.opt_map … (get_v_flag m t s)
405 (λV_op.execute_any_BRANCH m t s i cur_pc (N_op ⊙ V_op))).
408 ndefinition execute_BMC ≝
409 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
410 opt_map … (get_i_flag m t s)
411 (λI_op.execute_any_BRANCH m t s i cur_pc (⊖I_op)).
414 ndefinition execute_BMI ≝
415 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
416 opt_map … (get_n_flag m t s)
417 (λN_op.execute_any_BRANCH m t s i cur_pc N_op).
420 ndefinition execute_BMS ≝
421 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
422 opt_map … (get_i_flag m t s)
423 (λI_op.execute_any_BRANCH m t s i cur_pc I_op).
426 ndefinition execute_BNE ≝
427 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
428 execute_any_BRANCH m t s i cur_pc (⊖(get_z_flag m t s)).
431 ndefinition execute_BPL ≝
432 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
433 opt_map … (get_n_flag m t s)
434 (λN_op.execute_any_BRANCH m t s i cur_pc (⊖N_op)).
437 ndefinition execute_BRA ≝
438 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
439 execute_any_BRANCH m t s i cur_pc true.
442 ndefinition execute_BRCLRn ≝
443 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
444 execute_BRCLRn_BRSETn_aux m t s i cur_pc
445 (λMn_op.eq_b8 Mn_op 〈x0,x0〉).
447 (* branch never... come se fosse un nop da 2 byte *)
448 ndefinition execute_BRN ≝
449 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
450 execute_any_BRANCH m t s i cur_pc false.
453 ndefinition execute_BRSETn ≝
454 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
455 execute_BRCLRn_BRSETn_aux m t s i cur_pc
456 (λMn_op.⊖(eq_b8 Mn_op 〈x0,x0〉)).
459 ndefinition execute_BSETn ≝
460 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
461 execute_BCLRn_BSETn_aux m t s i cur_pc 〈xF,xF〉.
463 (* branch to subroutine *)
464 (* HC05/HC08/HCS08 si appoggiano allo stack, RS08 a SPC *)
465 ndefinition execute_BSR ≝
466 λm:mcu_type.λt:memory_impl.λs:any_status m t .λi:instr_mode.λcur_pc:word16.
467 opt_map … (multi_mode_load true m t s cur_pc i)
468 (λS_M_PC.match S_M_PC with
469 [ triple s_tmp1 M_op new_pc ⇒ let aux ≝
470 (* push (new_pc low) *)
471 opt_map … (aux_push m t s_tmp1 (w16l new_pc))
472 (* push (new_pc high) *)
473 (λs_tmp2.opt_map … (aux_push m t s_tmp2 (w16h new_pc))
474 (* new_pc = new_pc + rel *)
475 (λs_tmp3.Some ? (pair … s_tmp3 (branched_pc m t s_tmp3 new_pc M_op))))
477 [ HC05 ⇒ aux | HC08 ⇒ aux | HCS08 ⇒ aux
480 opt_map … (set_spc_reg m t s_tmp1 new_pc)
481 (* new_pc = new_pc + rel *)
482 (λs_tmp2.Some ? (pair … s_tmp2 (branched_pc m t s_tmp2 new_pc M_op)))
486 ndefinition execute_CBEQA ≝
487 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
488 opt_map … (multi_mode_load false m t s cur_pc i)
489 (λS_M_PC.match S_M_PC with
490 [ triple s_tmp1 M_op new_pc ⇒
492 [ mk_word16 MH_op ML_op ⇒
494 match eq_b8 (get_acc_8_low_reg m t s_tmp1) MH_op with
495 (* new_pc = new_pc + rel *)
496 [ true ⇒ Some ? (pair … s_tmp1 (branched_pc m t s_tmp1 new_pc ML_op))
497 (* new_pc = new_pc *)
498 | false ⇒ Some ? (pair … s_tmp1 new_pc)
502 ndefinition execute_CBEQX ≝
503 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
504 opt_map … (multi_mode_load false m t s cur_pc i)
505 (λS_M_PC.match S_M_PC with
506 [ triple s_tmp1 M_op new_pc ⇒
508 [ mk_word16 MH_op ML_op ⇒
509 opt_map … (get_indX_8_low_reg m t s_tmp1)
511 (λX_op.match eq_b8 X_op MH_op with
512 (* new_pc = new_pc + rel *)
513 [ true ⇒ Some ? (pair … s_tmp1 (branched_pc m t s_tmp1 new_pc ML_op))
514 (* new_pc = new_pc *)
515 | false ⇒ Some ? (pair … s_tmp1 new_pc)
519 ndefinition execute_CLC ≝
520 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
521 Some ? (pair … (set_c_flag m t s false) cur_pc).
524 ndefinition execute_CLI ≝
525 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
526 opt_map … (set_i_flag m t s false)
527 (λs_tmp.Some ? (pair … s_tmp cur_pc)).
530 ndefinition execute_CLR ≝
531 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
533 opt_map … (multi_mode_write true m t s cur_pc i 〈x0,x0〉)
534 (λS_PC.match S_PC with
535 [ pair s_tmp1 new_pc ⇒
537 let s_tmp2 ≝ set_z_flag m t s_tmp1 true in
539 let s_tmp3 ≝ setweak_n_flag m t s_tmp2 false in
541 let s_tmp4 ≝ setweak_v_flag m t s_tmp3 false in
543 Some ? (pair … s_tmp4 new_pc) ]).
546 ndefinition execute_CMP ≝
547 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
548 execute_SBC_SUB_aux m t s i cur_pc false (λA_op.λM_op.λC_op.plus_b8_dc_dc A_op (compl_b8 M_op) false).
551 ndefinition execute_COM ≝
552 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
553 execute_COM_DEC_INC_NEG_aux m t s i cur_pc not_b8
559 (* flags = H:X - M *)
560 ndefinition execute_CPHX ≝
561 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
562 opt_map … (multi_mode_load false m t s cur_pc i)
563 (λS_M_PC.match S_M_PC with
564 [ triple s_tmp1 M_op new_pc ⇒
565 opt_map … (get_indX_16_reg m t s_tmp1)
567 match plus_w16_dc_dc X_op (compl_w16 M_op) false with
569 let X15 ≝ MSB_w16 X_op in let M15 ≝ MSB_w16 M_op in let R15 ≝ MSB_w16 R_op in
570 (* Z = nR15&nR14&nR13&nR12&nR11&nR10&nR9&nR8&nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
571 let s_tmp2 ≝ set_z_flag m t s_tmp1 (eq_w16 R_op 〈〈x0,x0〉:〈x0,x0〉〉) in
572 (* C = nX15&M15 | M15&R15 | R15&nX15 *)
573 let s_tmp3 ≝ set_c_flag m t s_tmp2 (((⊖X15)⊗M15) ⊕ (M15⊗R15) ⊕ (R15⊗(⊖X15))) in
575 let s_tmp4 ≝ setweak_n_flag m t s_tmp3 R15 in
576 (* V = X15&nM15&nR15 | nX15&M15&R15 *)
577 let s_tmp5 ≝ setweak_v_flag m t s_tmp4 ((X15⊗(⊖M15)⊗(⊖R15)) ⊕ ((⊖X15)⊗M15⊗R15)) in
579 Some ? (pair … s_tmp5 new_pc) ] ) ]).
582 ndefinition execute_CPX ≝
583 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
584 opt_map … (multi_mode_load true m t s cur_pc i)
585 (λS_M_PC.match S_M_PC with
586 [ triple s_tmp1 M_op new_pc ⇒
587 opt_map … (get_indX_8_low_reg m t s_tmp1)
589 match plus_b8_dc_dc X_op (compl_b8 M_op) false with
591 let X7 ≝ MSB_b8 X_op in let M7 ≝ MSB_b8 M_op in let R7 ≝ MSB_b8 R_op in
592 (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
593 let s_tmp2 ≝ set_z_flag m t s_tmp1 (eq_b8 R_op 〈x0,x0〉) in
594 (* C = nX7&M7 | M7&R7 | R7&nX7 *)
595 let s_tmp3 ≝ set_c_flag m t s_tmp2 (((⊖X7)⊗M7) ⊕ (M7⊗R7) ⊕ (R7⊗(⊖X7))) in
597 let s_tmp4 ≝ setweak_n_flag m t s_tmp3 R7 in
598 (* V = X7&nM7&nR7 | nX7&M7&R7 *)
599 let s_tmp5 ≝ setweak_v_flag m t s_tmp4 ((X7⊗(⊖M7)⊗(⊖R7)) ⊕ ((⊖X7)⊗M7⊗R7)) in
601 Some ? (pair … s_tmp5 new_pc) ] ) ]).
603 (* decimal adjiust A *)
604 (* per i dettagli vedere daa_b8 (modulo byte8) *)
605 ndefinition execute_DAA ≝
606 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
607 opt_map … (get_h_flag m t s)
609 let M_op ≝ get_acc_8_low_reg m t s in
610 match daa_b8 H (get_c_flag m t s) M_op with
613 let s_tmp1 ≝ set_acc_8_low_reg m t s R_op in
614 (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
615 let s_tmp2 ≝ set_z_flag m t s_tmp1 (eq_b8 R_op 〈x0,x0〉) in
617 let s_tmp3 ≝ set_c_flag m t s_tmp2 carry in
619 let s_tmp4 ≝ setweak_n_flag m t s_tmp3 (MSB_b8 R_op) in
621 let s_tmp5 ≝ setweak_v_flag m t s_tmp4 ((MSB_b8 M_op) ⊙ (MSB_b8 R_op)) in
623 Some ? (pair … s_tmp5 cur_pc) ]).
625 (* if (--M)≠0, branch *)
626 ndefinition execute_DBNZ ≝
627 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
628 opt_map … (multi_mode_load false m t s cur_pc i)
629 (λS_M_PC.match S_M_PC with
630 [ triple s_tmp1 M_op new_pc ⇒
632 [ mk_word16 MH_op ML_op ⇒
634 let MH_op' ≝ pred_b8 MH_op in
635 opt_map … (multi_mode_write true m t s_tmp1 cur_pc i MH_op')
636 (λS_PC.match S_PC with
638 (* if (--M)≠0, branch *)
639 match eq_b8 MH_op' 〈x0,x0〉 with
640 (* new_pc = new_pc *)
641 [ true ⇒ Some ? (pair … s_tmp2 new_pc)
642 (* new_pc = new_pc + rel *)
643 | false ⇒ Some ? (pair … s_tmp2 (branched_pc m t s_tmp2 new_pc ML_op)) ]])]]).
646 ndefinition execute_DEC ≝
647 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
648 execute_COM_DEC_INC_NEG_aux m t s i cur_pc pred_b8
654 (* A = H:A/X, H = H:AmodX se non c'e' overflow, altrimenti invariati *)
655 (* per i dettagli vedere div_b8 (modulo word16) *)
656 ndefinition execute_DIV ≝
657 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
658 opt_map … (get_indX_8_high_reg m t s)
659 (λH_op.opt_map … (get_indX_8_low_reg m t s)
660 (λX_op.match div_b8 〈H_op:(get_acc_8_low_reg m t s)〉 X_op with
661 [ triple quoz rest overflow ⇒
663 let s_tmp1 ≝ set_c_flag m t s overflow in
665 let s_tmp2 ≝ match overflow with
667 | false ⇒ set_acc_8_low_reg m t s_tmp1 quoz ] in
668 (* Z = nA7&nA6&nA5&nA4&nA3&nA2&nA1&nA0 *)
669 (* NB: che A sia cambiato o no, lo testa *)
670 let s_tmp3 ≝ set_z_flag m t s_tmp2 (eq_b8 (get_acc_8_low_reg m t s_tmp2) 〈x0,x0〉) in
671 (* H = H o H:AmodX *)
672 opt_map … (match overflow with
673 [ true ⇒ Some ? s_tmp3
674 | false ⇒ set_indX_8_high_reg m t s_tmp3 rest])
675 (λs_tmp4.Some ? (pair … s_tmp4 cur_pc)) ])).
678 ndefinition execute_EOR ≝
679 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
680 execute_AND_BIT_EOR_ORA_aux m t s i cur_pc true xor_b8.
683 ndefinition execute_INC ≝
684 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
685 execute_COM_DEC_INC_NEG_aux m t s i cur_pc succ_b8
691 (* jmp, il nuovo indirizzo e' una WORD *)
692 ndefinition execute_JMP ≝
693 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
694 opt_map … (multi_mode_load false m t s cur_pc i)
697 Some ? (pair … (fst3T ??? S_M_PC) (snd3T ??? S_M_PC))).
699 (* jump to subroutine *)
700 (* HC05/HC08/HCS08 si appoggiano allo stack, RS08 a SPC *)
701 ndefinition execute_JSR ≝
702 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
703 opt_map … (multi_mode_load false m t s cur_pc i)
704 (λS_M_PC.match S_M_PC with
705 [ triple s_tmp1 M_op new_pc ⇒ let aux ≝
706 (* push (new_pc low) *)
707 opt_map … (aux_push m t s_tmp1 (w16l new_pc))
708 (* push (new_pc high) *)
709 (λs_tmp2.opt_map … (aux_push m t s_tmp2 (w16h new_pc))
711 (λs_tmp3.Some ? (pair … s_tmp3 M_op)))
713 [ HC05 ⇒ aux | HC08 ⇒ aux | HCS08 ⇒ aux
716 opt_map … (set_spc_reg m t s_tmp1 new_pc)
718 (λs_tmp2.Some ? (pair … s_tmp2 M_op))
722 ndefinition execute_LDA ≝
723 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
724 opt_map … (multi_mode_load true m t s cur_pc i)
725 (λS_M_PC.match S_M_PC with
726 [ triple s_tmp1 M_op new_pc ⇒
728 let s_tmp2 ≝ set_acc_8_low_reg m t s_tmp1 M_op in
729 (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
730 let s_tmp3 ≝ set_z_flag m t s_tmp2 (eq_b8 M_op 〈x0,x0〉) in
732 let s_tmp4 ≝ setweak_n_flag m t s_tmp3 (MSB_b8 M_op) in
734 let s_tmp5 ≝ setweak_v_flag m t s_tmp4 false in
736 Some ? (pair … s_tmp5 new_pc) ]).
739 ndefinition execute_LDHX ≝
740 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
741 opt_map … (multi_mode_load false m t s cur_pc i)
742 (λS_M_PC.match S_M_PC with
743 [ triple s_tmp1 M_op new_pc ⇒
744 opt_map … (set_indX_16_reg m t s_tmp1 M_op)
746 (* Z = nR15&nR14&nR13nR12&nR11&nR10&nR9&nR8nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
747 let s_tmp3 ≝ set_z_flag m t s_tmp2 (eq_w16 M_op 〈〈x0,x0〉:〈x0,x0〉〉) in
749 let s_tmp4 ≝ setweak_n_flag m t s_tmp3 (MSB_w16 M_op) in
751 let s_tmp5 ≝ setweak_v_flag m t s_tmp4 false in
753 Some ? (pair … s_tmp5 new_pc)) ]).
756 ndefinition execute_LDX ≝
757 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
758 opt_map … (multi_mode_load true m t s cur_pc i)
759 (λS_M_PC.match S_M_PC with
760 [ triple s_tmp1 M_op new_pc ⇒
761 opt_map … (set_indX_8_low_reg m t s_tmp1 M_op)
763 (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
764 let s_tmp3 ≝ set_z_flag m t s_tmp2 (eq_b8 M_op 〈x0,x0〉) in
766 let s_tmp4 ≝ setweak_n_flag m t s_tmp3 (MSB_b8 M_op) in
768 let s_tmp5 ≝ setweak_v_flag m t s_tmp4 false in
770 Some ? (pair … s_tmp5 new_pc)) ]).
772 (* M = 0 -> rcr M -> C' *)
773 ndefinition execute_LSR ≝
774 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
775 execute_ASL_ASR_LSR_ROL_ROR_aux m t s i cur_pc (λM_op.λC_op.rcr_b8 M_op false).
778 ndefinition execute_MOV ≝
779 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
781 opt_map … (multi_mode_load true m t s cur_pc i)
782 (λS_R_PC.match S_R_PC with
783 [ triple s_tmp1 R_op tmp_pc ⇒
785 opt_map … (multi_mode_write true m t s_tmp1 tmp_pc i R_op)
786 (λS_PC.match S_PC with
787 [ pair s_tmp2 new_pc ⇒
788 (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
789 let s_tmp3 ≝ set_z_flag m t s_tmp2 (eq_b8 R_op 〈x0,x0〉) in
791 let s_tmp4 ≝ setweak_n_flag m t s_tmp3 (MSB_b8 R_op) in
793 let s_tmp5 ≝ setweak_v_flag m t s_tmp4 false in
795 Some ? (pair … s_tmp5 new_pc)])]).
798 ndefinition execute_MUL ≝
799 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
800 opt_map … (get_indX_8_low_reg m t s)
801 (λX_op.let R_op ≝ mul_b8 X_op (get_acc_8_low_reg m t s) in
802 opt_map … (set_indX_8_low_reg m t s (w16h R_op))
803 (λs_tmp.Some ? (pair … (set_acc_8_low_reg m t s_tmp (w16l R_op)) cur_pc))).
806 ndefinition execute_NEG ≝
807 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
808 execute_COM_DEC_INC_NEG_aux m t s i cur_pc compl_b8
811 (* fC = R7|R6|R5|R4|R3|R2|R1|R0 *)
812 (λC_op.λR_op.⊖(eq_b8 R_op 〈x0,x0〉)).
815 ndefinition execute_NOP ≝
816 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
817 Some ? (pair … s cur_pc).
819 (* A = (mk_byte8 (b8l A) (b8h A)) *)
820 (* cioe' swap del nibble alto/nibble basso di A *)
821 ndefinition execute_NSA ≝
822 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
823 match get_acc_8_low_reg m t s with [ mk_byte8 ah al ⇒
824 (* A = (mk_byte8 (b8l A) (b8h A)) *)
825 Some ? (pair … (set_acc_8_low_reg m t s 〈al,ah〉) cur_pc) ].
828 ndefinition execute_ORA ≝
829 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
830 execute_AND_BIT_EOR_ORA_aux m t s i cur_pc true or_b8.
833 ndefinition execute_PSHA ≝
834 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
835 opt_map … (aux_push m t s (get_acc_8_low_reg m t s))
836 (λs_tmp1.Some ? (pair … s_tmp1 cur_pc)).
839 ndefinition execute_PSHH ≝
840 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
841 opt_map … (get_indX_8_high_reg m t s)
842 (λH_op.opt_map … (aux_push m t s H_op)
843 (λs_tmp1.Some ? (pair … s_tmp1 cur_pc))).
846 ndefinition execute_PSHX ≝
847 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
848 opt_map … (get_indX_8_low_reg m t s)
849 (λH_op.opt_map … (aux_push m t s H_op)
850 (λs_tmp1.Some ? (pair … s_tmp1 cur_pc))).
853 ndefinition execute_PULA ≝
854 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
855 opt_map … (aux_pop m t s)
856 (λS_and_A.match S_and_A with [ pair s_tmp1 A_op ⇒
857 Some ? (pair … (set_acc_8_low_reg m t s_tmp1 A_op) cur_pc) ]).
860 ndefinition execute_PULH ≝
861 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
862 opt_map … (aux_pop m t s)
863 (λS_and_H.match S_and_H with [ pair s_tmp1 H_op ⇒
864 opt_map … (set_indX_8_high_reg m t s_tmp1 H_op)
865 (λs_tmp2.Some ? (pair … s_tmp2 cur_pc))]).
868 ndefinition execute_PULX ≝
869 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
870 opt_map … (aux_pop m t s)
871 (λS_and_X.match S_and_X with [ pair s_tmp1 X_op ⇒
872 opt_map … (set_indX_8_low_reg m t s_tmp1 X_op)
873 (λs_tmp2.Some ? (pair … s_tmp2 cur_pc))]).
875 (* M = C' <- rcl M <- C *)
876 ndefinition execute_ROL ≝
877 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
878 execute_ASL_ASR_LSR_ROL_ROR_aux m t s i cur_pc (λM_op.λC_op.rcl_b8 M_op C_op).
880 (* M = C -> rcr M -> C' *)
881 ndefinition execute_ROR ≝
882 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
883 execute_ASL_ASR_LSR_ROL_ROR_aux m t s i cur_pc (λM_op.λC_op.rcr_b8 M_op C_op).
886 (* lascia inalterato il byte superiore di SP *)
887 ndefinition execute_RSP ≝
888 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
889 opt_map … (get_sp_reg m t s)
890 (λSP_op.match SP_op with [ mk_word16 sph spl ⇒
891 opt_map … (set_sp_reg m t s 〈sph:〈xF,xF〉〉)
892 (λs_tmp.Some ? (pair … s_tmp cur_pc))]).
894 (* return from interrupt *)
895 ndefinition execute_RTI ≝
896 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
898 opt_map … (aux_pop m t s)
899 (λS_and_CCR.match S_and_CCR with [ pair s_tmp1 CCR_op ⇒
900 let s_tmp2 ≝ aux_set_CCR m t s_tmp1 CCR_op in
902 opt_map … (aux_pop m t s_tmp2)
903 (λS_and_A.match S_and_A with [ pair s_tmp3 A_op ⇒
904 let s_tmp4 ≝ set_acc_8_low_reg m t s_tmp3 A_op in
906 opt_map … (aux_pop m t s_tmp4)
907 (λS_and_X.match S_and_X with [ pair s_tmp5 X_op ⇒
908 opt_map … (set_indX_8_low_reg m t s_tmp5 X_op)
910 (λs_tmp6.opt_map … (aux_pop m t s_tmp6)
911 (λS_and_PCH.match S_and_PCH with [ pair s_tmp7 PCH_op ⇒
913 opt_map … (aux_pop m t s_tmp7)
914 (λS_and_PCL.match S_and_PCL with [ pair s_tmp8 PCL_op ⇒
915 Some ? (pair … s_tmp8 〈PCH_op:PCL_op〉)])]))])])]).
917 (* return from subroutine *)
918 (* HC05/HC08/HCS08 si appoggia allo stack, RS08 si appoggia a SPC *)
919 ndefinition execute_RTS ≝
920 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
923 opt_map … (aux_pop m t s)
924 (λS_and_PCH.match S_and_PCH with [ pair s_tmp1 PCH_op ⇒
926 opt_map … (aux_pop m t s_tmp1)
927 (λS_and_PCL.match S_and_PCL with [ pair s_tmp2 PCL_op ⇒
928 Some ? (pair … s_tmp2 〈PCH_op:PCL_op〉)])])
930 [ HC05 ⇒ aux | HC08 ⇒ aux | HCS08 ⇒ aux
933 opt_map … (get_spc_reg m t s)
934 (λSPC_op.Some ? (pair … s SPC_op))
938 ndefinition execute_SBC ≝
939 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
940 execute_SBC_SUB_aux m t s i cur_pc true
941 (λA_op.λM_op.λC_op.match plus_b8_dc_dc A_op (compl_b8 M_op) false with
942 [ pair resb resc ⇒ match C_op with
943 [ true ⇒ plus_b8_dc_dc resb 〈xF,xF〉 false
944 | false ⇒ pair … resb resc ]]).
947 ndefinition execute_SEC ≝
948 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
949 Some ? (pair … (set_c_flag m t s true) cur_pc).
952 ndefinition execute_SEI ≝
953 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
954 opt_map … (set_i_flag m t s true)
955 (λs_tmp.Some ? (pair … s_tmp cur_pc)).
958 (* senso: nell'RS08 SPC non e' accessibile direttamente e come si possono
959 fare subroutine annidate se RA (return address) e' salvato sempre in SPC?
960 occore accedere a SPC e salvarne il contenuto *)
961 ndefinition execute_SHA ≝
962 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
963 opt_map … (get_spc_reg m t s)
964 (λSPC_op.opt_map … (set_spc_reg m t s 〈(get_acc_8_low_reg m t s):(w16l SPC_op)〉)
965 (λs_tmp1.Some ? (pair … (set_acc_8_low_reg m t s_tmp1 (w16h SPC_op)) cur_pc))).
968 (* senso: nell'RS08 SPC non e' accessibile direttamente e come si possono
969 fare subroutine annidate se RA (return address) e' salvato sempre in SPC?
970 occore accedere a SPC e salvarne il contenuto *)
971 ndefinition execute_SLA ≝
972 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
973 opt_map … (get_spc_reg m t s)
974 (λSPC_op.opt_map … (set_spc_reg m t s 〈(w16h SPC_op):(get_acc_8_low_reg m t s)〉)
975 (λs_tmp1.Some ? (pair … (set_acc_8_low_reg m t s_tmp1 (w16l SPC_op)) cur_pc))).
978 ndefinition execute_STA ≝
979 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
981 let A_op ≝ (get_acc_8_low_reg m t s) in
982 opt_map … (multi_mode_write true m t s cur_pc i A_op)
983 (λS_op_and_PC.match S_op_and_PC with
984 [ pair s_tmp1 new_pc ⇒
985 (* Z = nA7&nA6&nA5&nA4&nA3&nA2&nA1&nA0 *)
986 let s_tmp2 ≝ set_z_flag m t s_tmp1 (eq_b8 A_op 〈x0,x0〉) in
988 let s_tmp3 ≝ setweak_n_flag m t s_tmp2 (MSB_b8 A_op) in
990 let s_tmp4 ≝ setweak_v_flag m t s_tmp3 false in
992 Some ? (pair … s_tmp4 new_pc) ]).
995 ndefinition execute_STHX ≝
996 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
998 opt_map … (get_indX_16_reg m t s)
999 (λX_op.opt_map … (multi_mode_write false m t s cur_pc i X_op)
1000 (λS_op_and_PC.match S_op_and_PC with
1001 [ pair s_tmp1 new_pc ⇒
1002 (* Z = nR15&nR14&nR13nR12&nR11&nR10&nR9&nR8nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
1003 let s_tmp2 ≝ set_z_flag m t s_tmp1 (eq_w16 X_op 〈〈x0,x0〉:〈x0,x0〉〉) in
1005 let s_tmp3 ≝ setweak_n_flag m t s_tmp2 (MSB_w16 X_op) in
1007 let s_tmp4 ≝ setweak_v_flag m t s_tmp3 false in
1008 (* newpc = nextpc *)
1009 Some ? (pair … s_tmp4 new_pc) ])).
1012 ndefinition execute_STOP ≝
1013 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
1014 Some ? (pair … (setweak_i_flag m t s false) cur_pc).
1017 ndefinition execute_STX ≝
1018 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
1020 opt_map … (get_indX_8_low_reg m t s)
1021 (λX_op.opt_map … (multi_mode_write true m t s cur_pc i X_op)
1022 (λS_op_and_PC.match S_op_and_PC with
1023 [ pair s_tmp1 new_pc ⇒
1024 (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
1025 let s_tmp2 ≝ set_z_flag m t s_tmp1 (eq_b8 X_op 〈x0,x0〉) in
1027 let s_tmp3 ≝ setweak_n_flag m t s_tmp2 (MSB_b8 X_op) in
1029 let s_tmp4 ≝ setweak_v_flag m t s_tmp3 false in
1030 (* newpc = nextpc *)
1031 Some ? (pair … s_tmp4 new_pc) ])).
1034 ndefinition execute_SUB ≝
1035 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
1036 execute_SBC_SUB_aux m t s i cur_pc true (λA_op.λM_op.λC_op.plus_b8_dc_dc A_op (compl_b8 M_op) false).
1038 (* software interrupt *)
1039 ndefinition execute_SWI ≝
1040 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
1041 (* indirizzo da cui caricare il nuovo pc *)
1042 let vector ≝ get_pc_reg m t (set_pc_reg m t s 〈〈xF,xF〉:〈xF,xC〉〉) in
1043 (* push (cur_pc low) *)
1044 opt_map … (aux_push m t s (w16l cur_pc))
1045 (* push (cur_pc high *)
1046 (λs_tmp1.opt_map … (aux_push m t s_tmp1 (w16h cur_pc))
1047 (λs_tmp2.opt_map … (get_indX_8_low_reg m t s_tmp2)
1049 (λX_op.opt_map … (aux_push m t s_tmp2 X_op)
1051 (λs_tmp3.opt_map … (aux_push m t s_tmp3 (get_acc_8_low_reg m t s_tmp3))
1053 (λs_tmp4.opt_map … (aux_push m t s_tmp4 (aux_get_CCR m t s_tmp4))
1055 (λs_tmp5.opt_map … (set_i_flag m t s_tmp5 true)
1056 (* load from vector high *)
1057 (λs_tmp6.opt_map … (memory_filter_read m t s_tmp6 vector)
1058 (* load from vector low *)
1059 (λaddrh.opt_map … (memory_filter_read m t s_tmp6 (succ_w16 vector))
1060 (* newpc = [vector] *)
1061 (λaddrl.Some ? (pair … s_tmp6 〈addrh:addrl〉)))))))))).
1064 ndefinition execute_TAP ≝
1065 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
1066 Some ? (pair … (aux_set_CCR m t s (get_acc_8_low_reg m t s)) cur_pc).
1069 ndefinition execute_TAX ≝
1070 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
1071 opt_map … (set_indX_8_low_reg m t s (get_acc_8_low_reg m t s))
1072 (λs_tmp.Some ? (pair … s_tmp cur_pc)).
1075 ndefinition execute_TPA ≝
1076 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
1077 Some ? (pair … (set_acc_8_low_reg m t s (aux_get_CCR m t s)) cur_pc).
1080 (* implementata senza richiamare la sottrazione, la modifica dei flag
1082 ndefinition execute_TST ≝
1083 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
1084 opt_map … (multi_mode_load true m t s cur_pc i)
1085 (λS_M_PC.match S_M_PC with
1086 [ triple s_tmp1 M_op new_pc ⇒
1087 (* Z = nR7&nR6&nR5&nR4&nR3&nR2&nR1&nR0 *)
1088 let s_tmp2 ≝ set_z_flag m t s_tmp1 (eq_b8 M_op 〈x0,x0〉) in
1090 let s_tmp3 ≝ setweak_n_flag m t s_tmp2 (MSB_b8 M_op) in
1092 let s_tmp4 ≝ setweak_v_flag m t s_tmp3 false in
1093 (* newpc = nextpc *)
1094 Some ? (pair … s_tmp4 new_pc) ]).
1097 ndefinition execute_TSX ≝
1098 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
1099 opt_map … (get_sp_reg m t s )
1100 (λSP_op.opt_map … (set_indX_16_reg m t s (succ_w16 SP_op))
1102 (λs_tmp.Some ? (pair … s_tmp cur_pc))).
1105 ndefinition execute_TXA ≝
1106 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
1107 opt_map … (get_indX_8_low_reg m t s)
1108 (λX_op.Some ? (pair … (set_acc_8_low_reg m t s X_op) cur_pc)).
1111 ndefinition execute_TXS ≝
1112 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
1113 opt_map … (get_indX_16_reg m t s )
1114 (λX_op.opt_map … (set_sp_reg m t s (pred_w16 X_op))
1116 (λs_tmp.Some ? (pair … s_tmp cur_pc))).
1119 ndefinition execute_WAIT ≝
1120 λm:mcu_type.λt:memory_impl.λs:any_status m t.λi:instr_mode.λcur_pc:word16.
1121 Some ? (pair … (setweak_i_flag m t s false) cur_pc).
1127 (* enumerazione delle possibili modalita' di sospensione *)
1128 ninductive susp_type : Type ≝
1129 BGND_MODE: susp_type
1130 | STOP_MODE: susp_type
1131 | WAIT_MODE: susp_type.
1133 (* un tipo opzione ad hoc
1134 - errore: errore+stato (seguira' reset o …, cmq lo stato non va buttato)
1135 - sospensione: sospensione+stato (seguira' resume o …)
1138 ninductive tick_result (A:Type) : Type ≝
1139 TickERR : A → error_type → tick_result A
1140 | TickSUSP : A → susp_type → tick_result A
1141 | TickOK : A → tick_result A.
1143 (* sostanazialmente simula
1144 - fetch/decode/execute
1145 - l'esecuzione e' considerata atomica quindi nel caso di un'instruzione
1146 da 3 cicli la successione sara'
1147 ([fetch/decode] s,clk:None) →
1148 ( s,clk:Some 1,pseudo,mode,3,cur_pc) →
1149 ( s,clk:Some 2,pseudo,mode,3,cur_pc) →
1150 ([execute] s',clk:None) *)
1152 ndefinition tick_execute ≝
1153 λm:mcu_type.λt:memory_impl.λs:any_status m t.
1154 λpseudo:any_opcode m.λmode:instr_mode.λcur_pc:word16.
1155 let abs_pseudo ≝ match pseudo with [ anyOP pseudo' ⇒ pseudo' ] in
1156 let a_status_and_fetch ≝ match abs_pseudo with
1157 [ ADC ⇒ execute_ADC m t s mode cur_pc (* add with carry *)
1158 | ADD ⇒ execute_ADD m t s mode cur_pc (* add *)
1159 | AIS ⇒ execute_AIS m t s mode cur_pc (* add immediate to SP *)
1160 | AIX ⇒ execute_AIX m t s mode cur_pc (* add immediate to X *)
1161 | AND ⇒ execute_AND m t s mode cur_pc (* and *)
1162 | ASL ⇒ execute_ASL m t s mode cur_pc (* aritmetic shift left *)
1163 | ASR ⇒ execute_ASR m t s mode cur_pc (* aritmetic shift right *)
1164 | BCC ⇒ execute_BCC m t s mode cur_pc (* branch if C=0 *)
1165 | BCLRn ⇒ execute_BCLRn m t s mode cur_pc (* clear bit n *)
1166 | BCS ⇒ execute_BCS m t s mode cur_pc (* branch if C=1 *)
1167 | BEQ ⇒ execute_BEQ m t s mode cur_pc (* branch if Z=1 *)
1168 | BGE ⇒ execute_BGE m t s mode cur_pc (* branch if N⊙V=0 (great or equal) *)
1169 | BGND ⇒ execute_BGND m t s mode cur_pc (* !!background mode!!*)
1170 | BGT ⇒ execute_BGT m t s mode cur_pc (* branch if Z|N⊙V=0 clear (great) *)
1171 | BHCC ⇒ execute_BHCC m t s mode cur_pc (* branch if H=0 *)
1172 | BHCS ⇒ execute_BHCS m t s mode cur_pc (* branch if H=1 *)
1173 | BHI ⇒ execute_BHI m t s mode cur_pc (* branch if C|Z=0, (higher) *)
1174 | BIH ⇒ execute_BIH m t s mode cur_pc (* branch if nIRQ=1 *)
1175 | BIL ⇒ execute_BIL m t s mode cur_pc (* branch if nIRQ=0 *)
1176 | BIT ⇒ execute_BIT m t s mode cur_pc (* flag = and (bit test) *)
1177 | BLE ⇒ execute_BLE m t s mode cur_pc (* branch if Z|N⊙V=1 (less or equal) *)
1178 | BLS ⇒ execute_BLS m t s mode cur_pc (* branch if C|Z=1 (lower or same) *)
1179 | BLT ⇒ execute_BLT m t s mode cur_pc (* branch if N⊙1=1 (less) *)
1180 | BMC ⇒ execute_BMC m t s mode cur_pc (* branch if I=0 (interrupt mask clear) *)
1181 | BMI ⇒ execute_BMI m t s mode cur_pc (* branch if N=1 (minus) *)
1182 | BMS ⇒ execute_BMS m t s mode cur_pc (* branch if I=1 (interrupt mask set) *)
1183 | BNE ⇒ execute_BNE m t s mode cur_pc (* branch if Z=0 *)
1184 | BPL ⇒ execute_BPL m t s mode cur_pc (* branch if N=0 (plus) *)
1185 | BRA ⇒ execute_BRA m t s mode cur_pc (* branch always *)
1186 | BRCLRn ⇒ execute_BRCLRn m t s mode cur_pc (* branch if bit n clear *)
1187 | BRN ⇒ execute_BRN m t s mode cur_pc (* branch never (nop) *)
1188 | BRSETn ⇒ execute_BRSETn m t s mode cur_pc (* branch if bit n set *)
1189 | BSETn ⇒ execute_BSETn m t s mode cur_pc (* set bit n *)
1190 | BSR ⇒ execute_BSR m t s mode cur_pc (* branch to subroutine *)
1191 | CBEQA ⇒ execute_CBEQA m t s mode cur_pc (* compare (A) and BEQ *)
1192 | CBEQX ⇒ execute_CBEQX m t s mode cur_pc (* compare (X) and BEQ *)
1193 | CLC ⇒ execute_CLC m t s mode cur_pc (* C=0 *)
1194 | CLI ⇒ execute_CLI m t s mode cur_pc (* I=0 *)
1195 | CLR ⇒ execute_CLR m t s mode cur_pc (* operand=0 *)
1196 | CMP ⇒ execute_CMP m t s mode cur_pc (* flag = sub (compare A) *)
1197 | COM ⇒ execute_COM m t s mode cur_pc (* not (1 complement) *)
1198 | CPHX ⇒ execute_CPHX m t s mode cur_pc (* flag = sub (compare H:X) *)
1199 | CPX ⇒ execute_CPX m t s mode cur_pc (* flag = sub (compare X) *)
1200 | DAA ⇒ execute_DAA m t s mode cur_pc (* decimal adjust A *)
1201 | DBNZ ⇒ execute_DBNZ m t s mode cur_pc (* dec and BNE *)
1202 | DEC ⇒ execute_DEC m t s mode cur_pc (* operand=operand-1 (decrement) *)
1203 | DIV ⇒ execute_DIV m t s mode cur_pc (* div *)
1204 | EOR ⇒ execute_EOR m t s mode cur_pc (* xor *)
1205 | INC ⇒ execute_INC m t s mode cur_pc (* operand=operand+1 (increment) *)
1206 | JMP ⇒ execute_JMP m t s mode cur_pc (* jmp word [operand] *)
1207 | JSR ⇒ execute_JSR m t s mode cur_pc (* jmp to subroutine *)
1208 | LDA ⇒ execute_LDA m t s mode cur_pc (* load in A *)
1209 | LDHX ⇒ execute_LDHX m t s mode cur_pc (* load in H:X *)
1210 | LDX ⇒ execute_LDX m t s mode cur_pc (* load in X *)
1211 | LSR ⇒ execute_LSR m t s mode cur_pc (* logical shift right *)
1212 | MOV ⇒ execute_MOV m t s mode cur_pc (* move *)
1213 | MUL ⇒ execute_MUL m t s mode cur_pc (* mul *)
1214 | NEG ⇒ execute_NEG m t s mode cur_pc (* neg (2 complement) *)
1215 | NOP ⇒ execute_NOP m t s mode cur_pc (* nop *)
1216 | NSA ⇒ execute_NSA m t s mode cur_pc (* nibble swap A (al:ah <- ah:al) *)
1217 | ORA ⇒ execute_ORA m t s mode cur_pc (* or *)
1218 | PSHA ⇒ execute_PSHA m t s mode cur_pc (* push A *)
1219 | PSHH ⇒ execute_PSHH m t s mode cur_pc (* push H *)
1220 | PSHX ⇒ execute_PSHX m t s mode cur_pc (* push X *)
1221 | PULA ⇒ execute_PULA m t s mode cur_pc (* pop A *)
1222 | PULH ⇒ execute_PULH m t s mode cur_pc (* pop H *)
1223 | PULX ⇒ execute_PULX m t s mode cur_pc (* pop X *)
1224 | ROL ⇒ execute_ROL m t s mode cur_pc (* rotate left *)
1225 | ROR ⇒ execute_ROR m t s mode cur_pc (* rotate right *)
1226 | RSP ⇒ execute_RSP m t s mode cur_pc (* reset SP (0x00FF) *)
1227 | RTI ⇒ execute_RTI m t s mode cur_pc (* return from interrupt *)
1228 | RTS ⇒ execute_RTS m t s mode cur_pc (* return from subroutine *)
1229 | SBC ⇒ execute_SBC m t s mode cur_pc (* sub with carry*)
1230 | SEC ⇒ execute_SEC m t s mode cur_pc (* C=1 *)
1231 | SEI ⇒ execute_SEI m t s mode cur_pc (* I=1 *)
1232 | SHA ⇒ execute_SHA m t s mode cur_pc (* swap spc_high,A *)
1233 | SLA ⇒ execute_SLA m t s mode cur_pc (* swap spc_low,A *)
1234 | STA ⇒ execute_STA m t s mode cur_pc (* store from A *)
1235 | STHX ⇒ execute_STHX m t s mode cur_pc (* store from H:X *)
1236 | STOP ⇒ execute_STOP m t s mode cur_pc (* !!stop mode!! *)
1237 | STX ⇒ execute_STX m t s mode cur_pc (* store from X *)
1238 | SUB ⇒ execute_SUB m t s mode cur_pc (* sub *)
1239 | SWI ⇒ execute_SWI m t s mode cur_pc (* software interrupt *)
1240 | TAP ⇒ execute_TAP m t s mode cur_pc (* flag=A (transfer A to process status byte *)
1241 | TAX ⇒ execute_TAX m t s mode cur_pc (* X=A (transfer A to X) *)
1242 | TPA ⇒ execute_TPA m t s mode cur_pc (* A=flag (transfer process status byte to A) *)
1243 | TST ⇒ execute_TST m t s mode cur_pc (* flag = sub (test) *)
1244 | TSX ⇒ execute_TSX m t s mode cur_pc (* X:H=SP (transfer SP to H:X) *)
1245 | TXA ⇒ execute_TXA m t s mode cur_pc (* A=X (transfer X to A) *)
1246 | TXS ⇒ execute_TXS m t s mode cur_pc (* SP=X:H (transfer H:X to SP) *)
1247 | WAIT ⇒ execute_WAIT m t s mode cur_pc (* !!wait mode!!*)
1248 ] in match a_status_and_fetch with
1249 (* errore nell'execute (=caricamento argomenti)? riportato in output *)
1250 (* nessun avanzamento e clk a None *)
1251 [ None ⇒ TickERR ? (set_clk_desc m t s (None ?)) ILL_EX_AD
1252 | Some status_and_newpc ⇒
1253 (* aggiornamento centralizzato di pc e clk *)
1254 match status_and_newpc with
1255 [ pair s_tmp1 new_pc ⇒
1256 let s_tmp2 ≝ set_pc_reg m t s_tmp1 new_pc in
1257 let s_tmp3 ≝ set_clk_desc m t s_tmp2 (None ?) in
1258 (* distinzione fra le 4 modalita' possibili, normale/BGND/STOP/WAIT *)
1259 match eq_op abs_pseudo BGND with
1260 [ true ⇒ TickSUSP ? s_tmp3 BGND_MODE
1261 | false ⇒ match eq_op abs_pseudo STOP with
1262 [ true ⇒ TickSUSP ? s_tmp3 STOP_MODE
1263 | false ⇒ match eq_op abs_pseudo WAIT with
1264 [ true ⇒ TickSUSP ? s_tmp3 WAIT_MODE
1265 | false ⇒ TickOK ? s_tmp3
1269 λm:mcu_type.λt:memory_impl.λs:any_status m t.
1270 let opt_info ≝ clk_desc m t s in
1272 (* e' il momento del fetch *)
1273 [ None ⇒ match fetch m t s with
1274 (* errore nel fetch/decode? riportato in output, nessun avanzamento *)
1275 [ FetchERR err ⇒ TickERR ? s err
1276 (* nessun errore nel fetch *)
1277 | FetchOK fetch_info cur_pc ⇒ match fetch_info with
1278 [ quadruple pseudo mode _ tot_clk ⇒
1279 match eq_b8 〈x0,x1〉 tot_clk with
1280 (* un solo clk, execute subito *)
1281 [ true ⇒ tick_execute m t s pseudo mode cur_pc
1282 (* piu' clk, execute rimandata *)
1283 | false ⇒ TickOK ? (set_clk_desc m t s (Some ? (quintuple … 〈x0,x1〉 pseudo mode tot_clk cur_pc)))
1287 (* il fetch e' gia' stato eseguito, e' il turno di execute? *)
1288 | Some info ⇒ match info with [ quintuple cur_clk pseudo mode tot_clk cur_pc ⇒
1289 match eq_b8 (succ_b8 cur_clk) tot_clk with
1291 [ true ⇒ tick_execute m t s pseudo mode cur_pc
1292 (* no, avanzamento cur_clk *)
1293 | false ⇒ TickOK ? (set_clk_desc m t s (Some ? (quintuple … (succ_b8 cur_clk) pseudo mode tot_clk cur_pc)))
1302 nlet rec execute (m:mcu_type) (t:memory_impl) (s:tick_result (any_status m t)) (n:nat) on n ≝
1304 [ TickERR s' error ⇒ TickERR ? s' error
1305 | TickSUSP s' susp ⇒ TickSUSP ? s' susp
1306 | TickOK s' ⇒ match n with [ O ⇒ TickOK ? s' | S n' ⇒ execute m t (tick m t s') n' ]