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/status/status.ma".
25 (* ***************************** *)
26 (* SETTER SPECIFICI FORTI/DEBOLI *)
27 (* ***************************** *)
29 (* funzione ausiliaria per il tipaggio dei setter forti *)
30 ndefinition aux_set_type ≝ λT:Type.λm:mcu_type.aux_alu_type m → T → aux_alu_type m.
32 (* funzione ausiliaria per il tipaggio dei setter deboli *)
33 ndefinition aux_set_type_opt ≝ λT:Type.λm:mcu_type.option (aux_set_type T m).
35 (* DESCRITTORI ESTERNI ALLA ALU *)
37 (* setter forte della ALU *)
39 λm:mcu_type.λt:memory_impl.λs:any_status m t.λalu'.
40 mk_any_status … alu' (mem_desc … s) (chk_desc … s) (clk_desc … s).
42 (* setter forte della memoria *)
43 ndefinition set_mem_desc ≝
44 λm:mcu_type.λt:memory_impl.λs:any_status m t.λmem':aux_mem_type t.
45 mk_any_status … (alu … s) mem' (chk_desc … s) (clk_desc … s).
47 (* setter forte del descrittore *)
48 ndefinition set_chk_desc ≝
49 λm:mcu_type.λt:memory_impl.λs:any_status m t.λchk':aux_chk_type t.
50 mk_any_status … (alu … s) (mem_desc … s) chk' (clk_desc … s).
52 (* setter forte del clik *)
53 ndefinition set_clk_desc ≝
54 λm:mcu_type.λt:memory_impl.λs:any_status m t.λclk':option (aux_clk_type m).
55 mk_any_status … (alu … s) (mem_desc … s) (chk_desc … s) clk'.
59 (* setter forte di A *)
60 ndefinition set_acc_8_low_reg ≝
61 λm:mcu_type.λt:memory_impl.λs:any_status m t.λval:byte8.
63 (match m return aux_set_type byte8 with
64 [ HC05 ⇒ set_acc_8_low_reg_HC05
65 | HC08 ⇒ set_acc_8_low_reg_HC08
66 | HCS08 ⇒ set_acc_8_low_reg_HC08
67 | RS08 ⇒ set_acc_8_low_reg_RS08
68 | IP2022 ⇒ set_acc_8_low_reg_IP2022
73 ndefinition set_indX_8_low_reg_sHC05 ≝
74 λt:memory_impl.λs:any_status HC05 t.λval.
75 set_alu … s (set_indX_8_low_reg_HC05 (alu … s) val).
77 ndefinition set_indX_8_low_reg_sHC08 ≝
78 λt:memory_impl.λs:any_status HC08 t.λval.
79 set_alu … s (set_indX_8_low_reg_HC08 (alu … s) val).
81 ndefinition set_indX_8_low_reg_sHCS08 ≝
82 λt:memory_impl.λs:any_status HCS08 t.λval.
83 set_alu … s (set_indX_8_low_reg_HC08 (alu … s) val).
85 (* setter forte di X *)
86 ndefinition set_indX_8_low_reg ≝
89 return λm.any_status m t → byte8 → option (any_status m t)
91 [ HC05 ⇒ λs:any_status ? t.λval.Some ? (set_indX_8_low_reg_sHC05 t s val)
92 | HC08 ⇒ λs:any_status ? t.λval.Some ? (set_indX_8_low_reg_sHC08 t s val)
93 | HCS08 ⇒ λs:any_status ? t.λval.Some ? (set_indX_8_low_reg_sHCS08 t s val)
94 | RS08 ⇒ λs:any_status ? t.λval.None ?
95 | IP2022 ⇒ λs:any_status ? t.λval.None ?
98 (* setter debole di X *)
99 ndefinition setweak_indX_8_low_reg ≝
100 λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
101 match set_indX_8_low_reg … s val with
102 [ None ⇒ s | Some s' ⇒ s' ].
106 ndefinition set_indX_8_high_reg_sHC08 ≝
107 λt:memory_impl.λs:any_status HC08 t.λval.
108 set_alu … s (set_indX_8_high_reg_HC08 (alu … s) val).
110 ndefinition set_indX_8_high_reg_sHCS08 ≝
111 λt:memory_impl.λs:any_status HCS08 t.λval.
112 set_alu … s (set_indX_8_high_reg_HC08 (alu … s) val).
114 (* setter forte di H *)
115 ndefinition set_indX_8_high_reg ≝
118 return λm.any_status m t → byte8 → option (any_status m t)
120 [ HC05 ⇒ λs:any_status ? t.λval.None ?
121 | HC08 ⇒ λs:any_status ? t.λval.Some ? (set_indX_8_high_reg_sHC08 t s val)
122 | HCS08 ⇒ λs:any_status ? t.λval.Some ? (set_indX_8_high_reg_sHCS08 t s val)
123 | RS08 ⇒ λs:any_status ? t.λval.None ?
124 | IP2022 ⇒ λs:any_status ? t.λval.None ?
127 (* setter debole di H *)
128 ndefinition setweak_indX_8_high_reg ≝
129 λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
130 match set_indX_8_high_reg … s val with
131 [ None ⇒ s | Some s' ⇒ s' ].
135 ndefinition set_indX_16_reg_sHC08 ≝
136 λt:memory_impl.λs:any_status HC08 t.λval.
137 set_alu … s (set_indX_16_reg_HC08 (alu … s) val).
139 ndefinition set_indX_16_reg_sHCS08 ≝
140 λt:memory_impl.λs:any_status HCS08 t.λval.
141 set_alu … s (set_indX_16_reg_HC08 (alu … s) val).
143 (* setter forte di H:X *)
144 ndefinition set_indX_16_reg ≝
147 return λm.any_status m t → word16 → option (any_status m t)
149 [ HC05 ⇒ λs:any_status ? t.λval.None ?
150 | HC08 ⇒ λs:any_status ? t.λval.Some ? (set_indX_16_reg_sHC08 t s val)
151 | HCS08 ⇒ λs:any_status ? t.λval.Some ? (set_indX_16_reg_sHCS08 t s val)
152 | RS08 ⇒ λs:any_status ? t.λval.None ?
153 | IP2022 ⇒ λs:any_status ? t.λval.None ?
156 (* setter debole di H:X *)
157 ndefinition setweak_indX_16_reg ≝
158 λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
159 match set_indX_16_reg … s val with
160 [ None ⇒ s | Some s' ⇒ s' ].
164 ndefinition set_sp_reg_sHC05 ≝
165 λt:memory_impl.λs:any_status HC05 t.λval.
166 set_alu … s (set_sp_reg_HC05 (alu … s) val).
168 ndefinition set_sp_reg_sHC08 ≝
169 λt:memory_impl.λs:any_status HC08 t.λval.
170 set_alu … s (set_sp_reg_HC08 (alu … s) val).
172 ndefinition set_sp_reg_sHCS08 ≝
173 λt:memory_impl.λs:any_status HCS08 t.λval.
174 set_alu … s (set_sp_reg_HC08 (alu … s) val).
176 ndefinition set_sp_reg_sIP2022 ≝
177 λt:memory_impl.λs:any_status IP2022 t.λval.
178 set_alu … s (set_sp_reg_IP2022 (alu … s) val).
180 (* setter forte di SP *)
181 ndefinition set_sp_reg ≝
184 return λm.any_status m t → word16 → option (any_status m t)
186 [ HC05 ⇒ λs:any_status ? t.λval.Some ? (set_sp_reg_sHC05 t s val)
187 | HC08 ⇒ λs:any_status ? t.λval.Some ? (set_sp_reg_sHC08 t s val)
188 | HCS08 ⇒ λs:any_status ? t.λval.Some ? (set_sp_reg_sHCS08 t s val)
189 | RS08 ⇒ λs:any_status ? t.λval.None ?
190 | IP2022 ⇒ λs:any_status ? t.λval.Some ? (set_sp_reg_sIP2022 t s val)
193 (* setter debole di SP *)
194 ndefinition setweak_sp_reg ≝
195 λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
196 match set_sp_reg … s val with
197 [ None ⇒ s | Some s' ⇒ s' ].
201 (* setter forte di PC *)
202 ndefinition set_pc_reg ≝
203 λm:mcu_type.λt:memory_impl.λs:any_status m t.λpc':word16.
205 (match m return aux_set_type word16 with
206 [ HC05 ⇒ set_pc_reg_HC05
207 | HC08 ⇒ set_pc_reg_HC08
208 | HCS08 ⇒ set_pc_reg_HC08
209 | RS08 ⇒ set_pc_reg_RS08
210 | IP2022 ⇒ set_pc_reg_IP2022
215 ndefinition set_spc_reg_sRS08 ≝
216 λt:memory_impl.λs:any_status RS08 t.λval.
217 set_alu … s (set_spc_reg_RS08 (alu … s) val).
219 (* setter forte di SPC *)
220 ndefinition set_spc_reg ≝
223 return λm.any_status m t → word16 → option (any_status m t)
225 [ HC05 ⇒ λs:any_status ? t.λval.None ?
226 | HC08 ⇒ λs:any_status ? t.λval.None ?
227 | HCS08 ⇒ λs:any_status ? t.λval.None ?
228 | RS08 ⇒ λs:any_status ? t.λval.Some ? (set_spc_reg_sRS08 t s val)
229 | IP2022 ⇒ λs:any_status ? t.λval.None ?
232 (* setter debole di SPC *)
233 ndefinition setweak_spc_reg ≝
234 λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
235 match set_spc_reg … s val with
236 [ None ⇒ s | Some s' ⇒ s' ].
240 ndefinition set_mulh_reg_sIP2022 ≝
241 λt:memory_impl.λs:any_status IP2022 t.λval.
242 set_alu … s (set_mulh_reg_IP2022 (alu … s) val).
244 (* setter forte di MULH *)
245 ndefinition set_mulh_reg ≝
248 return λm.any_status m t → byte8 → option (any_status m t)
250 [ HC05 ⇒ λs:any_status ? t.λval.None ?
251 | HC08 ⇒ λs:any_status ? t.λval.None ?
252 | HCS08 ⇒ λs:any_status ? t.λval.None ?
253 | RS08 ⇒ λs:any_status ? t.λval.None ?
254 | IP2022 ⇒ λs:any_status ? t.λval.Some ? (set_mulh_reg_sIP2022 t s val)
257 (* setter debole di MULH *)
258 ndefinition setweak_mulh_reg ≝
259 λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
260 match set_mulh_reg … s val with
261 [ None ⇒ s | Some s' ⇒ s' ].
263 (* REGISTRO ADDRSEL *)
265 ndefinition set_addrsel_reg_sIP2022 ≝
266 λt:memory_impl.λs:any_status IP2022 t.λval.
267 set_alu … s (set_addrsel_reg_IP2022 (alu … s) val).
269 (* setter forte di ADDRSEL *)
270 ndefinition set_addrsel_reg ≝
273 return λm.any_status m t → byte8 → option (any_status m t)
275 [ HC05 ⇒ λs:any_status ? t.λval.None ?
276 | HC08 ⇒ λs:any_status ? t.λval.None ?
277 | HCS08 ⇒ λs:any_status ? t.λval.None ?
278 | RS08 ⇒ λs:any_status ? t.λval.None ?
279 | IP2022 ⇒ λs:any_status ? t.λval.Some ? (set_addrsel_reg_sIP2022 t s val)
282 (* setter debole di ADDRSEL *)
283 ndefinition setweak_addrsel_reg ≝
284 λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
285 match set_addrsel_reg … s val with
286 [ None ⇒ s | Some s' ⇒ s' ].
290 ndefinition set_addr_reg_sIP2022 ≝
291 λt:memory_impl.λs:any_status IP2022 t.λval.
292 set_alu … s (set_addr_reg_IP2022 (alu … s) val).
294 (* setter forte di ADDR *)
295 ndefinition set_addr_reg ≝
298 return λm.any_status m t → word24 → option (any_status m t)
300 [ HC05 ⇒ λs:any_status ? t.λval.None ?
301 | HC08 ⇒ λs:any_status ? t.λval.None ?
302 | HCS08 ⇒ λs:any_status ? t.λval.None ?
303 | RS08 ⇒ λs:any_status ? t.λval.None ?
304 | IP2022 ⇒ λs:any_status ? t.λval.Some ? (set_addr_reg_sIP2022 t s val)
307 (* setter debole di ADDR *)
308 ndefinition setweak_addr_reg ≝
309 λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
310 match set_addr_reg … s val with
311 [ None ⇒ s | Some s' ⇒ s' ].
315 ndefinition set_call_reg_sIP2022 ≝
316 λt:memory_impl.λs:any_status IP2022 t.λval.
317 set_alu … s (set_call_reg_IP2022 (alu … s) val).
319 (* setter forte di CALL *)
320 ndefinition set_call_reg ≝
323 return λm.any_status m t → word16 → option (any_status m t)
325 [ HC05 ⇒ λs:any_status ? t.λval.None ?
326 | HC08 ⇒ λs:any_status ? t.λval.None ?
327 | HCS08 ⇒ λs:any_status ? t.λval.None ?
328 | RS08 ⇒ λs:any_status ? t.λval.None ?
329 | IP2022 ⇒ λs:any_status ? t.λval.Some ? (set_call_reg_sIP2022 t s val)
332 (* setter debole di CALL *)
333 ndefinition setweak_call_reg ≝
334 λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
335 match set_call_reg … s val with
336 [ None ⇒ s | Some s' ⇒ s' ].
338 (* REGISTRO CALL [push] *)
340 ndefinition push_call_reg_sIP2022 ≝
341 λt:memory_impl.λs:any_status IP2022 t.λval.
342 set_alu … s (push_call_reg_IP2022 (alu … s) val).
344 (* push forte di CALL *)
345 ndefinition push_call_reg ≝
348 return λm.any_status m t → word16 → option (any_status m t)
350 [ HC05 ⇒ λs:any_status ? t.λval.None ?
351 | HC08 ⇒ λs:any_status ? t.λval.None ?
352 | HCS08 ⇒ λs:any_status ? t.λval.None ?
353 | RS08 ⇒ λs:any_status ? t.λval.None ?
354 | IP2022 ⇒ λs:any_status ? t.λval.Some ? (push_call_reg_sIP2022 t s val)
357 (* REGISTRO CALL [pop] *)
359 ndefinition pop_call_reg_sIP2022 ≝
360 λt:memory_impl.λs:any_status IP2022 t.
361 match pop_call_reg_IP2022 (alu … s) with
362 [ pair val alu' ⇒ pair … val (set_alu … s alu') ].
364 (* pop forte di CALL *)
365 ndefinition pop_call_reg ≝
368 return λm.any_status m t → option (ProdT word16 (any_status m t))
370 [ HC05 ⇒ λs:any_status ? t.None ?
371 | HC08 ⇒ λs:any_status ? t.None ?
372 | HCS08 ⇒ λs:any_status ? t.None ?
373 | RS08 ⇒ λs:any_status ? t.None ?
374 | IP2022 ⇒ λs:any_status ? t.Some ? (pop_call_reg_sIP2022 t s)
379 ndefinition set_ip_reg_sIP2022 ≝
380 λt:memory_impl.λs:any_status IP2022 t.λval.
381 set_alu … s (set_ip_reg_IP2022 (alu … s) val).
383 (* setter forte di IP *)
384 ndefinition set_ip_reg ≝
387 return λm.any_status m t → word16 → option (any_status m t)
389 [ HC05 ⇒ λs:any_status ? t.λval.None ?
390 | HC08 ⇒ λs:any_status ? t.λval.None ?
391 | HCS08 ⇒ λs:any_status ? t.λval.None ?
392 | RS08 ⇒ λs:any_status ? t.λval.None ?
393 | IP2022 ⇒ λs:any_status ? t.λval.Some ? (set_ip_reg_sIP2022 t s val)
396 (* setter debole di IP *)
397 ndefinition setweak_ip_reg ≝
398 λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
399 match set_ip_reg … s val with
400 [ None ⇒ s | Some s' ⇒ s' ].
404 ndefinition set_dp_reg_sIP2022 ≝
405 λt:memory_impl.λs:any_status IP2022 t.λval.
406 set_alu … s (set_dp_reg_IP2022 (alu … s) val).
408 (* setter forte di DP *)
409 ndefinition set_dp_reg ≝
412 return λm.any_status m t → word16 → option (any_status m t)
414 [ HC05 ⇒ λs:any_status ? t.λval.None ?
415 | HC08 ⇒ λs:any_status ? t.λval.None ?
416 | HCS08 ⇒ λs:any_status ? t.λval.None ?
417 | RS08 ⇒ λs:any_status ? t.λval.None ?
418 | IP2022 ⇒ λs:any_status ? t.λval.Some ? (set_dp_reg_sIP2022 t s val)
421 (* setter debole di DP *)
422 ndefinition setweak_dp_reg ≝
423 λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
424 match set_dp_reg … s val with
425 [ None ⇒ s | Some s' ⇒ s' ].
429 ndefinition set_data_reg_sIP2022 ≝
430 λt:memory_impl.λs:any_status IP2022 t.λval.
431 set_alu … s (set_data_reg_IP2022 (alu … s) val).
433 (* setter forte di DATA *)
434 ndefinition set_data_reg ≝
437 return λm.any_status m t → word16 → option (any_status m t)
439 [ HC05 ⇒ λs:any_status ? t.λval.None ?
440 | HC08 ⇒ λs:any_status ? t.λval.None ?
441 | HCS08 ⇒ λs:any_status ? t.λval.None ?
442 | RS08 ⇒ λs:any_status ? t.λval.None ?
443 | IP2022 ⇒ λs:any_status ? t.λval.Some ? (set_data_reg_sIP2022 t s val)
446 (* setter debole di DATA *)
447 ndefinition setweak_data_reg ≝
448 λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
449 match set_data_reg … s val with
450 [ None ⇒ s | Some s' ⇒ s' ].
454 ndefinition set_speed_reg_sIP2022 ≝
455 λt:memory_impl.λs:any_status IP2022 t.λval.
456 set_alu … s (set_speed_reg_IP2022 (alu … s) val).
458 (* setter forte di SPEED *)
459 ndefinition set_speed_reg ≝
462 return λm.any_status m t → exadecim → option (any_status m t)
464 [ HC05 ⇒ λs:any_status ? t.λval.None ?
465 | HC08 ⇒ λs:any_status ? t.λval.None ?
466 | HCS08 ⇒ λs:any_status ? t.λval.None ?
467 | RS08 ⇒ λs:any_status ? t.λval.None ?
468 | IP2022 ⇒ λs:any_status ? t.λval.Some ? (set_speed_reg_sIP2022 t s val)
471 (* setter debole di SPEED *)
472 ndefinition setweak_speed_reg ≝
473 λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
474 match set_speed_reg … s val with
475 [ None ⇒ s | Some s' ⇒ s' ].
479 ndefinition set_page_reg_sIP2022 ≝
480 λt:memory_impl.λs:any_status IP2022 t.λval.
481 set_alu … s (set_page_reg_IP2022 (alu … s) val).
483 (* setter forte di PAGE *)
484 ndefinition set_page_reg ≝
487 return λm.any_status m t → oct → option (any_status m t)
489 [ HC05 ⇒ λs:any_status ? t.λval.None ?
490 | HC08 ⇒ λs:any_status ? t.λval.None ?
491 | HCS08 ⇒ λs:any_status ? t.λval.None ?
492 | RS08 ⇒ λs:any_status ? t.λval.None ?
493 | IP2022 ⇒ λs:any_status ? t.λval.Some ? (set_page_reg_sIP2022 t s val)
496 (* setter debole di PAGE *)
497 ndefinition setweak_page_reg ≝
498 λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
499 match set_page_reg … s val with
500 [ None ⇒ s | Some s' ⇒ s' ].
502 (* REGISTRO MEMORY MAPPED X *)
504 ndefinition set_x_map_sRS08 ≝
505 λt:memory_impl.λs:any_status RS08 t.λval.
506 set_alu … s (set_x_map_RS08 (alu … s) val).
508 (* setter forte di memory mapped X *)
509 ndefinition set_x_map ≝
512 return λm.any_status m t → byte8 → option (any_status m t)
514 [ HC05 ⇒ λs:any_status ? t.λval.None ?
515 | HC08 ⇒ λs:any_status ? t.λval.None ?
516 | HCS08 ⇒ λs:any_status ? t.λval.None ?
517 | RS08 ⇒ λs:any_status ? t.λval.Some ? (set_x_map_sRS08 t s val)
518 | IP2022 ⇒ λs:any_status ? t.λval.None ?
521 (* setter debole di memory mapped X *)
522 ndefinition setweak_x_map ≝
523 λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
524 match set_x_map … s val with
525 [ None ⇒ s | Some s' ⇒ s' ].
527 (* REGISTRO MEMORY MAPPED PS *)
529 ndefinition set_ps_map_sRS08 ≝
530 λt:memory_impl.λs:any_status RS08 t.λval.
531 set_alu … s (set_ps_map_RS08 (alu … s) val).
533 (* setter forte di memory mapped PS *)
534 ndefinition set_ps_map ≝
537 return λm.any_status m t → byte8 → option (any_status m t)
539 [ HC05 ⇒ λs:any_status ? t.λval.None ?
540 | HC08 ⇒ λs:any_status ? t.λval.None ?
541 | HCS08 ⇒ λs:any_status ? t.λval.None ?
542 | RS08 ⇒ λs:any_status ? t.λval.Some ? (set_ps_map_sRS08 t s val)
543 | IP2022 ⇒ λs:any_status ? t.λval.None ?
546 (* setter debole di memory mapped PS *)
547 ndefinition setweak_ps_map ≝
548 λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
549 match set_ps_map … s val with
550 [ None ⇒ s | Some s' ⇒ s' ].
554 ndefinition set_skip_mode_sIP2022 ≝
555 λt:memory_impl.λs:any_status IP2022 t.λval.
556 set_alu … s (set_skip_mode_IP2022 (alu … s) val).
558 (* setter forte di modalita SKIP *)
559 ndefinition set_skip_mode ≝
562 return λm.any_status m t → bool → option (any_status m t)
564 [ HC05 ⇒ λs:any_status ? t.λval.None ?
565 | HC08 ⇒ λs:any_status ? t.λval.None ?
566 | HCS08 ⇒ λs:any_status ? t.λval.None ?
567 | RS08 ⇒ λs:any_status ? t.λval.None ?
568 | IP2022 ⇒ λs:any_status ? t.λval.Some ? (set_skip_mode_sIP2022 t s val)
571 (* setter debole di SKIP *)
572 ndefinition setweak_skip_mode ≝
573 λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
574 match set_skip_mode … s val with
575 [ None ⇒ s | Some s' ⇒ s' ].
579 ndefinition set_v_flag_sHC08 ≝
580 λt:memory_impl.λs:any_status HC08 t.λval.
581 set_alu … s (set_v_flag_HC08 (alu … s) val).
583 ndefinition set_v_flag_sHCS08 ≝
584 λt:memory_impl.λs:any_status HCS08 t.λval.
585 set_alu … s (set_v_flag_HC08 (alu … s) val).
587 (* setter forte di V *)
588 ndefinition set_v_flag ≝
591 return λm.any_status m t → bool → option (any_status m t)
593 [ HC05 ⇒ λs:any_status ? t.λval.None ?
594 | HC08 ⇒ λs:any_status ? t.λval.Some ? (set_v_flag_sHC08 t s val)
595 | HCS08 ⇒ λs:any_status ? t.λval.Some ? (set_v_flag_sHCS08 t s val)
596 | RS08 ⇒ λs:any_status ? t.λval.None ?
597 | IP2022 ⇒ λs:any_status ? t.λval.None ?
600 (* setter debole di V *)
601 ndefinition setweak_v_flag ≝
602 λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
603 match set_v_flag … s val with
604 [ None ⇒ s | Some s' ⇒ s' ].
608 ndefinition set_h_flag_sHC05 ≝
609 λt:memory_impl.λs:any_status HC05 t.λval.
610 set_alu … s (set_h_flag_HC05 (alu … s) val).
612 ndefinition set_h_flag_sHC08 ≝
613 λt:memory_impl.λs:any_status HC08 t.λval.
614 set_alu … s (set_h_flag_HC08 (alu … s) val).
616 ndefinition set_h_flag_sHCS08 ≝
617 λt:memory_impl.λs:any_status HCS08 t.λval.
618 set_alu … s (set_h_flag_HC08 (alu … s) val).
620 ndefinition set_h_flag_sIP2022 ≝
621 λt:memory_impl.λs:any_status IP2022 t.λval.
622 set_alu … s (set_h_flag_IP2022 (alu … s) val).
624 (* setter forte di H *)
625 ndefinition set_h_flag ≝
628 return λm.any_status m t → bool → option (any_status m t)
630 [ HC05 ⇒ λs:any_status ? t.λval.Some ? (set_h_flag_sHC05 t s val)
631 | HC08 ⇒ λs:any_status ? t.λval.Some ? (set_h_flag_sHC08 t s val)
632 | HCS08 ⇒ λs:any_status ? t.λval.Some ? (set_h_flag_sHCS08 t s val)
633 | RS08 ⇒ λs:any_status ? t.λval.None ?
634 | IP2022 ⇒ λs:any_status ? t.λval.Some ? (set_h_flag_sIP2022 t s val)
637 (* setter debole di H *)
638 ndefinition setweak_h_flag ≝
639 λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
640 match set_h_flag … s val with
641 [ None ⇒ s | Some s' ⇒ s' ].
645 ndefinition set_i_flag_sHC05 ≝
646 λt:memory_impl.λs:any_status HC05 t.λval.
647 set_alu … s (set_i_flag_HC05 (alu … s) val).
649 ndefinition set_i_flag_sHC08 ≝
650 λt:memory_impl.λs:any_status HC08 t.λval.
651 set_alu … s (set_i_flag_HC08 (alu … s) val).
653 ndefinition set_i_flag_sHCS08 ≝
654 λt:memory_impl.λs:any_status HCS08 t.λval.
655 set_alu … s (set_i_flag_HC08 (alu … s) val).
657 (* setter forte di I *)
658 ndefinition set_i_flag ≝
661 return λm.any_status m t → bool → option (any_status m t)
663 [ HC05 ⇒ λs:any_status ? t.λval.Some ? (set_i_flag_sHC05 t s val)
664 | HC08 ⇒ λs:any_status ? t.λval.Some ? (set_i_flag_sHC08 t s val)
665 | HCS08 ⇒ λs:any_status ? t.λval.Some ? (set_i_flag_sHCS08 t s val)
666 | RS08 ⇒ λs:any_status ? t.λval.None ?
667 | IP2022 ⇒ λs:any_status ? t.λval.None ?
670 (* setter debole di I *)
671 ndefinition setweak_i_flag ≝
672 λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
673 match set_i_flag … s val with
674 [ None ⇒ s | Some s' ⇒ s' ].
678 ndefinition set_n_flag_sHC05 ≝
679 λt:memory_impl.λs:any_status HC05 t.λval.
680 set_alu … s (set_n_flag_HC05 (alu … s) val).
682 ndefinition set_n_flag_sHC08 ≝
683 λt:memory_impl.λs:any_status HC08 t.λval.
684 set_alu … s (set_n_flag_HC08 (alu … s) val).
686 ndefinition set_n_flag_sHCS08 ≝
687 λt:memory_impl.λs:any_status HCS08 t.λval.
688 set_alu … s (set_n_flag_HC08 (alu … s) val).
690 (* setter forte di N *)
691 ndefinition set_n_flag ≝
694 return λm.any_status m t → bool → option (any_status m t)
696 [ HC05 ⇒ λs:any_status ? t.λval.Some ? (set_n_flag_sHC05 t s val)
697 | HC08 ⇒ λs:any_status ? t.λval.Some ? (set_n_flag_sHC08 t s val)
698 | HCS08 ⇒ λs:any_status ? t.λval.Some ? (set_n_flag_sHCS08 t s val)
699 | RS08 ⇒ λs:any_status ? t.λval.None ?
700 | IP2022 ⇒ λs:any_status ? t.λval.None ?
703 (* setter debole di N *)
704 ndefinition setweak_n_flag ≝
705 λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
706 match set_n_flag … s val with
707 [ None ⇒ s | Some s' ⇒ s' ].
711 (* setter forte di Z *)
712 ndefinition set_z_flag ≝
713 λm:mcu_type.λt:memory_impl.λs:any_status m t.λzfl':bool.
715 (match m return aux_set_type bool with
716 [ HC05 ⇒ set_z_flag_HC05
717 | HC08 ⇒ set_z_flag_HC08
718 | HCS08 ⇒ set_z_flag_HC08
719 | RS08 ⇒ set_z_flag_RS08
720 | IP2022 ⇒ set_z_flag_IP2022
725 (* setter forte di C *)
726 ndefinition set_c_flag ≝
727 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcfl':bool.
729 (match m return aux_set_type bool with
730 [ HC05 ⇒ set_c_flag_HC05
731 | HC08 ⇒ set_c_flag_HC08
732 | HCS08 ⇒ set_c_flag_HC08
733 | RS08 ⇒ set_c_flag_RS08
734 | IP2022 ⇒ set_c_flag_IP2022
739 ndefinition set_irq_flag_sHC05 ≝
740 λt:memory_impl.λs:any_status HC05 t.λval.
741 set_alu … s (set_irq_flag_HC05 (alu … s) val).
743 ndefinition set_irq_flag_sHC08 ≝
744 λt:memory_impl.λs:any_status HC08 t.λval.
745 set_alu … s (set_irq_flag_HC08 (alu … s) val).
747 ndefinition set_irq_flag_sHCS08 ≝
748 λt:memory_impl.λs:any_status HCS08 t.λval.
749 set_alu … s (set_irq_flag_HC08 (alu … s) val).
751 (* setter forte di IRQ *)
752 ndefinition set_irq_flag ≝
755 return λm.any_status m t → bool → option (any_status m t)
757 [ HC05 ⇒ λs:any_status ? t.λval.Some ? (set_irq_flag_sHC05 t s val)
758 | HC08 ⇒ λs:any_status ? t.λval.Some ? (set_irq_flag_sHC08 t s val)
759 | HCS08 ⇒ λs:any_status ? t.λval.Some ? (set_irq_flag_sHCS08 t s val)
760 | RS08 ⇒ λs:any_status ? t.λval.None ?
761 | IP2022 ⇒ λs:any_status ? t.λval.None ?
764 (* setter debole di IRQ *)
765 ndefinition setweak_irq_flag ≝
766 λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
767 match set_irq_flag … s val with
768 [ None ⇒ s | Some s' ⇒ s' ].