(* funzione ausiliaria per il tipaggio dei setter forti *)
ndefinition aux_set_type ≝ λx:Type.λm:mcu_type.
- match m with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ]
+ match m with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08
+ | IP2022 ⇒ alu_IP2022 ]
→ x →
- match m with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ].
+ match m with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08
+ | IP2022 ⇒ alu_IP2022 ].
(* funzione ausiliaria per il tipaggio dei setter deboli *)
ndefinition aux_set_type_opt ≝ λx:Type.λm:mcu_type.option
- (match m with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ]
+ (match m with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08
+ | IP2022 ⇒ alu_IP2022 ]
→ x →
- match m with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ]).
+ match m with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08
+ | IP2022 ⇒ alu_IP2022 ]).
(* DESCRITTORI ESTERNI ALLA ALU *)
(* REGISTRO A *)
-(* setter specifico HC05 di A *)
-ndefinition set_acc_8_low_reg_HC05 ≝
-λalu.λacclow':byte8.
- mk_alu_HC05
- acclow'
- (indX_low_reg_HC05 alu)
- (sp_reg_HC05 alu)
- (sp_mask_HC05 alu)
- (sp_fix_HC05 alu)
- (pc_reg_HC05 alu)
- (pc_mask_HC05 alu)
- (h_flag_HC05 alu)
- (i_flag_HC05 alu)
- (n_flag_HC05 alu)
- (z_flag_HC05 alu)
- (c_flag_HC05 alu)
- (irq_flag_HC05 alu).
-
-(* setter specifico HC08/HCS08 di A *)
-ndefinition set_acc_8_low_reg_HC08 ≝
-λalu.λacclow':byte8.
- mk_alu_HC08
- acclow'
- (indX_low_reg_HC08 alu)
- (indX_high_reg_HC08 alu)
- (sp_reg_HC08 alu)
- (pc_reg_HC08 alu)
- (v_flag_HC08 alu)
- (h_flag_HC08 alu)
- (i_flag_HC08 alu)
- (n_flag_HC08 alu)
- (z_flag_HC08 alu)
- (c_flag_HC08 alu)
- (irq_flag_HC08 alu).
-
-(* setter specifico RS08 di A *)
-ndefinition set_acc_8_low_reg_RS08 ≝
-λalu.λacclow':byte8.
- mk_alu_RS08
- acclow'
- (pc_reg_RS08 alu)
- (pc_mask_RS08 alu)
- (spc_reg_RS08 alu)
- (x_map_RS08 alu)
- (ps_map_RS08 alu)
- (z_flag_RS08 alu)
- (c_flag_RS08 alu).
-
(* setter forte di A *)
ndefinition set_acc_8_low_reg ≝
-λm:mcu_type.λt:memory_impl.λs:any_status m t.λacclow':byte8.
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λval:byte8.
set_alu m t s
(match m return aux_set_type byte8 with
[ HC05 ⇒ set_acc_8_low_reg_HC05
| HC08 ⇒ set_acc_8_low_reg_HC08
| HCS08 ⇒ set_acc_8_low_reg_HC08
| RS08 ⇒ set_acc_8_low_reg_RS08
- ] (alu m t s) acclow').
+ | IP2022 ⇒ set_acc_8_low_reg_IP2022
+ ] (alu m t s) val).
(* REGISTRO X *)
-(* setter specifico HC05 di X *)
-ndefinition set_indX_8_low_reg_HC05 ≝
-λalu.λindxlow':byte8.
- mk_alu_HC05
- (acc_low_reg_HC05 alu)
- indxlow'
- (sp_reg_HC05 alu)
- (sp_mask_HC05 alu)
- (sp_fix_HC05 alu)
- (pc_reg_HC05 alu)
- (pc_mask_HC05 alu)
- (h_flag_HC05 alu)
- (i_flag_HC05 alu)
- (n_flag_HC05 alu)
- (z_flag_HC05 alu)
- (c_flag_HC05 alu)
- (irq_flag_HC05 alu).
-
-(* setter specifico HC08/HCS08 di X *)
-ndefinition set_indX_8_low_reg_HC08 ≝
-λalu.λindxlow':byte8.
- mk_alu_HC08
- (acc_low_reg_HC08 alu)
- indxlow'
- (indX_high_reg_HC08 alu)
- (sp_reg_HC08 alu)
- (pc_reg_HC08 alu)
- (v_flag_HC08 alu)
- (h_flag_HC08 alu)
- (i_flag_HC08 alu)
- (n_flag_HC08 alu)
- (z_flag_HC08 alu)
- (c_flag_HC08 alu)
- (irq_flag_HC08 alu).
+ndefinition set_indX_8_low_reg_sHC05 ≝
+λt:memory_impl.λs:any_status HC05 t.λval.
+ set_alu … s (set_indX_8_low_reg_HC05 (alu … s) val).
+
+ndefinition set_indX_8_low_reg_sHC08 ≝
+λt:memory_impl.λs:any_status HC08 t.λval.
+ set_alu … s (set_indX_8_low_reg_HC08 (alu … s) val).
+
+ndefinition set_indX_8_low_reg_sHCS08 ≝
+λt:memory_impl.λs:any_status HCS08 t.λval.
+ set_alu … s (set_indX_8_low_reg_HC08 (alu … s) val).
(* setter forte di X *)
ndefinition set_indX_8_low_reg ≝
-λm:mcu_type.λt:memory_impl.λs:any_status m t.λindxlow':byte8.
- opt_map … (match m return aux_set_type_opt byte8 with
- [ HC05 ⇒ Some ? set_indX_8_low_reg_HC05
- | HC08 ⇒ Some ? set_indX_8_low_reg_HC08
- | HCS08 ⇒ Some ? set_indX_8_low_reg_HC08
- | RS08 ⇒ None ? ])
- (λf.Some ? (set_alu m t s (f (alu m t s) indxlow'))).
+λm:mcu_type.λt.
+ match m
+ return λm.any_status m t → byte8 → option (any_status m t)
+ with
+ [ HC05 ⇒ λs:any_status ? t.λval.Some ? (set_indX_8_low_reg_sHC05 t s val)
+ | HC08 ⇒ λs:any_status ? t.λval.Some ? (set_indX_8_low_reg_sHC08 t s val)
+ | HCS08 ⇒ λs:any_status ? t.λval.Some ? (set_indX_8_low_reg_sHCS08 t s val)
+ | RS08 ⇒ λs:any_status ? t.λval.None ?
+ | IP2022 ⇒ λs:any_status ? t.λval.None ?
+ ].
(* setter debole di X *)
ndefinition setweak_indX_8_low_reg ≝
-λm:mcu_type.λt:memory_impl.λs:any_status m t.λindxlow':byte8.
- match set_indX_8_low_reg m t s indxlow' with
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
+ match set_indX_8_low_reg m t s val with
[ None ⇒ s | Some s' ⇒ s' ].
(* REGISTRO H *)
-(* setter specifico HC08/HCS08 di H *)
-ndefinition set_indX_8_high_reg_HC08 ≝
-λalu.λindxhigh':byte8.
- mk_alu_HC08
- (acc_low_reg_HC08 alu)
- (indX_low_reg_HC08 alu)
- indxhigh'
- (sp_reg_HC08 alu)
- (pc_reg_HC08 alu)
- (v_flag_HC08 alu)
- (h_flag_HC08 alu)
- (i_flag_HC08 alu)
- (n_flag_HC08 alu)
- (z_flag_HC08 alu)
- (c_flag_HC08 alu)
- (irq_flag_HC08 alu).
+ndefinition set_indX_8_high_reg_sHC08 ≝
+λt:memory_impl.λs:any_status HC08 t.λval.
+ set_alu … s (set_indX_8_high_reg_HC08 (alu … s) val).
+
+ndefinition set_indX_8_high_reg_sHCS08 ≝
+λt:memory_impl.λs:any_status HCS08 t.λval.
+ set_alu … s (set_indX_8_high_reg_HC08 (alu … s) val).
(* setter forte di H *)
ndefinition set_indX_8_high_reg ≝
-λm:mcu_type.λt:memory_impl.λs:any_status m t.λindxhigh':byte8.
- opt_map … (match m return aux_set_type_opt byte8 with
- [ HC05 ⇒ None ?
- | HC08 ⇒ Some ? set_indX_8_high_reg_HC08
- | HCS08 ⇒ Some ? set_indX_8_high_reg_HC08
- | RS08 ⇒ None ? ])
- (λf.Some ? (set_alu m t s (f (alu m t s) indxhigh'))).
+λm:mcu_type.λt.
+ match m
+ return λm.any_status m t → byte8 → option (any_status m t)
+ with
+ [ HC05 ⇒ λs:any_status ? t.λval.None ?
+ | HC08 ⇒ λs:any_status ? t.λval.Some ? (set_indX_8_high_reg_sHC08 t s val)
+ | HCS08 ⇒ λs:any_status ? t.λval.Some ? (set_indX_8_high_reg_sHCS08 t s val)
+ | RS08 ⇒ λs:any_status ? t.λval.None ?
+ | IP2022 ⇒ λs:any_status ? t.λval.None ?
+ ].
(* setter debole di H *)
ndefinition setweak_indX_8_high_reg ≝
-λm:mcu_type.λt:memory_impl.λs:any_status m t.λindxhigh':byte8.
- match set_indX_8_high_reg m t s indxhigh' with
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
+ match set_indX_8_high_reg m t s val with
[ None ⇒ s | Some s' ⇒ s' ].
(* REGISTRO H:X *)
-(* setter specifico HC08/HCS08 di H:X *)
-ndefinition set_indX_16_reg_HC08 ≝
-λalu.λindx16:word16.
- mk_alu_HC08
- (acc_low_reg_HC08 alu)
- (w16l indx16)
- (w16h indx16)
- (sp_reg_HC08 alu)
- (pc_reg_HC08 alu)
- (v_flag_HC08 alu)
- (h_flag_HC08 alu)
- (i_flag_HC08 alu)
- (n_flag_HC08 alu)
- (z_flag_HC08 alu)
- (c_flag_HC08 alu)
- (irq_flag_HC08 alu).
+ndefinition set_indX_16_reg_sHC08 ≝
+λt:memory_impl.λs:any_status HC08 t.λval.
+ set_alu … s (set_indX_16_reg_HC08 (alu … s) val).
+
+ndefinition set_indX_16_reg_sHCS08 ≝
+λt:memory_impl.λs:any_status HCS08 t.λval.
+ set_alu … s (set_indX_16_reg_HC08 (alu … s) val).
(* setter forte di H:X *)
ndefinition set_indX_16_reg ≝
-λm:mcu_type.λt:memory_impl.λs:any_status m t.λindx16:word16.
- opt_map … (match m return aux_set_type_opt word16 with
- [ HC05 ⇒ None ?
- | HC08 ⇒ Some ? set_indX_16_reg_HC08
- | HCS08 ⇒ Some ? set_indX_16_reg_HC08
- | RS08 ⇒ None ? ])
- (λf.Some ? (set_alu m t s (f (alu m t s) indx16))).
+λm:mcu_type.λt.
+ match m
+ return λm.any_status m t → word16 → option (any_status m t)
+ with
+ [ HC05 ⇒ λs:any_status ? t.λval.None ?
+ | HC08 ⇒ λs:any_status ? t.λval.Some ? (set_indX_16_reg_sHC08 t s val)
+ | HCS08 ⇒ λs:any_status ? t.λval.Some ? (set_indX_16_reg_sHCS08 t s val)
+ | RS08 ⇒ λs:any_status ? t.λval.None ?
+ | IP2022 ⇒ λs:any_status ? t.λval.None ?
+ ].
(* setter debole di H:X *)
ndefinition setweak_indX_16_reg ≝
-λm:mcu_type.λt:memory_impl.λs:any_status m t.λindx16:word16.
- match set_indX_16_reg m t s indx16 with
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
+ match set_indX_16_reg m t s val with
[ None ⇒ s | Some s' ⇒ s' ].
(* REGISTRO SP *)
-(* setter specifico HC05 di SP, effettua (SP∧mask)∨fix *)
-ndefinition set_sp_reg_HC05 ≝
-λalu.λsp':word16.
- mk_alu_HC05
- (acc_low_reg_HC05 alu)
- (indX_low_reg_HC05 alu)
- (or_w16 (and_w16 sp' (sp_mask_HC05 alu)) (sp_fix_HC05 alu))
- (sp_mask_HC05 alu)
- (sp_fix_HC05 alu)
- (pc_reg_HC05 alu)
- (pc_mask_HC05 alu)
- (h_flag_HC05 alu)
- (i_flag_HC05 alu)
- (n_flag_HC05 alu)
- (z_flag_HC05 alu)
- (c_flag_HC05 alu)
- (irq_flag_HC05 alu).
-
-(* setter specifico HC08/HCS08 di SP *)
-ndefinition set_sp_reg_HC08 ≝
-λalu.λsp':word16.
- mk_alu_HC08
- (acc_low_reg_HC08 alu)
- (indX_low_reg_HC08 alu)
- (indX_high_reg_HC08 alu)
- sp'
- (pc_reg_HC08 alu)
- (v_flag_HC08 alu)
- (h_flag_HC08 alu)
- (i_flag_HC08 alu)
- (n_flag_HC08 alu)
- (z_flag_HC08 alu)
- (c_flag_HC08 alu)
- (irq_flag_HC08 alu).
+ndefinition set_sp_reg_sHC05 ≝
+λt:memory_impl.λs:any_status HC05 t.λval.
+ set_alu … s (set_sp_reg_HC05 (alu … s) val).
+
+ndefinition set_sp_reg_sHC08 ≝
+λt:memory_impl.λs:any_status HC08 t.λval.
+ set_alu … s (set_sp_reg_HC08 (alu … s) val).
+
+ndefinition set_sp_reg_sHCS08 ≝
+λt:memory_impl.λs:any_status HCS08 t.λval.
+ set_alu … s (set_sp_reg_HC08 (alu … s) val).
+
+ndefinition set_sp_reg_sIP2022 ≝
+λt:memory_impl.λs:any_status IP2022 t.λval.
+ set_alu … s (set_sp_reg_IP2022 (alu … s) val).
(* setter forte di SP *)
ndefinition set_sp_reg ≝
-λm:mcu_type.λt:memory_impl.λs:any_status m t.λsp':word16.
- opt_map … (match m return aux_set_type_opt word16 with
- [ HC05 ⇒ Some ? set_sp_reg_HC05
- | HC08 ⇒ Some ? set_sp_reg_HC08
- | HCS08 ⇒ Some ? set_sp_reg_HC08
- | RS08 ⇒ None ? ])
- (λf.Some ? (set_alu m t s (f (alu m t s) sp'))).
+λm:mcu_type.λt.
+ match m
+ return λm.any_status m t → word16 → option (any_status m t)
+ with
+ [ HC05 ⇒ λs:any_status ? t.λval.Some ? (set_sp_reg_sHC05 t s val)
+ | HC08 ⇒ λs:any_status ? t.λval.Some ? (set_sp_reg_sHC08 t s val)
+ | HCS08 ⇒ λs:any_status ? t.λval.Some ? (set_sp_reg_sHCS08 t s val)
+ | RS08 ⇒ λs:any_status ? t.λval.None ?
+ | IP2022 ⇒ λs:any_status ? t.λval.Some ? (set_sp_reg_sIP2022 t s val)
+ ].
(* setter debole di SP *)
ndefinition setweak_sp_reg ≝
-λm:mcu_type.λt:memory_impl.λs:any_status m t.λsp':word16.
- match set_sp_reg m t s sp' with
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
+ match set_sp_reg m t s val with
[ None ⇒ s | Some s' ⇒ s' ].
(* REGISTRO PC *)
-(* setter specifico HC05 di PC, effettua PC∧mask *)
-ndefinition set_pc_reg_HC05 ≝
-λalu.λpc':word16.
- mk_alu_HC05
- (acc_low_reg_HC05 alu)
- (indX_low_reg_HC05 alu)
- (sp_reg_HC05 alu)
- (sp_mask_HC05 alu)
- (sp_fix_HC05 alu)
- (and_w16 pc' (pc_mask_HC05 alu))
- (pc_mask_HC05 alu)
- (h_flag_HC05 alu)
- (i_flag_HC05 alu)
- (n_flag_HC05 alu)
- (z_flag_HC05 alu)
- (c_flag_HC05 alu)
- (irq_flag_HC05 alu).
-
-(* setter specifico HC08/HCS08 di PC *)
-ndefinition set_pc_reg_HC08 ≝
-λalu.λpc':word16.
- mk_alu_HC08
- (acc_low_reg_HC08 alu)
- (indX_low_reg_HC08 alu)
- (indX_high_reg_HC08 alu)
- (sp_reg_HC08 alu)
- pc'
- (v_flag_HC08 alu)
- (h_flag_HC08 alu)
- (i_flag_HC08 alu)
- (n_flag_HC08 alu)
- (z_flag_HC08 alu)
- (c_flag_HC08 alu)
- (irq_flag_HC08 alu).
-
-(* setter specifico RS08 di PC, effettua PC∧mask *)
-ndefinition set_pc_reg_RS08 ≝
-λalu.λpc':word16.
- mk_alu_RS08
- (acc_low_reg_RS08 alu)
- (and_w16 pc' (pc_mask_RS08 alu))
- (pc_mask_RS08 alu)
- (spc_reg_RS08 alu)
- (x_map_RS08 alu)
- (ps_map_RS08 alu)
- (z_flag_RS08 alu)
- (c_flag_RS08 alu).
-
(* setter forte di PC *)
ndefinition set_pc_reg ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λpc':word16.
| HC08 ⇒ set_pc_reg_HC08
| HCS08 ⇒ set_pc_reg_HC08
| RS08 ⇒ set_pc_reg_RS08
+ | IP2022 ⇒ set_pc_reg_IP2022
] (alu m t s) pc').
(* REGISTRO SPC *)
-(* setter specifico RS08 di SPC, effettua SPC∧mask *)
-ndefinition set_spc_reg_RS08 ≝
-λalu.λspc':word16.
- mk_alu_RS08
- (acc_low_reg_RS08 alu)
- (pc_reg_RS08 alu)
- (pc_mask_RS08 alu)
- (and_w16 spc' (pc_mask_RS08 alu))
- (x_map_RS08 alu)
- (ps_map_RS08 alu)
- (z_flag_RS08 alu)
- (c_flag_RS08 alu).
+ndefinition set_spc_reg_sRS08 ≝
+λt:memory_impl.λs:any_status RS08 t.λval.
+ set_alu … s (set_spc_reg_RS08 (alu … s) val).
(* setter forte di SPC *)
ndefinition set_spc_reg ≝
-λm:mcu_type.λt:memory_impl.λs:any_status m t.λspc':word16.
- opt_map … (match m return aux_set_type_opt word16 with
- [ HC05 ⇒ None ?
- | HC08 ⇒ None ?
- | HCS08 ⇒ None ?
- | RS08 ⇒ Some ? set_spc_reg_RS08 ])
- (λf.Some ? (set_alu m t s (f (alu m t s) spc'))).
+λm:mcu_type.λt.
+ match m
+ return λm.any_status m t → word16 → option (any_status m t)
+ with
+ [ HC05 ⇒ λs:any_status ? t.λval.None ?
+ | HC08 ⇒ λs:any_status ? t.λval.None ?
+ | HCS08 ⇒ λs:any_status ? t.λval.None ?
+ | RS08 ⇒ λs:any_status ? t.λval.Some ? (set_spc_reg_sRS08 t s val)
+ | IP2022 ⇒ λs:any_status ? t.λval.None ?
+ ].
(* setter debole di SPC *)
ndefinition setweak_spc_reg ≝
-λm:mcu_type.λt:memory_impl.λs:any_status m t.λspc':word16.
- match set_spc_reg m t s spc' with
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
+ match set_spc_reg m t s val with
+ [ None ⇒ s | Some s' ⇒ s' ].
+
+(* REGISTRO MULH *)
+
+ndefinition set_mulh_reg_sIP2022 ≝
+λt:memory_impl.λs:any_status IP2022 t.λval.
+ set_alu … s (set_mulh_reg_IP2022 (alu … s) val).
+
+(* setter forte di MULH *)
+ndefinition set_mulh_reg ≝
+λm:mcu_type.λt.
+ match m
+ return λm.any_status m t → byte8 → option (any_status m t)
+ with
+ [ HC05 ⇒ λs:any_status ? t.λval.None ?
+ | HC08 ⇒ λs:any_status ? t.λval.None ?
+ | HCS08 ⇒ λs:any_status ? t.λval.None ?
+ | RS08 ⇒ λs:any_status ? t.λval.None ?
+ | IP2022 ⇒ λs:any_status ? t.λval.Some ? (set_mulh_reg_sIP2022 t s val)
+ ].
+
+(* setter debole di MULH *)
+ndefinition setweak_mulh_reg ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
+ match set_mulh_reg m t s val with
+ [ None ⇒ s | Some s' ⇒ s' ].
+
+(* REGISTRO ADDRSEL *)
+
+ndefinition set_addrsel_reg_sIP2022 ≝
+λt:memory_impl.λs:any_status IP2022 t.λval.
+ set_alu … s (set_addrsel_reg_IP2022 (alu … s) val).
+
+(* setter forte di ADDRSEL *)
+ndefinition set_addrsel_reg ≝
+λm:mcu_type.λt.
+ match m
+ return λm.any_status m t → byte8 → option (any_status m t)
+ with
+ [ HC05 ⇒ λs:any_status ? t.λval.None ?
+ | HC08 ⇒ λs:any_status ? t.λval.None ?
+ | HCS08 ⇒ λs:any_status ? t.λval.None ?
+ | RS08 ⇒ λs:any_status ? t.λval.None ?
+ | IP2022 ⇒ λs:any_status ? t.λval.Some ? (set_addrsel_reg_sIP2022 t s val)
+ ].
+
+(* setter debole di ADDRSEL *)
+ndefinition setweak_addrsel_reg ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
+ match set_addrsel_reg m t s val with
+ [ None ⇒ s | Some s' ⇒ s' ].
+
+(* REGISTRO ADDR *)
+
+ndefinition set_addr_reg_sIP2022 ≝
+λt:memory_impl.λs:any_status IP2022 t.λval.
+ set_alu … s (set_addr_reg_IP2022 (alu … s) val).
+
+(* setter forte di ADDR *)
+ndefinition set_addr_reg ≝
+λm:mcu_type.λt.
+ match m
+ return λm.any_status m t → word24 → option (any_status m t)
+ with
+ [ HC05 ⇒ λs:any_status ? t.λval.None ?
+ | HC08 ⇒ λs:any_status ? t.λval.None ?
+ | HCS08 ⇒ λs:any_status ? t.λval.None ?
+ | RS08 ⇒ λs:any_status ? t.λval.None ?
+ | IP2022 ⇒ λs:any_status ? t.λval.Some ? (set_addr_reg_sIP2022 t s val)
+ ].
+
+(* setter debole di ADDR *)
+ndefinition setweak_addr_reg ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
+ match set_addr_reg m t s val with
+ [ None ⇒ s | Some s' ⇒ s' ].
+
+(* REGISTRO CALL *)
+
+ndefinition set_call_reg_sIP2022 ≝
+λt:memory_impl.λs:any_status IP2022 t.λval.
+ set_alu … s (set_call_reg_IP2022 (alu … s) val).
+
+(* setter forte di CALL *)
+ndefinition set_call_reg ≝
+λm:mcu_type.λt.
+ match m
+ return λm.any_status m t → word16 → option (any_status m t)
+ with
+ [ HC05 ⇒ λs:any_status ? t.λval.None ?
+ | HC08 ⇒ λs:any_status ? t.λval.None ?
+ | HCS08 ⇒ λs:any_status ? t.λval.None ?
+ | RS08 ⇒ λs:any_status ? t.λval.None ?
+ | IP2022 ⇒ λs:any_status ? t.λval.Some ? (set_call_reg_sIP2022 t s val)
+ ].
+
+(* setter debole di CALL *)
+ndefinition setweak_call_reg ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
+ match set_call_reg m t s val with
+ [ None ⇒ s | Some s' ⇒ s' ].
+
+(* REGISTRO CALL [push] *)
+
+ndefinition push_call_reg_sIP2022 ≝
+λt:memory_impl.λs:any_status IP2022 t.λval.
+ set_alu … s (push_call_reg_IP2022 (alu … s) val).
+
+(* push forte di CALL *)
+ndefinition push_call_reg ≝
+λm:mcu_type.λt.
+ match m
+ return λm.any_status m t → word16 → option (any_status m t)
+ with
+ [ HC05 ⇒ λs:any_status ? t.λval.None ?
+ | HC08 ⇒ λs:any_status ? t.λval.None ?
+ | HCS08 ⇒ λs:any_status ? t.λval.None ?
+ | RS08 ⇒ λs:any_status ? t.λval.None ?
+ | IP2022 ⇒ λs:any_status ? t.λval.Some ? (push_call_reg_sIP2022 t s val)
+ ].
+
+(* REGISTRO CALL [pop] *)
+
+ndefinition pop_call_reg_sIP2022 ≝
+λt:memory_impl.λs:any_status IP2022 t.
+ match pop_call_reg_IP2022 (alu … s) with
+ [ pair val alu' ⇒ pair … val (set_alu … s alu') ].
+
+(* pop forte di CALL *)
+ndefinition pop_call_reg ≝
+λm:mcu_type.λt.
+ match m
+ return λm.any_status m t → option (ProdT word16 (any_status m t))
+ with
+ [ HC05 ⇒ λs:any_status ? t.None ?
+ | HC08 ⇒ λs:any_status ? t.None ?
+ | HCS08 ⇒ λs:any_status ? t.None ?
+ | RS08 ⇒ λs:any_status ? t.None ?
+ | IP2022 ⇒ λs:any_status ? t.Some ? (pop_call_reg_sIP2022 t s)
+ ].
+
+(* REGISTRO IP *)
+
+ndefinition set_ip_reg_sIP2022 ≝
+λt:memory_impl.λs:any_status IP2022 t.λval.
+ set_alu … s (set_ip_reg_IP2022 (alu … s) val).
+
+(* setter forte di IP *)
+ndefinition set_ip_reg ≝
+λm:mcu_type.λt.
+ match m
+ return λm.any_status m t → word16 → option (any_status m t)
+ with
+ [ HC05 ⇒ λs:any_status ? t.λval.None ?
+ | HC08 ⇒ λs:any_status ? t.λval.None ?
+ | HCS08 ⇒ λs:any_status ? t.λval.None ?
+ | RS08 ⇒ λs:any_status ? t.λval.None ?
+ | IP2022 ⇒ λs:any_status ? t.λval.Some ? (set_ip_reg_sIP2022 t s val)
+ ].
+
+(* setter debole di IP *)
+ndefinition setweak_ip_reg ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
+ match set_ip_reg m t s val with
+ [ None ⇒ s | Some s' ⇒ s' ].
+
+(* REGISTRO DP *)
+
+ndefinition set_dp_reg_sIP2022 ≝
+λt:memory_impl.λs:any_status IP2022 t.λval.
+ set_alu … s (set_dp_reg_IP2022 (alu … s) val).
+
+(* setter forte di DP *)
+ndefinition set_dp_reg ≝
+λm:mcu_type.λt.
+ match m
+ return λm.any_status m t → word16 → option (any_status m t)
+ with
+ [ HC05 ⇒ λs:any_status ? t.λval.None ?
+ | HC08 ⇒ λs:any_status ? t.λval.None ?
+ | HCS08 ⇒ λs:any_status ? t.λval.None ?
+ | RS08 ⇒ λs:any_status ? t.λval.None ?
+ | IP2022 ⇒ λs:any_status ? t.λval.Some ? (set_dp_reg_sIP2022 t s val)
+ ].
+
+(* setter debole di DP *)
+ndefinition setweak_dp_reg ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
+ match set_dp_reg m t s val with
+ [ None ⇒ s | Some s' ⇒ s' ].
+
+(* REGISTRO DATA *)
+
+ndefinition set_data_reg_sIP2022 ≝
+λt:memory_impl.λs:any_status IP2022 t.λval.
+ set_alu … s (set_data_reg_IP2022 (alu … s) val).
+
+(* setter forte di DATA *)
+ndefinition set_data_reg ≝
+λm:mcu_type.λt.
+ match m
+ return λm.any_status m t → word16 → option (any_status m t)
+ with
+ [ HC05 ⇒ λs:any_status ? t.λval.None ?
+ | HC08 ⇒ λs:any_status ? t.λval.None ?
+ | HCS08 ⇒ λs:any_status ? t.λval.None ?
+ | RS08 ⇒ λs:any_status ? t.λval.None ?
+ | IP2022 ⇒ λs:any_status ? t.λval.Some ? (set_data_reg_sIP2022 t s val)
+ ].
+
+(* setter debole di DATA *)
+ndefinition setweak_data_reg ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
+ match set_data_reg m t s val with
+ [ None ⇒ s | Some s' ⇒ s' ].
+
+(* REGISTRO SPEED *)
+
+ndefinition set_speed_reg_sIP2022 ≝
+λt:memory_impl.λs:any_status IP2022 t.λval.
+ set_alu … s (set_speed_reg_IP2022 (alu … s) val).
+
+(* setter forte di SPEED *)
+ndefinition set_speed_reg ≝
+λm:mcu_type.λt.
+ match m
+ return λm.any_status m t → exadecim → option (any_status m t)
+ with
+ [ HC05 ⇒ λs:any_status ? t.λval.None ?
+ | HC08 ⇒ λs:any_status ? t.λval.None ?
+ | HCS08 ⇒ λs:any_status ? t.λval.None ?
+ | RS08 ⇒ λs:any_status ? t.λval.None ?
+ | IP2022 ⇒ λs:any_status ? t.λval.Some ? (set_speed_reg_sIP2022 t s val)
+ ].
+
+(* setter debole di SPEED *)
+ndefinition setweak_speed_reg ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
+ match set_speed_reg m t s val with
+ [ None ⇒ s | Some s' ⇒ s' ].
+
+(* REGISTRO PAGE *)
+
+ndefinition set_page_reg_sIP2022 ≝
+λt:memory_impl.λs:any_status IP2022 t.λval.
+ set_alu … s (set_page_reg_IP2022 (alu … s) val).
+
+(* setter forte di PAGE *)
+ndefinition set_page_reg ≝
+λm:mcu_type.λt.
+ match m
+ return λm.any_status m t → oct → option (any_status m t)
+ with
+ [ HC05 ⇒ λs:any_status ? t.λval.None ?
+ | HC08 ⇒ λs:any_status ? t.λval.None ?
+ | HCS08 ⇒ λs:any_status ? t.λval.None ?
+ | RS08 ⇒ λs:any_status ? t.λval.None ?
+ | IP2022 ⇒ λs:any_status ? t.λval.Some ? (set_page_reg_sIP2022 t s val)
+ ].
+
+(* setter debole di PAGE *)
+ndefinition setweak_page_reg ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
+ match set_page_reg m t s val with
[ None ⇒ s | Some s' ⇒ s' ].
(* REGISTRO MEMORY MAPPED X *)
-(* setter specifico RS08 di memory mapped X *)
-ndefinition set_x_map_RS08 ≝
-λalu.λxm':byte8.
- mk_alu_RS08
- (acc_low_reg_RS08 alu)
- (pc_reg_RS08 alu)
- (pc_mask_RS08 alu)
- (spc_reg_RS08 alu)
- xm'
- (ps_map_RS08 alu)
- (z_flag_RS08 alu)
- (c_flag_RS08 alu).
+ndefinition set_x_map_sRS08 ≝
+λt:memory_impl.λs:any_status RS08 t.λval.
+ set_alu … s (set_x_map_RS08 (alu … s) val).
(* setter forte di memory mapped X *)
ndefinition set_x_map ≝
-λm:mcu_type.λt:memory_impl.λs:any_status m t.λxm':byte8.
- opt_map … (match m return aux_set_type_opt byte8 with
- [ HC05 ⇒ None ?
- | HC08 ⇒ None ?
- | HCS08 ⇒ None ?
- | RS08 ⇒ Some ? set_x_map_RS08 ])
- (λf.Some ? (set_alu m t s (f (alu m t s) xm'))).
+λm:mcu_type.λt.
+ match m
+ return λm.any_status m t → byte8 → option (any_status m t)
+ with
+ [ HC05 ⇒ λs:any_status ? t.λval.None ?
+ | HC08 ⇒ λs:any_status ? t.λval.None ?
+ | HCS08 ⇒ λs:any_status ? t.λval.None ?
+ | RS08 ⇒ λs:any_status ? t.λval.Some ? (set_x_map_sRS08 t s val)
+ | IP2022 ⇒ λs:any_status ? t.λval.None ?
+ ].
(* setter debole di memory mapped X *)
ndefinition setweak_x_map ≝
-λm:mcu_type.λt:memory_impl.λs:any_status m t.λxm':byte8.
- match set_x_map m t s xm' with
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
+ match set_x_map m t s val with
[ None ⇒ s | Some s' ⇒ s' ].
(* REGISTRO MEMORY MAPPED PS *)
-(* setter specifico RS08 di memory mapped PS *)
-ndefinition set_ps_map_RS08 ≝
-λalu.λpsm':byte8.
- mk_alu_RS08
- (acc_low_reg_RS08 alu)
- (pc_reg_RS08 alu)
- (pc_mask_RS08 alu)
- (spc_reg_RS08 alu)
- (x_map_RS08 alu)
- psm'
- (z_flag_RS08 alu)
- (c_flag_RS08 alu).
+ndefinition set_ps_map_sRS08 ≝
+λt:memory_impl.λs:any_status RS08 t.λval.
+ set_alu … s (set_ps_map_RS08 (alu … s) val).
(* setter forte di memory mapped PS *)
ndefinition set_ps_map ≝
-λm:mcu_type.λt:memory_impl.λs:any_status m t.λpsm':byte8.
- opt_map … (match m return aux_set_type_opt byte8 with
- [ HC05 ⇒ None ?
- | HC08 ⇒ None ?
- | HCS08 ⇒ None ?
- | RS08 ⇒ Some ? set_ps_map_RS08 ])
- (λf.Some ? (set_alu m t s (f (alu m t s) psm'))).
+λm:mcu_type.λt.
+ match m
+ return λm.any_status m t → byte8 → option (any_status m t)
+ with
+ [ HC05 ⇒ λs:any_status ? t.λval.None ?
+ | HC08 ⇒ λs:any_status ? t.λval.None ?
+ | HCS08 ⇒ λs:any_status ? t.λval.None ?
+ | RS08 ⇒ λs:any_status ? t.λval.Some ? (set_ps_map_sRS08 t s val)
+ | IP2022 ⇒ λs:any_status ? t.λval.None ?
+ ].
(* setter debole di memory mapped PS *)
ndefinition setweak_ps_map ≝
-λm:mcu_type.λt:memory_impl.λs:any_status m t.λpsm':byte8.
- match set_ps_map m t s psm' with
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
+ match set_ps_map m t s val with
+ [ None ⇒ s | Some s' ⇒ s' ].
+
+(* MODALITA SKIP *)
+
+ndefinition set_skip_mode_sIP2022 ≝
+λt:memory_impl.λs:any_status IP2022 t.λval.
+ set_alu … s (set_skip_mode_IP2022 (alu … s) val).
+
+(* setter forte di modalita SKIP *)
+ndefinition set_skip_mode ≝
+λm:mcu_type.λt.
+ match m
+ return λm.any_status m t → bool → option (any_status m t)
+ with
+ [ HC05 ⇒ λs:any_status ? t.λval.None ?
+ | HC08 ⇒ λs:any_status ? t.λval.None ?
+ | HCS08 ⇒ λs:any_status ? t.λval.None ?
+ | RS08 ⇒ λs:any_status ? t.λval.None ?
+ | IP2022 ⇒ λs:any_status ? t.λval.Some ? (set_skip_mode_sIP2022 t s val)
+ ].
+
+(* setter debole di SKIP *)
+ndefinition setweak_skip_mode ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
+ match set_skip_mode m t s val with
[ None ⇒ s | Some s' ⇒ s' ].
(* FLAG V *)
-(* setter specifico HC08/HCS08 di V *)
-ndefinition set_v_flag_HC08 ≝
-λalu.λvfl':bool.
- mk_alu_HC08
- (acc_low_reg_HC08 alu)
- (indX_low_reg_HC08 alu)
- (indX_high_reg_HC08 alu)
- (sp_reg_HC08 alu)
- (pc_reg_HC08 alu)
- vfl'
- (h_flag_HC08 alu)
- (i_flag_HC08 alu)
- (n_flag_HC08 alu)
- (z_flag_HC08 alu)
- (c_flag_HC08 alu)
- (irq_flag_HC08 alu).
+ndefinition set_v_flag_sHC08 ≝
+λt:memory_impl.λs:any_status HC08 t.λval.
+ set_alu … s (set_v_flag_HC08 (alu … s) val).
+
+ndefinition set_v_flag_sHCS08 ≝
+λt:memory_impl.λs:any_status HCS08 t.λval.
+ set_alu … s (set_v_flag_HC08 (alu … s) val).
(* setter forte di V *)
ndefinition set_v_flag ≝
-λm:mcu_type.λt:memory_impl.λs:any_status m t.λvfl':bool.
- opt_map … (match m return aux_set_type_opt bool with
- [ HC05 ⇒ None ?
- | HC08 ⇒ Some ? set_v_flag_HC08
- | HCS08 ⇒ Some ? set_v_flag_HC08
- | RS08 ⇒ None ? ])
- (λf.Some ? (set_alu m t s (f (alu m t s) vfl'))).
+λm:mcu_type.λt.
+ match m
+ return λm.any_status m t → bool → option (any_status m t)
+ with
+ [ HC05 ⇒ λs:any_status ? t.λval.None ?
+ | HC08 ⇒ λs:any_status ? t.λval.Some ? (set_v_flag_sHC08 t s val)
+ | HCS08 ⇒ λs:any_status ? t.λval.Some ? (set_v_flag_sHCS08 t s val)
+ | RS08 ⇒ λs:any_status ? t.λval.None ?
+ | IP2022 ⇒ λs:any_status ? t.λval.None ?
+ ].
(* setter debole di V *)
ndefinition setweak_v_flag ≝
-λm:mcu_type.λt:memory_impl.λs:any_status m t.λvfl':bool.
- match set_v_flag m t s vfl' with
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
+ match set_v_flag m t s val with
[ None ⇒ s | Some s' ⇒ s' ].
(* FLAG H *)
-(* setter specifico HC05 di H *)
-ndefinition set_h_flag_HC05 ≝
-λalu.λhfl':bool.
- mk_alu_HC05
- (acc_low_reg_HC05 alu)
- (indX_low_reg_HC05 alu)
- (sp_reg_HC05 alu)
- (sp_mask_HC05 alu)
- (sp_fix_HC05 alu)
- (pc_reg_HC05 alu)
- (pc_mask_HC05 alu)
- hfl'
- (i_flag_HC05 alu)
- (n_flag_HC05 alu)
- (z_flag_HC05 alu)
- (c_flag_HC05 alu)
- (irq_flag_HC05 alu).
-
-(* setter specifico HC08/HCS08 di H *)
-ndefinition set_h_flag_HC08 ≝
-λalu.λhfl':bool.
- mk_alu_HC08
- (acc_low_reg_HC08 alu)
- (indX_low_reg_HC08 alu)
- (indX_high_reg_HC08 alu)
- (sp_reg_HC08 alu)
- (pc_reg_HC08 alu)
- (v_flag_HC08 alu)
- hfl'
- (i_flag_HC08 alu)
- (n_flag_HC08 alu)
- (z_flag_HC08 alu)
- (c_flag_HC08 alu)
- (irq_flag_HC08 alu).
+ndefinition set_h_flag_sHC05 ≝
+λt:memory_impl.λs:any_status HC05 t.λval.
+ set_alu … s (set_h_flag_HC05 (alu … s) val).
+
+ndefinition set_h_flag_sHC08 ≝
+λt:memory_impl.λs:any_status HC08 t.λval.
+ set_alu … s (set_h_flag_HC08 (alu … s) val).
+
+ndefinition set_h_flag_sHCS08 ≝
+λt:memory_impl.λs:any_status HCS08 t.λval.
+ set_alu … s (set_h_flag_HC08 (alu … s) val).
+
+ndefinition set_h_flag_sIP2022 ≝
+λt:memory_impl.λs:any_status IP2022 t.λval.
+ set_alu … s (set_h_flag_IP2022 (alu … s) val).
(* setter forte di H *)
ndefinition set_h_flag ≝
-λm:mcu_type.λt:memory_impl.λs:any_status m t.λhfl':bool.
- opt_map … (match m return aux_set_type_opt bool with
- [ HC05 ⇒ Some ? set_h_flag_HC05
- | HC08 ⇒ Some ? set_h_flag_HC08
- | HCS08 ⇒ Some ? set_h_flag_HC08
- | RS08 ⇒ None ? ])
- (λf.Some ? (set_alu m t s (f (alu m t s) hfl'))).
+λm:mcu_type.λt.
+ match m
+ return λm.any_status m t → bool → option (any_status m t)
+ with
+ [ HC05 ⇒ λs:any_status ? t.λval.Some ? (set_h_flag_sHC05 t s val)
+ | HC08 ⇒ λs:any_status ? t.λval.Some ? (set_h_flag_sHC08 t s val)
+ | HCS08 ⇒ λs:any_status ? t.λval.Some ? (set_h_flag_sHCS08 t s val)
+ | RS08 ⇒ λs:any_status ? t.λval.None ?
+ | IP2022 ⇒ λs:any_status ? t.λval.Some ? (set_h_flag_sIP2022 t s val)
+ ].
(* setter debole di H *)
ndefinition setweak_h_flag ≝
-λm:mcu_type.λt:memory_impl.λs:any_status m t.λhfl':bool.
- match set_h_flag m t s hfl' with
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
+ match set_h_flag m t s val with
[ None ⇒ s | Some s' ⇒ s' ].
(* FLAG I *)
-(* setter specifico HC05 di I *)
-ndefinition set_i_flag_HC05 ≝
-λalu.λifl':bool.
- mk_alu_HC05
- (acc_low_reg_HC05 alu)
- (indX_low_reg_HC05 alu)
- (sp_reg_HC05 alu)
- (sp_mask_HC05 alu)
- (sp_fix_HC05 alu)
- (pc_reg_HC05 alu)
- (pc_mask_HC05 alu)
- (h_flag_HC05 alu)
- ifl'
- (n_flag_HC05 alu)
- (z_flag_HC05 alu)
- (c_flag_HC05 alu)
- (irq_flag_HC05 alu).
-
-(* setter specifico HC08/HCS08 di I *)
-ndefinition set_i_flag_HC08 ≝
-λalu.λifl':bool.
- mk_alu_HC08
- (acc_low_reg_HC08 alu)
- (indX_low_reg_HC08 alu)
- (indX_high_reg_HC08 alu)
- (sp_reg_HC08 alu)
- (pc_reg_HC08 alu)
- (v_flag_HC08 alu)
- (h_flag_HC08 alu)
- ifl'
- (n_flag_HC08 alu)
- (z_flag_HC08 alu)
- (c_flag_HC08 alu)
- (irq_flag_HC08 alu).
+ndefinition set_i_flag_sHC05 ≝
+λt:memory_impl.λs:any_status HC05 t.λval.
+ set_alu … s (set_i_flag_HC05 (alu … s) val).
+
+ndefinition set_i_flag_sHC08 ≝
+λt:memory_impl.λs:any_status HC08 t.λval.
+ set_alu … s (set_i_flag_HC08 (alu … s) val).
+
+ndefinition set_i_flag_sHCS08 ≝
+λt:memory_impl.λs:any_status HCS08 t.λval.
+ set_alu … s (set_i_flag_HC08 (alu … s) val).
(* setter forte di I *)
ndefinition set_i_flag ≝
-λm:mcu_type.λt:memory_impl.λs:any_status m t.λifl':bool.
- opt_map … (match m return aux_set_type_opt bool with
- [ HC05 ⇒ Some ? set_i_flag_HC05
- | HC08 ⇒ Some ? set_i_flag_HC08
- | HCS08 ⇒ Some ? set_i_flag_HC08
- | RS08 ⇒ None ? ])
- (λf.Some ? (set_alu m t s (f (alu m t s) ifl'))).
+λm:mcu_type.λt.
+ match m
+ return λm.any_status m t → bool → option (any_status m t)
+ with
+ [ HC05 ⇒ λs:any_status ? t.λval.Some ? (set_i_flag_sHC05 t s val)
+ | HC08 ⇒ λs:any_status ? t.λval.Some ? (set_i_flag_sHC08 t s val)
+ | HCS08 ⇒ λs:any_status ? t.λval.Some ? (set_i_flag_sHCS08 t s val)
+ | RS08 ⇒ λs:any_status ? t.λval.None ?
+ | IP2022 ⇒ λs:any_status ? t.λval.None ?
+ ].
(* setter debole di I *)
ndefinition setweak_i_flag ≝
-λm:mcu_type.λt:memory_impl.λs:any_status m t.λifl':bool.
- match set_i_flag m t s ifl' with
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
+ match set_i_flag m t s val with
[ None ⇒ s | Some s' ⇒ s' ].
(* FLAG N *)
-(* setter specifico HC05 di N *)
-ndefinition set_n_flag_HC05 ≝
-λalu.λnfl':bool.
- mk_alu_HC05
- (acc_low_reg_HC05 alu)
- (indX_low_reg_HC05 alu)
- (sp_reg_HC05 alu)
- (sp_mask_HC05 alu)
- (sp_fix_HC05 alu)
- (pc_reg_HC05 alu)
- (pc_mask_HC05 alu)
- (h_flag_HC05 alu)
- (i_flag_HC05 alu)
- nfl'
- (z_flag_HC05 alu)
- (c_flag_HC05 alu)
- (irq_flag_HC05 alu).
-
-(* setter specifico HC08/HCS08 di N *)
-ndefinition set_n_flag_HC08 ≝
-λalu.λnfl':bool.
- mk_alu_HC08
- (acc_low_reg_HC08 alu)
- (indX_low_reg_HC08 alu)
- (indX_high_reg_HC08 alu)
- (sp_reg_HC08 alu)
- (pc_reg_HC08 alu)
- (v_flag_HC08 alu)
- (h_flag_HC08 alu)
- (i_flag_HC08 alu)
- nfl'
- (z_flag_HC08 alu)
- (c_flag_HC08 alu)
- (irq_flag_HC08 alu).
+ndefinition set_n_flag_sHC05 ≝
+λt:memory_impl.λs:any_status HC05 t.λval.
+ set_alu … s (set_n_flag_HC05 (alu … s) val).
+
+ndefinition set_n_flag_sHC08 ≝
+λt:memory_impl.λs:any_status HC08 t.λval.
+ set_alu … s (set_n_flag_HC08 (alu … s) val).
+
+ndefinition set_n_flag_sHCS08 ≝
+λt:memory_impl.λs:any_status HCS08 t.λval.
+ set_alu … s (set_n_flag_HC08 (alu … s) val).
(* setter forte di N *)
ndefinition set_n_flag ≝
-λm:mcu_type.λt:memory_impl.λs:any_status m t.λnfl':bool.
- opt_map … (match m return aux_set_type_opt bool with
- [ HC05 ⇒ Some ? set_n_flag_HC05
- | HC08 ⇒ Some ? set_n_flag_HC08
- | HCS08 ⇒ Some ? set_n_flag_HC08
- | RS08 ⇒ None ? ])
- (λf.Some ? (set_alu m t s (f (alu m t s) nfl'))).
+λm:mcu_type.λt.
+ match m
+ return λm.any_status m t → bool → option (any_status m t)
+ with
+ [ HC05 ⇒ λs:any_status ? t.λval.Some ? (set_n_flag_sHC05 t s val)
+ | HC08 ⇒ λs:any_status ? t.λval.Some ? (set_n_flag_sHC08 t s val)
+ | HCS08 ⇒ λs:any_status ? t.λval.Some ? (set_n_flag_sHCS08 t s val)
+ | RS08 ⇒ λs:any_status ? t.λval.None ?
+ | IP2022 ⇒ λs:any_status ? t.λval.None ?
+ ].
(* setter debole di N *)
ndefinition setweak_n_flag ≝
-λm:mcu_type.λt:memory_impl.λs:any_status m t.λnfl':bool.
- match set_n_flag m t s nfl' with
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
+ match set_n_flag m t s val with
[ None ⇒ s | Some s' ⇒ s' ].
(* FLAG Z *)
-(* setter specifico HC05 di Z *)
-ndefinition set_z_flag_HC05 ≝
-λalu.λzfl':bool.
- mk_alu_HC05
- (acc_low_reg_HC05 alu)
- (indX_low_reg_HC05 alu)
- (sp_reg_HC05 alu)
- (sp_mask_HC05 alu)
- (sp_fix_HC05 alu)
- (pc_reg_HC05 alu)
- (pc_mask_HC05 alu)
- (h_flag_HC05 alu)
- (i_flag_HC05 alu)
- (n_flag_HC05 alu)
- zfl'
- (c_flag_HC05 alu)
- (irq_flag_HC05 alu).
-
-(* setter specifico HC08/HCS08 di Z *)
-ndefinition set_z_flag_HC08 ≝
-λalu.λzfl':bool.
- mk_alu_HC08
- (acc_low_reg_HC08 alu)
- (indX_low_reg_HC08 alu)
- (indX_high_reg_HC08 alu)
- (sp_reg_HC08 alu)
- (pc_reg_HC08 alu)
- (v_flag_HC08 alu)
- (h_flag_HC08 alu)
- (i_flag_HC08 alu)
- (n_flag_HC08 alu)
- zfl'
- (c_flag_HC08 alu)
- (irq_flag_HC08 alu).
-
-(* setter sprcifico RS08 di Z *)
-ndefinition set_z_flag_RS08 ≝
-λalu.λzfl':bool.
- mk_alu_RS08
- (acc_low_reg_RS08 alu)
- (pc_reg_RS08 alu)
- (pc_mask_RS08 alu)
- (spc_reg_RS08 alu)
- (x_map_RS08 alu)
- (ps_map_RS08 alu)
- zfl'
- (c_flag_RS08 alu).
-
(* setter forte di Z *)
ndefinition set_z_flag ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λzfl':bool.
| HC08 ⇒ set_z_flag_HC08
| HCS08 ⇒ set_z_flag_HC08
| RS08 ⇒ set_z_flag_RS08
+ | IP2022 ⇒ set_z_flag_IP2022
] (alu m t s) zfl').
(* FLAG C *)
-(* setter specifico HC05 di C *)
-ndefinition set_c_flag_HC05 ≝
-λalu.λcfl':bool.
- mk_alu_HC05
- (acc_low_reg_HC05 alu)
- (indX_low_reg_HC05 alu)
- (sp_reg_HC05 alu)
- (sp_mask_HC05 alu)
- (sp_fix_HC05 alu)
- (pc_reg_HC05 alu)
- (pc_mask_HC05 alu)
- (h_flag_HC05 alu)
- (i_flag_HC05 alu)
- (n_flag_HC05 alu)
- (z_flag_HC05 alu)
- cfl'
- (irq_flag_HC05 alu).
-
-(* setter specifico HC08/HCS08 di C *)
-ndefinition set_c_flag_HC08 ≝
-λalu.λcfl':bool.
- mk_alu_HC08
- (acc_low_reg_HC08 alu)
- (indX_low_reg_HC08 alu)
- (indX_high_reg_HC08 alu)
- (sp_reg_HC08 alu)
- (pc_reg_HC08 alu)
- (v_flag_HC08 alu)
- (h_flag_HC08 alu)
- (i_flag_HC08 alu)
- (n_flag_HC08 alu)
- (z_flag_HC08 alu)
- cfl'
- (irq_flag_HC08 alu).
-
-(* setter specifico RS08 di C *)
-ndefinition set_c_flag_RS08 ≝
-λalu.λcfl':bool.
- mk_alu_RS08
- (acc_low_reg_RS08 alu)
- (pc_reg_RS08 alu)
- (pc_mask_RS08 alu)
- (spc_reg_RS08 alu)
- (x_map_RS08 alu)
- (ps_map_RS08 alu)
- (z_flag_RS08 alu)
- cfl'.
-
(* setter forte di C *)
ndefinition set_c_flag ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λcfl':bool.
| HC08 ⇒ set_c_flag_HC08
| HCS08 ⇒ set_c_flag_HC08
| RS08 ⇒ set_c_flag_RS08
+ | IP2022 ⇒ set_c_flag_IP2022
] (alu m t s) cfl').
(* FLAG IRQ *)
-(* setter specifico HC05 di IRQ *)
-ndefinition set_irq_flag_HC05 ≝
-λalu.λirqfl':bool.
- mk_alu_HC05
- (acc_low_reg_HC05 alu)
- (indX_low_reg_HC05 alu)
- (sp_reg_HC05 alu)
- (sp_mask_HC05 alu)
- (sp_fix_HC05 alu)
- (pc_reg_HC05 alu)
- (pc_mask_HC05 alu)
- (h_flag_HC05 alu)
- (i_flag_HC05 alu)
- (n_flag_HC05 alu)
- (z_flag_HC05 alu)
- (c_flag_HC05 alu)
- irqfl'.
-
-(* setter specifico HC08/HCS08 di IRQ *)
-ndefinition set_irq_flag_HC08 ≝
-λalu.λirqfl':bool.
- mk_alu_HC08
- (acc_low_reg_HC08 alu)
- (indX_low_reg_HC08 alu)
- (indX_high_reg_HC08 alu)
- (sp_reg_HC08 alu)
- (pc_reg_HC08 alu)
- (v_flag_HC08 alu)
- (h_flag_HC08 alu)
- (i_flag_HC08 alu)
- (n_flag_HC08 alu)
- (z_flag_HC08 alu)
- (c_flag_HC08 alu)
- irqfl'.
+ndefinition set_irq_flag_sHC05 ≝
+λt:memory_impl.λs:any_status HC05 t.λval.
+ set_alu … s (set_irq_flag_HC05 (alu … s) val).
+
+ndefinition set_irq_flag_sHC08 ≝
+λt:memory_impl.λs:any_status HC08 t.λval.
+ set_alu … s (set_irq_flag_HC08 (alu … s) val).
+
+ndefinition set_irq_flag_sHCS08 ≝
+λt:memory_impl.λs:any_status HCS08 t.λval.
+ set_alu … s (set_irq_flag_HC08 (alu … s) val).
(* setter forte di IRQ *)
ndefinition set_irq_flag ≝
-λm:mcu_type.λt:memory_impl.λs:any_status m t.λirqfl':bool.
- opt_map … (match m return aux_set_type_opt bool with
- [ HC05 ⇒ Some ? set_irq_flag_HC05
- | HC08 ⇒ Some ? set_irq_flag_HC08
- | HCS08 ⇒ Some ? set_irq_flag_HC08
- | RS08 ⇒ None ? ])
- (λf.Some ? (set_alu m t s (f (alu m t s) irqfl'))).
+λm:mcu_type.λt.
+ match m
+ return λm.any_status m t → bool → option (any_status m t)
+ with
+ [ HC05 ⇒ λs:any_status ? t.λval.Some ? (set_irq_flag_sHC05 t s val)
+ | HC08 ⇒ λs:any_status ? t.λval.Some ? (set_irq_flag_sHC08 t s val)
+ | HCS08 ⇒ λs:any_status ? t.λval.Some ? (set_irq_flag_sHCS08 t s val)
+ | RS08 ⇒ λs:any_status ? t.λval.None ?
+ | IP2022 ⇒ λs:any_status ? t.λval.None ?
+ ].
(* setter debole di IRQ *)
ndefinition setweak_irq_flag ≝
-λm:mcu_type.λt:memory_impl.λs:any_status m t.λirqfl':bool.
- match set_irq_flag m t s irqfl' with
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λval.
+ match set_irq_flag m t s val with
[ None ⇒ s | Some s' ⇒ s' ].