X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Femulator%2Fstatus%2Fstatus_setter.ma;h=e28410878155af6677e758afb3766818f11c99ac;hb=b082cb1e1fc9dbd471d16d2eb231e883e96e588f;hp=5a89d2f01cb50c7fac53a59c857e5f8c23529be7;hpb=0f13d14b63b012e0ea8ce0d0e71bf808fdd444eb;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/emulator/status/status_setter.ma b/helm/software/matita/contribs/ng_assembly/emulator/status/status_setter.ma
index 5a89d2f01..e28410878 100755
--- a/helm/software/matita/contribs/ng_assembly/emulator/status/status_setter.ma
+++ b/helm/software/matita/contribs/ng_assembly/emulator/status/status_setter.ma
@@ -28,15 +28,19 @@ include "emulator/status/status.ma".
 
 (* 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 *)
 
@@ -63,54 +67,6 @@ ndefinition set_clk_desc ≝
 
 (* 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.
@@ -120,45 +76,11 @@ ndefinition set_acc_8_low_reg ≝
   | HC08 ⇒ set_acc_8_low_reg_HC08
   | HCS08 ⇒ set_acc_8_low_reg_HC08
   | RS08 ⇒ set_acc_8_low_reg_RS08
+  | IP2022 ⇒ set_acc_8_low_reg_IP2022
   ] (alu m t s) acclow').
 
 (* 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).
-
 (* setter forte di X *)
 ndefinition set_indX_8_low_reg ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindxlow':byte8.
@@ -166,7 +88,8 @@ ndefinition set_indX_8_low_reg ≝
              [ 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 ? ])
+             | RS08 ⇒ None ?
+             | IP2022 ⇒ None ? ])
  (λf.Some ? (set_alu m t s (f (alu m t s) indxlow'))).
 
 (* setter debole di X *)
@@ -177,23 +100,6 @@ ndefinition setweak_indX_8_low_reg ≝
 
 (* 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).
-
 (* setter forte di H *)
 ndefinition set_indX_8_high_reg ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindxhigh':byte8.
@@ -201,7 +107,8 @@ ndefinition set_indX_8_high_reg ≝
              [ HC05 ⇒ None ?
              | HC08 ⇒ Some ? set_indX_8_high_reg_HC08
              | HCS08 ⇒ Some ? set_indX_8_high_reg_HC08
-             | RS08 ⇒ None ? ])
+             | RS08 ⇒ None ?
+             | IP2022 ⇒ None ? ])
  (λf.Some ? (set_alu m t s (f (alu m t s) indxhigh'))).
 
 (* setter debole di H *)
@@ -212,23 +119,6 @@ ndefinition setweak_indX_8_high_reg ≝
 
 (* 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).
-
 (* setter forte di H:X *)
 ndefinition set_indX_16_reg ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λindx16:word16.
@@ -236,7 +126,8 @@ ndefinition set_indX_16_reg ≝
              [ HC05 ⇒ None ?
              | HC08 ⇒ Some ? set_indX_16_reg_HC08
              | HCS08 ⇒ Some ? set_indX_16_reg_HC08
-             | RS08 ⇒ None ? ])
+             | RS08 ⇒ None ?
+             | IP2022 ⇒ None ? ])
  (λf.Some ? (set_alu m t s (f (alu m t s) indx16))).
 
 (* setter debole di H:X *)
@@ -247,41 +138,6 @@ ndefinition setweak_indX_16_reg ≝
 
 (* 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).
-
 (* setter forte di SP *)
 ndefinition set_sp_reg ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λsp':word16.
@@ -289,7 +145,8 @@ ndefinition set_sp_reg ≝
              [ HC05 ⇒ Some ? set_sp_reg_HC05
              | HC08 ⇒ Some ? set_sp_reg_HC08
              | HCS08 ⇒ Some ? set_sp_reg_HC08
-             | RS08 ⇒ None ? ])
+             | RS08 ⇒ None ?
+             | IP2022 ⇒ Some ? set_sp_reg_IP2022 ])
  (λf.Some ? (set_alu m t s (f (alu m t s) sp'))).
 
 (* setter debole di SP *)
@@ -300,54 +157,6 @@ ndefinition setweak_sp_reg ≝
 
 (* 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.
@@ -357,23 +166,11 @@ ndefinition set_pc_reg ≝
   | 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).
-
 (* setter forte di SPC *)
 ndefinition set_spc_reg ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λspc':word16.
@@ -381,7 +178,8 @@ ndefinition set_spc_reg ≝
              [ HC05 ⇒ None ?
              | HC08 ⇒ None ?
              | HCS08 ⇒ None ?
-             | RS08 ⇒ Some ? set_spc_reg_RS08 ])
+             | RS08 ⇒ Some ? set_spc_reg_RS08
+             | IP2022 ⇒ None ? ])
  (λf.Some ? (set_alu m t s (f (alu m t s) spc'))).
 
 (* setter debole di SPC *)
@@ -390,20 +188,204 @@ ndefinition setweak_spc_reg ≝
  match set_spc_reg m t s spc' with
   [ None ⇒ s | Some s' ⇒ s' ].
 
-(* REGISTRO MEMORY MAPPED X *)
+(* REGISTRO MULH *)
+
+(* setter forte di MULH *)
+ndefinition set_mulh_reg ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λmulh':byte8.
+ opt_map … (match m return aux_set_type_opt byte8 with
+             [ HC05 ⇒ None ?
+             | HC08 ⇒ None ?
+             | HCS08 ⇒ None ?
+             | RS08 ⇒ None ?
+             | IP2022 ⇒ Some ? set_mulh_reg_IP2022 ])
+ (λf.Some ? (set_alu m t s (f (alu m t s) mulh'))).
+
+(* setter debole di MULH *)
+ndefinition setweak_mulh_reg ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λmulh':byte8.
+ match set_mulh_reg m t s mulh' with
+  [ None ⇒ s | Some s' ⇒ s' ].
+
+(* REGISTRO ADDRSEL *)
+
+(* setter forte di ADDRSEL *)
+ndefinition set_addrsel_reg ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddrsel':byte8.
+ opt_map … (match m return aux_set_type_opt byte8 with
+             [ HC05 ⇒ None ?
+             | HC08 ⇒ None ?
+             | HCS08 ⇒ None ?
+             | RS08 ⇒ None ?
+             | IP2022 ⇒ Some ? set_addrsel_reg_IP2022 ])
+ (λf.Some ? (set_alu m t s (f (alu m t s) addrsel'))).
+
+(* setter debole di ADDRSEL *)
+ndefinition setweak_addrsel_reg ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddrsel':byte8.
+ match set_addrsel_reg m t s addrsel' with
+  [ None ⇒ s | Some s' ⇒ s' ].
+
+(* REGISTRO ADDR *)
+
+(* setter forte di ADDR *)
+ndefinition set_addr_reg ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddr':word24.
+ opt_map … (match m return aux_set_type_opt word24 with
+             [ HC05 ⇒ None ?
+             | HC08 ⇒ None ?
+             | HCS08 ⇒ None ?
+             | RS08 ⇒ None ?
+             | IP2022 ⇒ Some ? set_addr_reg_IP2022 ])
+ (λf.Some ? (set_alu m t s (f (alu m t s) addr'))).
+
+(* setter debole di ADDR *)
+ndefinition setweak_addr_reg ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddr':word24.
+ match set_addr_reg m t s addr' with
+  [ None ⇒ s | Some s' ⇒ s' ].
+
+(* REGISTRO CALL *)
+
+(* setter forte di CALL *)
+ndefinition set_call_reg ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λcall':word16.
+ opt_map … (match m return aux_set_type_opt word16 with
+             [ HC05 ⇒ None ?
+             | HC08 ⇒ None ?
+             | HCS08 ⇒ None ?
+             | RS08 ⇒ None ?
+             | IP2022 ⇒ Some ? set_call_reg_IP2022 ])
+ (λf.Some ? (set_alu m t s (f (alu m t s) call'))).
+
+(* setter debole di CALL *)
+ndefinition setweak_call_reg ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λcall':word16.
+ match set_call_reg m t s call' with
+  [ None ⇒ s | Some s' ⇒ s' ].
+
+(* push forte di CALL *)
+ndefinition push_call_reg ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λcall':word16.
+ opt_map … (match m return aux_set_type_opt word16 with
+             [ HC05 ⇒ None ?
+             | HC08 ⇒ None ?
+             | HCS08 ⇒ None ?
+             | RS08 ⇒ None ?
+             | IP2022 ⇒ Some ? push_call_reg_IP2022 ])
+ (λf.Some ? (set_alu m t s (f (alu m t s) call'))).
+
+(* pop forte di CALL *)
+ndefinition pop_call_reg ≝
+λm:mcu_type.
+ match m
+  return λm.Πt.any_status m t → option (ProdT word16 (any_status m t))
+ with
+  [ HC05 ⇒ λt:memory_impl.λs:any_status HC05 t.None ?
+  | HC08 ⇒ λt:memory_impl.λs:any_status HC08 t.None ?
+  | HCS08 ⇒ λt:memory_impl.λs:any_status HCS08 t.None ?
+  | RS08 ⇒ λt:memory_impl.λs:any_status RS08 t.None ?
+  | IP2022 ⇒ λt:memory_impl.λs:any_status IP2022 t.
+   match pop_call_reg_IP2022 (alu … s) with
+    [ pair val alu' ⇒ Some ? (pair … val (set_alu … s alu')) ]
+  ].
+
+(* REGISTRO IP *)
+
+(* setter forte di IP *)
+ndefinition set_ip_reg ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λip':word16.
+ opt_map … (match m return aux_set_type_opt word16 with
+             [ HC05 ⇒ None ?
+             | HC08 ⇒ None ?
+             | HCS08 ⇒ None ?
+             | RS08 ⇒ None ?
+             | IP2022 ⇒ Some ? set_ip_reg_IP2022 ])
+ (λf.Some ? (set_alu m t s (f (alu m t s) ip'))).
+
+(* setter debole di IP *)
+ndefinition setweak_ip_reg ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λip':word16.
+ match set_ip_reg m t s ip' with
+  [ None ⇒ s | Some s' ⇒ s' ].
+
+(* REGISTRO DP *)
+
+(* setter forte di DP *)
+ndefinition set_dp_reg ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λdp':word16.
+ opt_map … (match m return aux_set_type_opt word16 with
+             [ HC05 ⇒ None ?
+             | HC08 ⇒ None ?
+             | HCS08 ⇒ None ?
+             | RS08 ⇒ None ?
+             | IP2022 ⇒ Some ? set_dp_reg_IP2022 ])
+ (λf.Some ? (set_alu m t s (f (alu m t s) dp'))).
+
+(* setter debole di DP *)
+ndefinition setweak_dp_reg ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λdp':word16.
+ match set_dp_reg m t s dp' with
+  [ None ⇒ s | Some s' ⇒ s' ].
+
+(* REGISTRO DATA *)
+
+(* setter forte di DATA *)
+ndefinition set_data_reg ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λdata':word16.
+ opt_map … (match m return aux_set_type_opt word16 with
+             [ HC05 ⇒ None ?
+             | HC08 ⇒ None ?
+             | HCS08 ⇒ None ?
+             | RS08 ⇒ None ?
+             | IP2022 ⇒ Some ? set_data_reg_IP2022 ])
+ (λf.Some ? (set_alu m t s (f (alu m t s) data'))).
+
+(* setter debole di DATA *)
+ndefinition setweak_data_reg ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λdata':word16.
+ match set_data_reg m t s data' with
+  [ None ⇒ s | Some s' ⇒ s' ].
 
-(* 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).
+(* REGISTRO SPEED *)
+
+(* setter forte di SPEED *)
+ndefinition set_speed_reg ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λspeed':exadecim.
+ opt_map … (match m return aux_set_type_opt exadecim with
+             [ HC05 ⇒ None ?
+             | HC08 ⇒ None ?
+             | HCS08 ⇒ None ?
+             | RS08 ⇒ None ?
+             | IP2022 ⇒ Some ? set_speed_reg_IP2022 ])
+ (λf.Some ? (set_alu m t s (f (alu m t s) speed'))).
+
+(* setter debole di SPEED *)
+ndefinition setweak_speed_reg ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λspeed':exadecim.
+ match set_speed_reg m t s speed' with
+  [ None ⇒ s | Some s' ⇒ s' ].
+
+(* REGISTRO PAGE *)
+
+(* setter forte di PAGE *)
+ndefinition set_page_reg ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λpage':oct.
+ opt_map … (match m return aux_set_type_opt oct with
+             [ HC05 ⇒ None ?
+             | HC08 ⇒ None ?
+             | HCS08 ⇒ None ?
+             | RS08 ⇒ None ?
+             | IP2022 ⇒ Some ? set_page_reg_IP2022 ])
+ (λf.Some ? (set_alu m t s (f (alu m t s) page'))).
+
+(* setter debole di PAGE *)
+ndefinition setweak_page_reg ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λpage':oct.
+ match set_page_reg m t s page' with
+  [ None ⇒ s | Some s' ⇒ s' ].
+
+(* REGISTRO MEMORY MAPPED X *)
 
 (* setter forte di memory mapped X *)
 ndefinition set_x_map ≝
@@ -412,7 +394,8 @@ ndefinition set_x_map ≝
              [ HC05 ⇒ None ?
              | HC08 ⇒ None ?
              | HCS08 ⇒ None ?
-             | RS08 ⇒ Some ? set_x_map_RS08 ])
+             | RS08 ⇒ Some ? set_x_map_RS08
+             | IP2022 ⇒ None ? ])
  (λf.Some ? (set_alu m t s (f (alu m t s) xm'))).
 
 (* setter debole di memory mapped X *)
@@ -423,19 +406,6 @@ ndefinition setweak_x_map ≝
 
 (* 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).
-
 (* setter forte di memory mapped PS *)
 ndefinition set_ps_map ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λpsm':byte8.
@@ -443,7 +413,8 @@ ndefinition set_ps_map ≝
              [ HC05 ⇒ None ?
              | HC08 ⇒ None ?
              | HCS08 ⇒ None ?
-             | RS08 ⇒ Some ? set_ps_map_RS08 ])
+             | RS08 ⇒ Some ? set_ps_map_RS08
+             | IP2022 ⇒ None ? ])
  (λf.Some ? (set_alu m t s (f (alu m t s) psm'))).
 
 (* setter debole di memory mapped PS *)
@@ -452,24 +423,26 @@ ndefinition setweak_ps_map ≝
  match set_ps_map m t s psm' with
   [ None ⇒ s | Some s' ⇒ s' ].
 
-(* FLAG V *)
+(* MODALITA SKIP *)
 
-(* 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).
+(* setter forte di SKIP *)
+ndefinition set_skip_mode ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λskipmode':bool.
+ opt_map … (match m return aux_set_type_opt bool with
+             [ HC05 ⇒ None ?
+             | HC08 ⇒ None ?
+             | HCS08 ⇒ None ?
+             | RS08 ⇒ None ?
+             | IP2022 ⇒ Some ? set_skip_mode_IP2022 ])
+ (λf.Some ? (set_alu m t s (f (alu m t s) skipmode'))).
+
+(* setter debole  di SKIP *)
+ndefinition setweak_skip_mode ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λskipmode':bool.
+ match set_skip_mode m t s skipmode' with
+  [ None ⇒ s | Some s' ⇒ s' ].
+
+(* FLAG V *)
 
 (* setter forte di V *)
 ndefinition set_v_flag ≝
@@ -478,7 +451,8 @@ ndefinition set_v_flag ≝
              [ HC05 ⇒ None ?
              | HC08 ⇒ Some ? set_v_flag_HC08
              | HCS08 ⇒ Some ? set_v_flag_HC08
-             | RS08 ⇒ None ? ])
+             | RS08 ⇒ None ?
+             | IP2022 ⇒ None ? ])
  (λf.Some ? (set_alu m t s (f (alu m t s) vfl'))).
 
 (* setter debole  di V *)
@@ -489,41 +463,6 @@ ndefinition setweak_v_flag ≝
 
 (* 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).
-
 (* setter forte di H *)
 ndefinition set_h_flag ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λhfl':bool.
@@ -531,7 +470,8 @@ ndefinition set_h_flag ≝
              [ HC05 ⇒ Some ? set_h_flag_HC05
              | HC08 ⇒ Some ? set_h_flag_HC08
              | HCS08 ⇒ Some ? set_h_flag_HC08
-             | RS08 ⇒ None ? ])
+             | RS08 ⇒ None ?
+             | IP2022 ⇒ Some ? set_h_flag_IP2022 ])
  (λf.Some ? (set_alu m t s (f (alu m t s) hfl'))).
 
 (* setter debole di H *)
@@ -542,41 +482,6 @@ ndefinition setweak_h_flag ≝
 
 (* 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).
-
 (* setter forte di I *)
 ndefinition set_i_flag ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λifl':bool.
@@ -584,7 +489,8 @@ ndefinition set_i_flag ≝
              [ HC05 ⇒ Some ? set_i_flag_HC05
              | HC08 ⇒ Some ? set_i_flag_HC08
              | HCS08 ⇒ Some ? set_i_flag_HC08
-             | RS08 ⇒ None ? ])
+             | RS08 ⇒ None ?
+             | IP2022 ⇒ None ? ])
  (λf.Some ? (set_alu m t s (f (alu m t s) ifl'))).
 
 (* setter debole di I *)
@@ -595,41 +501,6 @@ ndefinition setweak_i_flag ≝
 
 (* 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).
-
 (* setter forte di N *)
 ndefinition set_n_flag ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λnfl':bool.
@@ -637,7 +508,8 @@ ndefinition set_n_flag ≝
              [ HC05 ⇒ Some ? set_n_flag_HC05
              | HC08 ⇒ Some ? set_n_flag_HC08
              | HCS08 ⇒ Some ? set_n_flag_HC08
-             | RS08 ⇒ None ? ])
+             | RS08 ⇒ None ?
+             | IP2022 ⇒ None ? ])
  (λf.Some ? (set_alu m t s (f (alu m t s) nfl'))).
 
 (* setter debole di N *)
@@ -648,54 +520,6 @@ ndefinition setweak_n_flag ≝
 
 (* 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.
@@ -705,58 +529,11 @@ ndefinition set_z_flag ≝
   | 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.
@@ -766,45 +543,11 @@ ndefinition set_c_flag ≝
   | 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'.
-
 (* setter forte di IRQ *)
 ndefinition set_irq_flag ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λirqfl':bool.
@@ -812,7 +555,8 @@ ndefinition set_irq_flag ≝
              [ HC05 ⇒ Some ? set_irq_flag_HC05
              | HC08 ⇒ Some ? set_irq_flag_HC08
              | HCS08 ⇒ Some ? set_irq_flag_HC08
-             | RS08 ⇒ None ? ])
+             | RS08 ⇒ None ?
+             | IP2022 ⇒ None ? ])
  (λf.Some ? (set_alu m t s (f (alu m t s) irqfl'))).
 
 (* setter debole di IRQ *)