From 2c38e6a237e6a0e263abccf8d8ef3e7a31272443 Mon Sep 17 00:00:00 2001
From: Cosimo Oliboni <??>
Date: Mon, 1 Feb 2010 12:40:32 +0000
Subject: [PATCH]

---
 .../read_write/Freescale_load_write.ma        |  10 +-
 .../emulator/read_write/IP2022_load_write.ma  | 215 +++++-
 .../emulator/read_write/IP2022_read_write.ma  |  44 +-
 .../ng_assembly/emulator/read_write/fetch.ma  |  27 +-
 .../emulator/read_write/load_write.ma         |   8 +-
 .../emulator/read_write/load_write_base.ma    |   4 -
 .../emulator/read_write/read_write.ma         |   8 +-
 .../emulator/status/IP2022_status.ma          |  49 +-
 .../emulator/status/status_getter.ma          |  34 +-
 .../emulator/status/status_setter.ma          | 693 ++++++++++++------
 .../matita/contribs/ng_assembly/num/word24.ma |   2 +
 11 files changed, 724 insertions(+), 370 deletions(-)
 mode change 100755 => 100644 helm/software/matita/contribs/ng_assembly/emulator/read_write/load_write_base.ma

diff --git a/helm/software/matita/contribs/ng_assembly/emulator/read_write/Freescale_load_write.ma b/helm/software/matita/contribs/ng_assembly/emulator/read_write/Freescale_load_write.ma
index be04ff2f1..f14b38b19 100755
--- a/helm/software/matita/contribs/ng_assembly/emulator/read_write/Freescale_load_write.ma
+++ b/helm/software/matita/contribs/ng_assembly/emulator/read_write/Freescale_load_write.ma
@@ -20,8 +20,8 @@
 (*                                                                        *)
 (* ********************************************************************** *)
 
-include "emulator/read_write/load_write_base.ma".
 include "emulator/status/status_getter.ma".
+include "emulator/read_write/load_write_base.ma".
 
 (* lettura da [curpc]: IMM1 *)
 ndefinition mode_IMM1_load ≝
@@ -195,7 +195,7 @@ ndefinition aux_inc_indX_16 ≝
    (λs_tmp.Some ? s_tmp)).
 
 ndefinition Freescale_multi_mode_load_auxb ≝
-λm,t.λs:any_status m t.λcur_pc:word16.λi:Freescale_instr_mode.match i with
+λm,t.λs:any_status m t.λpco,cur_pc:word16.λi:Freescale_instr_mode.match i with
 (* NO: non ci sono indicazioni *)
    [ MODE_INH  ⇒ None ?
 (* restituisce A *)
@@ -276,7 +276,7 @@ ndefinition Freescale_multi_mode_load_auxb ≝
    ].
 
 ndefinition Freescale_multi_mode_load_auxw ≝
-λm,t.λs:any_status m t.λcur_pc:word16.λi:Freescale_instr_mode.match i with
+λm,t.λs:any_status m t.λpco,cur_pc:word16.λi:Freescale_instr_mode.match i with
 (* NO: non ci sono indicazioni *)
    [ MODE_INH  ⇒ None ?
 (* NO: solo lettura/scrittura byte *)
@@ -417,7 +417,7 @@ ndefinition Freescale_multi_mode_load_auxw ≝
 (* **************************************** *)
 
 ndefinition Freescale_multi_mode_write_auxb ≝
-λm,t.λs:any_status m t.λcur_pc:word16.λi:Freescale_instr_mode.λwriteb:byte8.match i with
+λm,t.λs:any_status m t.λpco,cur_pc:word16.λflag:aux_mod_type.λi:Freescale_instr_mode.λwriteb:byte8.match i with
 (* NO: non ci sono indicazioni *)
   [ MODE_INH        ⇒ None ?
 (* scrive A *)
@@ -507,7 +507,7 @@ ndefinition Freescale_multi_mode_write_auxb ≝
   ].
 
 ndefinition Freescale_multi_mode_write_auxw ≝
-λm,t.λs:any_status m t.λcur_pc:word16.λi:Freescale_instr_mode.λwritew:word16.match i with
+λm,t.λs:any_status m t.λpco,cur_pc:word16.λi:Freescale_instr_mode.λwritew:word16.match i with
 (* NO: non ci sono indicazioni *)
   [ MODE_INH        ⇒ None ?
 (* NO: solo lettura/scrittura byte *)
diff --git a/helm/software/matita/contribs/ng_assembly/emulator/read_write/IP2022_load_write.ma b/helm/software/matita/contribs/ng_assembly/emulator/read_write/IP2022_load_write.ma
index 5e9a7d231..eccc4eefb 100755
--- a/helm/software/matita/contribs/ng_assembly/emulator/read_write/IP2022_load_write.ma
+++ b/helm/software/matita/contribs/ng_assembly/emulator/read_write/IP2022_load_write.ma
@@ -20,13 +20,19 @@
 (*                                                                        *)
 (* ********************************************************************** *)
 
-include "emulator/read_write/load_write_base.ma".
 include "emulator/status/status_getter.ma".
+include "emulator/read_write/load_write_base.ma".
 
-(* lettura da [PC<<1 - 1] : argomento non caricato dal fetch word-aligned *)
+(* lettura da [OLD PC<<1 + 1] : argomento non caricato dal fetch word-aligned *)
 ndefinition mode_IMM1_load ≝
-λt:memory_impl.λs:any_status IP2022 t.
- mem_read_s … s (rol_w32 〈〈〈x8,x1〉:〈x0,x0〉〉.(pred_w16 (get_pc_reg … s))〉).
+λt:memory_impl.λs:any_status IP2022 t.λpco:word16.
+ mem_read_s … s (rol_w32 〈〈〈x8,x1〉:〈x0,x0〉〉.pco〉).
+
+(* SCHEMA:
+   ADDRX=0x00 [ADDRH|ADDRL] 16Kb PROGRAM RAM
+   ADDRX=0x01 [ADDRH|ADDRL] 64Kb FLASH
+   ADDRX=0x80 [ADDRH|ADDRL] 64Kb EXTERNAL RAM
+   ADDRX=0x81 [ADDRH|ADDRL] 64Kb EXTERNAL RAM *)
 
 (* lettura da [ADDR] *)
 ndefinition mode_ADDR_load ≝
@@ -35,22 +41,22 @@ ndefinition mode_ADDR_load ≝
   (λaddr.match (eq_b8 (w24x addr) 〈x0,x1〉) ⊗ (le_w16 (pred_w16 (get_pc_reg … s)) 〈〈x1,xF〉:〈xF,xF〉〉) with
    (* lettura della FLASH da codice in RAM : operazione non bloccante non implementata! *)
    [ true ⇒ None ?
-   | false ⇒ opt_map … (memory_filter_read … s 〈〈〈x0,x2〉:(w24x addr)〉.〈(w24h addr):(w24l addr)〉〉)
-             (λbh.opt_map … (memory_filter_read … s 〈〈〈x0,x2〉:(w24x (succ_w24 addr))〉.〈(w24h (succ_w24 addr)):(w24l (succ_w24 addr))〉〉)
+   | false ⇒ opt_map … (memory_filter_read … s 〈〈〈x0,x2〉:(w24x addr)〉.〈(w24h addr):(clrLSB_b8 (w24l addr))〉〉)
+             (λbh.opt_map … (memory_filter_read … s 〈〈〈x0,x2〉:(w24x addr)〉.〈(w24h addr):(setLSB_b8 (w24l addr))〉〉)
               (λbl.Some ? 〈bh:bl〉))]).
 
 (* scrittura su [ADDR] *)
 ndefinition mode_ADDR_write ≝
 λt:memory_impl.λs:any_status IP2022 t.λval:word16.
  opt_map … (get_addr_reg … s)
-  (λaddr.opt_map … (memory_filter_write … s 〈〈〈x0,x2〉:(w24x addr)〉.〈(w24h addr):(w24l addr)〉〉 auxMode_ok (cnH ? val))
-   (λs'.memory_filter_write … s' 〈〈〈x0,x2〉:(w24x (succ_w24 addr))〉.〈(w24h (succ_w24 addr)):(w24l (succ_w24 addr))〉〉 auxMode_ok (cnL ? val))).
+  (λaddr.opt_map … (memory_filter_write … s 〈〈〈x0,x2〉:(w24x addr)〉.〈(w24h addr):(clrLSB_b8 (w24l addr))〉〉 auxMode_ok (cnH ? val))
+   (λs'.memory_filter_write … s' 〈〈〈x0,x2〉:(w24x addr)〉.〈(w24h addr):(setLSB_b8 (w24l addr))〉〉 auxMode_ok (cnL ? val))).
 
 (* IMM1 > 0 : lettura/scrittura da [IMM1] *)
 (* else     : lettura/scrittura da [IP] : IP ≥ 0x20 *)
 ndefinition mode_DIR1IP_aux ≝
-λt:memory_impl.λs:any_status IP2022 t.λT.λf:word32 → option T.
- opt_map … (mode_IMM1_load t s)
+λt:memory_impl.λs:any_status IP2022 t.λpco:word16.λT.λf:word32 → option T.
+ opt_map … (mode_IMM1_load t s pco)
   (λaddr.match eq_b8 addr 〈x0,x0〉 with
    (* xxxxxxx0 00000000 → [IP] *)
    [ true ⇒ opt_map … (get_ip_reg … s)
@@ -65,8 +71,8 @@ ndefinition mode_DIR1IP_aux ≝
 (* IMM1 < 0x80 : lettura/scrittura da [DP+IMM1] : DP+IMM1 ≥ 0x20 *)
 (* else        : lettura/scrittura da [SP+IMM1] : SP+IMM1 ≥ 0x20 *)
 ndefinition mode_DPSP_aux ≝
-λt:memory_impl.λs:any_status IP2022 t.λT.λf:word32 → option T.
- opt_map … (mode_IMM1_load t s)
+λt:memory_impl.λs:any_status IP2022 t.λpco:word16.λT.λf:word32 → option T.
+ opt_map … (mode_IMM1_load t s pco)
   (λaddr.opt_map … (match getMSB_b8 addr with
                     (* xxxxxxx1 1nnnnnnn → [SP+IMM1] *)
                     [ true ⇒ get_sp_reg … s
@@ -79,34 +85,187 @@ ndefinition mode_DPSP_aux ≝
 
 (* FR0 *)
 ndefinition mode_FR0_load ≝
-λt:memory_impl.λs:any_status IP2022 t.
- mode_DIR1IP_aux t s byte8 (memory_filter_read … s).
+λt:memory_impl.λs:any_status IP2022 t.λpco:word16.
+ mode_DIR1IP_aux t s pco byte8 (memory_filter_read … s).
 
 ndefinition mode_FR0n_load ≝
-λt:memory_impl.λs:any_status IP2022 t.λsub:oct.
- mode_DIR1IP_aux t s bool (λaddr.memory_filter_read_bit … s addr sub).
+λt:memory_impl.λs:any_status IP2022 t.λpco:word16.λsub:oct.
+ mode_DIR1IP_aux t s pco bool (λaddr.memory_filter_read_bit … s addr sub).
 
 ndefinition mode_FR0_write ≝
-λt:memory_impl.λs:any_status IP2022 t.λflag:aux_mod_type.λval:byte8.
- mode_DIR1IP_aux t s (any_status IP2022 t) (λaddr.memory_filter_write … s addr flag val).
+λt:memory_impl.λs:any_status IP2022 t.λpco:word16.λflag:aux_mod_type.λval:byte8.
+ mode_DIR1IP_aux t s pco (any_status IP2022 t) (λaddr.memory_filter_write … s addr flag val).
 
 ndefinition mode_FR0n_write ≝
-λt:memory_impl.λs:any_status IP2022 t.λsub:oct.λval:bool.
- mode_DIR1IP_aux t s (any_status IP2022 t) (λaddr.memory_filter_write_bit … s addr sub val).
+λt:memory_impl.λs:any_status IP2022 t.λpco:word16.λsub:oct.λval:bool.
+ mode_DIR1IP_aux t s pco (any_status IP2022 t) (λaddr.memory_filter_write_bit … s addr sub val).
 
 (* FR1 *)
 ndefinition mode_FR1_load ≝
-λt:memory_impl.λs:any_status IP2022 t.
- mode_DPSP_aux t s byte8 (memory_filter_read … s).
+λt:memory_impl.λs:any_status IP2022 t.λpco:word16.
+ mode_DPSP_aux t s pco byte8 (memory_filter_read … s).
 
 ndefinition mode_FR1n_load ≝
-λt:memory_impl.λs:any_status IP2022 t.λsub:oct.
- mode_DPSP_aux t s bool (λaddr.memory_filter_read_bit … s addr sub).
+λt:memory_impl.λs:any_status IP2022 t.λpco:word16.λsub:oct.
+ mode_DPSP_aux t s pco bool (λaddr.memory_filter_read_bit … s addr sub).
 
 ndefinition mode_FR1_write ≝
-λt:memory_impl.λs:any_status IP2022 t.λflag:aux_mod_type.λval:byte8.
- mode_DPSP_aux t s (any_status IP2022 t) (λaddr.memory_filter_write … s addr flag val).
+λt:memory_impl.λs:any_status IP2022 t.λpco:word16.λflag:aux_mod_type.λval:byte8.
+ mode_DPSP_aux t s pco (any_status IP2022 t) (λaddr.memory_filter_write … s addr flag val).
 
 ndefinition mode_FR1n_write ≝
-λt:memory_impl.λs:any_status IP2022 t.λsub:oct.λval:bool.
- mode_DPSP_aux t s (any_status IP2022 t) (λaddr.memory_filter_write_bit … s addr sub val).
+λt:memory_impl.λs:any_status IP2022 t.λpco:word16.λsub:oct.λval:bool.
+ mode_DPSP_aux t s pco (any_status IP2022 t) (λaddr.memory_filter_write_bit … s addr sub val).
+
+(* ************************************** *)
+(* raccordo di tutte le possibili letture *)
+(* ************************************** *)
+
+(* addr+=2 *)
+ndefinition aux_inc_addr2 ≝
+λt:memory_impl.λs:any_status IP2022 t.
+ set_addr_reg_sIP2022 t s (succ_w24 (succ_w24 (get_addr_reg_IP2022 (alu … s)))).
+
+ndefinition IP2022_multi_mode_load_auxb ≝
+λt.λs:any_status IP2022 t.λpco,cur_pc:word16.λi:IP2022_instr_mode.match i with
+(* NO: non ci sono indicazioni *)
+   [ MODE_INH ⇒ None ?
+(* NO: solo word *)
+   | MODE_INHADDR ⇒ None ?
+(* NO: solo word *)
+   | MODE_INHADDRpp ⇒ None ?
+
+(* IMM3 *)
+   | MODE_IMM3 o ⇒ Some ? (triple … s (extu_b8 (ex_of_oct o)) cur_pc)
+(* IMM8 *)
+   | MODE_IMM8 ⇒ opt_map … (mode_IMM1_load t s pco)
+                  (λb.Some ? (triple … s b cur_pc))
+(* NO: solo lettura word *)
+   | MODE_IMM13 _ ⇒ None ?
+
+(* NO: solo word *)
+   | MODE_FR0_and_W ⇒ None ?
+(* NO: solo word *)
+   | MODE_FR1_and_W ⇒ None ?
+(* NO: solo word *)
+   | MODE_W_and_FR0 ⇒ None ?
+(* NO: solo word *)
+   | MODE_W_and_FR1 ⇒ None ?
+
+(* [FRn] *)
+   | MODE_FR0n o ⇒ opt_map … (mode_FR0n_load t s pco o)
+                    (λb.Some ? (triple … s (extu_b8 (match b with [ true ⇒ x1 | false ⇒ x0 ])) cur_pc))
+(* [FRn] *)
+   | MODE_FR1n o ⇒ opt_map … (mode_FR1n_load t s pco o)
+                    (λb.Some ? (triple … s (extu_b8 (match b with [ true ⇒ x1 | false ⇒ x0 ])) cur_pc))
+   ].
+
+ndefinition IP2022_multi_mode_load_auxw ≝
+λt.λs:any_status IP2022 t.λpco,cur_pc:word16.λi:IP2022_instr_mode.match i with
+(* NO: non ci sono indicazioni *)
+   [ MODE_INH ⇒ None ?
+(* [ADDR] *)
+   | MODE_INHADDR ⇒ opt_map … (mode_ADDR_load t s)
+                     (λw.Some ? (triple … s w cur_pc))
+(* [ADDR], ADDR+=2 *)
+   | MODE_INHADDRpp ⇒ opt_map … (mode_ADDR_load t s)
+                       (λw.Some ? (triple … (aux_inc_addr2 t s) w cur_pc))
+
+(* NO: solo lettura byte *)
+   | MODE_IMM3 _ ⇒ None ?
+(* NO: solo lettura byte *)
+   | MODE_IMM8 ⇒ None ?
+(* IMM13 *)
+   | MODE_IMM13 bt ⇒ opt_map … (mode_IMM1_load t s pco)
+                      (λb.Some ? (triple … s 〈(b8_of_bit bt):b〉 cur_pc))
+
+(* FR, W → FR *)
+   | MODE_FR0_and_W ⇒ opt_map … (mode_FR0_load t s pco)
+                       (λfr.Some ? (triple … s 〈fr:(get_acc_8_low_reg … s)〉 cur_pc))
+(* FR, W → FR *)
+   | MODE_FR1_and_W ⇒ opt_map … (mode_FR1_load t s pco)
+                       (λfr.Some ? (triple … s 〈fr:(get_acc_8_low_reg … s)〉 cur_pc))
+(* W, FR → W *)
+   | MODE_W_and_FR0 ⇒ opt_map … (mode_FR0_load t s pco)
+                       (λfr.Some ? (triple … s 〈(get_acc_8_low_reg … s):fr〉 cur_pc))
+(* W, FR → W *)
+   | MODE_W_and_FR1 ⇒ opt_map … (mode_FR1_load t s pco)
+                       (λfr.Some ? (triple … s 〈(get_acc_8_low_reg … s):fr〉 cur_pc))
+
+(* NO: solo byte *)
+   | MODE_FR0n _ ⇒ None ?
+(* NO: solo byte *)
+   | MODE_FR1n _ ⇒ None ?
+   ].
+
+(* **************************************** *)
+(* raccordo di tutte le possibili scritture *)
+(* **************************************** *)
+
+ndefinition IP2022_multi_mode_write_auxb ≝
+λt.λs:any_status IP2022 t.λpco,cur_pc:word16.λflag:aux_mod_type.λi:IP2022_instr_mode.λwriteb:byte8.match i with
+(* NO: non ci sono indicazioni *)
+   [ MODE_INH ⇒ None ?
+(* NO: solo word *)
+   | MODE_INHADDR ⇒ None ?
+(* NO: solo word *)
+   | MODE_INHADDRpp ⇒ None ?
+
+(* NO: solo lettura byte *)
+   | MODE_IMM3 _ ⇒ None ?
+(* NO: solo lettura byte *)
+   | MODE_IMM8 ⇒ None ?
+(* NO: solo lettura word *)
+   | MODE_IMM13 _ ⇒ None ?
+
+(* FR, W → FR *)
+   | MODE_FR0_and_W ⇒ opt_map … (mode_FR0_write t s pco flag writeb)
+                       (λs'.Some ? (pair … s' cur_pc))
+(* FR, W → FR *)
+   | MODE_FR1_and_W ⇒ opt_map … (mode_FR1_write t s pco flag writeb)
+                       (λs'.Some ? (pair … s' cur_pc))
+(* W, FR → W *)
+   | MODE_W_and_FR0 ⇒ Some ? (pair … (set_acc_8_low_reg … s writeb) cur_pc)
+(* W, FR → W *)
+   | MODE_W_and_FR1 ⇒ Some ? (pair … (set_acc_8_low_reg … s writeb) cur_pc)
+
+(* [FRn] *)
+   | MODE_FR0n o ⇒ opt_map … (mode_FR0n_write t s pco o (getn_array8T o ? (bits_of_byte8 writeb)))
+                    (λs'.Some ? (pair … s' cur_pc))
+(* [FRn] *)
+   | MODE_FR1n o ⇒ opt_map … (mode_FR1n_write t s pco o (getn_array8T o ? (bits_of_byte8 writeb)))
+                    (λs'.Some ? (pair … s' cur_pc))
+   ].
+
+ndefinition IP2022_multi_mode_write_auxw ≝
+λt.λs:any_status IP2022 t.λpco,cur_pc:word16.λi:IP2022_instr_mode.λwritew:word16.match i with
+(* NO: non ci sono indicazioni *)
+   [ MODE_INH ⇒ None ?
+(* [ADDR] *)
+   | MODE_INHADDR ⇒ opt_map … (mode_ADDR_write t s writew)
+                     (λs'.Some ? (pair … s' cur_pc))
+(* [ADDR], ADDR+=2 *)
+   | MODE_INHADDRpp ⇒ opt_map … (mode_ADDR_write t s writew)
+                       (λs'.Some ? (pair … (aux_inc_addr2 t s') cur_pc))
+
+(* NO: solo lettura byte *)
+   | MODE_IMM3 _ ⇒ None ?
+(* NO: solo lettura byte *)
+   | MODE_IMM8 ⇒ None ?
+(* NO: solo lettura word *)
+   | MODE_IMM13 _ ⇒ None ?
+
+(* NO: solo byte *)
+   | MODE_FR0_and_W ⇒ None ?
+(* NO: solo byte *)
+   | MODE_FR1_and_W ⇒ None ?
+(* NO: solo byte *)
+   | MODE_W_and_FR0 ⇒ None ?
+(* NO: solo byte *)
+   | MODE_W_and_FR1 ⇒ None ?
+
+(* NO: solo byte *)
+   | MODE_FR0n _ ⇒ None ?
+(* NO: solo byte *)
+   | MODE_FR1n _ ⇒ None ?
+   ].
diff --git a/helm/software/matita/contribs/ng_assembly/emulator/read_write/IP2022_read_write.ma b/helm/software/matita/contribs/ng_assembly/emulator/read_write/IP2022_read_write.ma
index 3cb7b1f51..8ed36c36f 100755
--- a/helm/software/matita/contribs/ng_assembly/emulator/read_write/IP2022_read_write.ma
+++ b/helm/software/matita/contribs/ng_assembly/emulator/read_write/IP2022_read_write.ma
@@ -149,7 +149,7 @@ ndefinition IP2022_memory_filter_read_bit ≝
 ndefinition high_write_aux_w16 ≝
 λf:byte8 → byte8.λw:word16.〈(f (cnH ? w)):(cnL ? w)〉.
 
-ndefinition low_write_aux_w16 ≝
+ndefinition lowc_write_aux_w16 ≝
 λf:byte8 → byte8.λw:word16.λflag:aux_mod_type.
  〈((match flag with
     [ auxMode_ok ⇒ λx.x
@@ -157,6 +157,9 @@ ndefinition low_write_aux_w16 ≝
     | auxMode_dec ⇒ pred_b8 ]) (cnH ? w)):
   (f (cnL ? w))〉.
 
+ndefinition lownc_write_aux_w16 ≝
+λf:byte8 → byte8.λw:word16.〈(cnH ? w):(f (cnL ? w))〉.
+
 ndefinition ext_write_aux_w24 ≝
 λf:byte8 → byte8.λw:word24.〈(f (w24x w));(w24h w);(w24l w)〉.
 
@@ -172,13 +175,14 @@ ndefinition low_write_aux_w24 ≝
   [ mk_comp_num wx' wh' ⇒ 〈wx';wh';(w24l w)〉 ].
 
 (* flag di carry: riportare il carry al byte logicamente superiore *)
+(* modifica di pc: non inserita nella stato ma postposta *)
 ndefinition IP2022_memory_filter_write_aux ≝
 λt:memory_impl.λs:any_status IP2022 t.λaddr:word32.λflag:aux_mod_type.
 λfREG:byte8 → byte8.λfMEM:aux_mem_type t → aux_chk_type t → word32 → option (aux_mem_type t).
 (* intercettare le locazioni memory mapped *)
  match eq_w32 addr IP2022_ADDRSEL_loc with
   [ true ⇒ set_addrsel_reg … s (fREG (addrsel_reg_IP2022 (alu … s)))
-  | false ⇒
+  | false ⇒ 
  match eq_w32 addr IP2022_ADDRX_loc with
   [ true ⇒ set_addr_reg … s (ext_write_aux_w24 fREG (get_addrarray (addrsel_reg_IP2022 (alu … s))
                                                                    (addr_array_IP2022 (alu … s))))
@@ -187,16 +191,16 @@ ndefinition IP2022_memory_filter_write_aux ≝
   [ true ⇒ set_ip_reg … s (high_write_aux_w16 fREG (ip_reg_IP2022 (alu … s)))
   | false ⇒
  match eq_w32 addr IP2022_IPL_loc with
-  [ true ⇒ set_ip_reg … s (low_write_aux_w16 fREG (ip_reg_IP2022 (alu … s)) flag)
+  [ true ⇒ set_ip_reg … s (lowc_write_aux_w16 fREG (ip_reg_IP2022 (alu … s)) flag)
   | false ⇒
  match eq_w32 addr IP2022_SPH_loc with
   [ true ⇒ set_sp_reg … s (high_write_aux_w16 fREG (sp_reg_IP2022 (alu … s)))
   | false ⇒
  match eq_w32 addr IP2022_SPL_loc with
-  [ true ⇒ set_sp_reg … s (low_write_aux_w16 fREG (sp_reg_IP2022 (alu … s)) flag)
+  [ true ⇒ set_sp_reg … s (lowc_write_aux_w16 fREG (sp_reg_IP2022 (alu … s)) flag)
   | false ⇒
  match eq_w32 addr IP2022_PCL_loc with
-  [ true ⇒ Some ? (set_pc_reg … s (low_write_aux_w16 fREG (pc_reg_IP2022 (alu … s)) flag))
+  [ true ⇒ Some ? (set_pc_reg … s (lowc_write_aux_w16 fREG (pc_reg_IP2022 (alu … s)) flag))
   | false ⇒
  match eq_w32 addr IP2022_W_loc with
   [ true ⇒ Some ? (set_acc_8_low_reg … s (fREG (acc_low_reg_IP2022 (alu … s))))
@@ -205,7 +209,7 @@ ndefinition IP2022_memory_filter_write_aux ≝
   [ true ⇒ set_dp_reg … s (high_write_aux_w16 fREG (dp_reg_IP2022 (alu … s)))
   | false ⇒
  match eq_w32 addr IP2022_DPL_loc with
-  [ true ⇒ set_dp_reg … s (low_write_aux_w16 fREG (dp_reg_IP2022 (alu … s)) flag)
+  [ true ⇒ set_dp_reg … s (lowc_write_aux_w16 fREG (dp_reg_IP2022 (alu … s)) flag)
   | false ⇒
  match eq_w32 addr IP2022_MULH_loc with
   [ true ⇒ set_mulh_reg … s (fREG (mulh_reg_IP2022 (alu … s)))
@@ -221,17 +225,20 @@ ndefinition IP2022_memory_filter_write_aux ≝
  match eq_w32 addr IP2022_DATAH_loc with
   [ true ⇒ set_data_reg … s (high_write_aux_w16 fREG (data_reg_IP2022 (alu … s)))
   | false ⇒
+(* nessun riporto automatico *)
  match eq_w32 addr IP2022_DATAL_loc with
-  [ true ⇒ set_data_reg … s (low_write_aux_w16 fREG (data_reg_IP2022 (alu … s)) flag)
+  [ true ⇒ set_data_reg … s (lownc_write_aux_w16 fREG (data_reg_IP2022 (alu … s)))
   | false ⇒
  match eq_w32 addr IP2022_CALLH_loc with
   [ true ⇒ set_call_reg … s (high_write_aux_w16 fREG (getn_array16T x0 ? (call_stack_IP2022 (alu … s))))
   | false ⇒
+(* nessun riporto automatico *)
  match eq_w32 addr IP2022_CALLL_loc with
-  [ true ⇒ set_call_reg … s (low_write_aux_w16 fREG (getn_array16T x0 ? (call_stack_IP2022 (alu … s))) flag)
+  [ true ⇒ set_call_reg … s (lownc_write_aux_w16 fREG (getn_array16T x0 ? (call_stack_IP2022 (alu … s))))
 (* accesso normale *)
   | false ⇒ opt_map … (fMEM (mem_desc … s) (chk_desc … s) addr)
-             (λmem'.Some ? (set_mem_desc … s mem')) ]]]]]]]]]]]]]]]]].
+             (λmem'.Some ? (set_mem_desc … s mem'))
+  ]]]]]]]]]]]]]]]]].
 
 (* scrittura IP2022 di un byte *)
 ndefinition IP2022_memory_filter_write ≝
@@ -239,15 +246,16 @@ ndefinition IP2022_memory_filter_write ≝
 λaddr:word32.λflag:aux_mod_type.λval:byte8.
  (* PAGE[7:5] Z[2] H[1] C [0] *)
  match eq_w32 addr IP2022_STATUS_loc with
-  [ true ⇒ Some ? (set_alu … s
-            (set_page_reg_IP2022
-             (set_z_flag_IP2022
-              (set_h_flag_IP2022
-               (set_c_flag_IP2022 (alu … s)
-                (getn_array8T o7 ? (bits_of_byte8 val)))
-               (getn_array8T o6 ? (bits_of_byte8 val)))
-              (getn_array8T o5 ? (bits_of_byte8 val)))
-             (oct_of_exH (cnH ? val))))
+  [ true ⇒ Some ? 
+            (set_alu … s
+             (set_page_reg_IP2022
+              (set_z_flag_IP2022
+               (set_h_flag_IP2022
+                (set_c_flag_IP2022 (alu … s)
+                 (getn_array8T o7 ? (bits_of_byte8 val)))
+                (getn_array8T o6 ? (bits_of_byte8 val)))
+               (getn_array8T o5 ? (bits_of_byte8 val)))
+              (oct_of_exH (cnH ? val))))
  (* accesso a registro_non_spezzato/normale *)
   | false ⇒ IP2022_memory_filter_write_aux t s addr flag
              (λb.val)
diff --git a/helm/software/matita/contribs/ng_assembly/emulator/read_write/fetch.ma b/helm/software/matita/contribs/ng_assembly/emulator/read_write/fetch.ma
index 37d095106..1d51f2bcf 100755
--- a/helm/software/matita/contribs/ng_assembly/emulator/read_write/fetch.ma
+++ b/helm/software/matita/contribs/ng_assembly/emulator/read_write/fetch.ma
@@ -31,23 +31,23 @@ ninductive error_type : Type ≝
 .
 
 (* - errore: interessa solo l'errore
-   - ok: interessa info e il nuovo pc *)
+   - ok: interessa info, vecchio pc, nuovo pc *)
 ninductive fetch_result (A:Type) : Type ≝
   FetchERR : error_type → fetch_result A
-| FetchOK  : A → word16 → fetch_result A.
+| FetchOK  : A → word16 → word16 → fetch_result A.
 
 ndefinition fetch_byte_aux ≝
-λm:mcu_type.λpc:word16.λbh:byte8.
+λm:mcu_type.λpco,pcn:word16.λbh:byte8.
  match full_info_of_word16 m (Byte bh) with
   [ None ⇒ FetchERR ? ILL_FETCH_AD
-  | Some info ⇒ FetchOK ? info pc
+  | Some info ⇒ FetchOK ? info pco pcn
   ].
 
 ndefinition fetch_word_aux ≝
-λm:mcu_type.λpc:word16.λw:word16.
+λm:mcu_type.λpco,pcn:word16.λw:word16.
  match full_info_of_word16 m (Word w) with
   [ None ⇒ FetchERR ? ILL_FETCH_AD
-  | Some info ⇒ FetchOK ? info pc
+  | Some info ⇒ FetchOK ? info pco pcn
   ].
 
 (* opcode a byte : HC05 / RS08 *)
@@ -55,7 +55,7 @@ ndefinition fetch_byte ≝
 λm:mcu_type.λfR:word32 → option byte8.λpc:word16.
  match fR (extu_w32 pc) with
   [ None ⇒ FetchERR ? ILL_FETCH_AD
-  | Some bh ⇒ fetch_byte_aux m (succ_w16 pc) bh ].
+  | Some bh ⇒ fetch_byte_aux m pc (succ_w16 pc) bh ].
 
 (* opcode a byte o 0x9E + byte : HC08 / HCS08 *)
 ndefinition Freescale_fetch_byte_or_word ≝
@@ -65,9 +65,9 @@ ndefinition Freescale_fetch_byte_or_word ≝
   | Some bh ⇒ match eq_b8 bh 〈x9,xE〉 with
    [ true ⇒ match fR (extu_w32 (succ_w16 pc)) with
     [ None ⇒ FetchERR ? ILL_FETCH_AD
-    | Some bl ⇒ fetch_word_aux m (succ_w16 (succ_w16 pc)) 〈bh:bl〉
+    | Some bl ⇒ fetch_word_aux m pc (succ_w16 (succ_w16 pc)) 〈bh:bl〉
     ]
-   | false ⇒ fetch_byte_aux m (succ_w16 pc) bh
+   | false ⇒ fetch_byte_aux m pc (succ_w16 pc) bh
    ]
   ].
 
@@ -76,15 +76,14 @@ ndefinition Freescale_fetch_byte_or_word ≝
 (* pc word aligned, mappato in 0x02000000-0x0201FFFF *)
 ndefinition IP2022_fetch_byte_or_word ≝
 λm:mcu_type.λfR:word32 → option byte8.λpc:word16.
- let map_pc ≝ rol_w32 〈〈〈x0,x1〉:〈x0,x0〉〉.pc〉 in
- match fR map_pc with
+ match fR (rol_w32 〈〈〈x0,x1〉:〈x0,x0〉〉.pc〉) with
   [ None ⇒ FetchERR ? ILL_FETCH_AD
   | Some bh ⇒ match eq_b8 bh 〈x0,x0〉 with
-   [ true ⇒ match fR (succ_w32 map_pc) with
+   [ true ⇒ match fR (rol_w32 〈〈〈x8,x1〉:〈x0,x0〉〉.pc〉) with
     [ None ⇒ FetchERR ? ILL_FETCH_AD
-    | Some bl ⇒ fetch_word_aux m (succ_w16 pc) 〈bh:bl〉
+    | Some bl ⇒ fetch_word_aux m pc (succ_w16 pc) 〈bh:bl〉
     ]
-   | false ⇒ fetch_byte_aux m (succ_w16 pc) bh
+   | false ⇒ fetch_byte_aux m pc (succ_w16 pc) bh
    ]
   ].
 
diff --git a/helm/software/matita/contribs/ng_assembly/emulator/read_write/load_write.ma b/helm/software/matita/contribs/ng_assembly/emulator/read_write/load_write.ma
index 683a0f7af..73db58f81 100755
--- a/helm/software/matita/contribs/ng_assembly/emulator/read_write/load_write.ma
+++ b/helm/software/matita/contribs/ng_assembly/emulator/read_write/load_write.ma
@@ -29,7 +29,7 @@ include "emulator/read_write/IP2022_load_write.ma".
 
 ndefinition multi_mode_loadb ≝
 λm.match m
-    return λm.Πt.any_status m t → word16 → aux_im_type m →
+    return λm.Πt.any_status m t → word16 → word16 → aux_im_type m →
               option (Prod3T (any_status m t) byte8 word16)
    with
     [ HC05 ⇒ Freescale_multi_mode_load_auxb HC05
@@ -41,7 +41,7 @@ ndefinition multi_mode_loadb ≝
 
 ndefinition multi_mode_loadw ≝
 λm.match m
-    return λm.Πt.any_status m t → word16 → aux_im_type m →
+    return λm.Πt.any_status m t → word16 → word16 → aux_im_type m →
                  option (Prod3T (any_status m t) word16 word16)
    with
     [ HC05 ⇒ Freescale_multi_mode_load_auxw HC05
@@ -59,7 +59,7 @@ ndefinition multi_mode_loadw ≝
 
 ndefinition multi_mode_writeb ≝
 λm.match m
-    return λm.Πt.any_status m t → word16 → aux_im_type m → byte8 →
+    return λm.Πt.any_status m t → word16 → word16 → aux_mod_type → aux_im_type m → byte8 →
               option (ProdT (any_status m t) word16)
    with
     [ HC05 ⇒ Freescale_multi_mode_write_auxb HC05
@@ -71,7 +71,7 @@ ndefinition multi_mode_writeb ≝
 
 ndefinition multi_mode_writew ≝
 λm.match m
-    return λm.Πt.any_status m t → word16 → aux_im_type m → word16 →
+    return λm.Πt.any_status m t → word16 → word16 → aux_im_type m → word16 →
               option (ProdT (any_status m t) word16)
    with
     [ HC05 ⇒ Freescale_multi_mode_write_auxw HC05
diff --git a/helm/software/matita/contribs/ng_assembly/emulator/read_write/load_write_base.ma b/helm/software/matita/contribs/ng_assembly/emulator/read_write/load_write_base.ma
old mode 100755
new mode 100644
index d3bd4f96d..8ee6e9446
--- a/helm/software/matita/contribs/ng_assembly/emulator/read_write/load_write_base.ma
+++ b/helm/software/matita/contribs/ng_assembly/emulator/read_write/load_write_base.ma
@@ -22,10 +22,6 @@
 
 include "emulator/read_write/read_write.ma".
 
-(* ************************ *)
-(* MODALITA' INDIRIZZAMENTO *)
-(* ************************ *)
-
 (* mattoni base *)
 (* - incrementano l'indirizzo normalmente *)
 (* - incrementano PC attraverso il filtro *)
diff --git a/helm/software/matita/contribs/ng_assembly/emulator/read_write/read_write.ma b/helm/software/matita/contribs/ng_assembly/emulator/read_write/read_write.ma
index 56c26a943..8f5e41b25 100755
--- a/helm/software/matita/contribs/ng_assembly/emulator/read_write/read_write.ma
+++ b/helm/software/matita/contribs/ng_assembly/emulator/read_write/read_write.ma
@@ -57,13 +57,13 @@ ndefinition memory_filter_write ≝
  return λm:mcu_type.any_status m t → word32 → aux_mod_type → byte8 → option (any_status m t) with
  [ HC05 ⇒ λs:any_status HC05 t.λaddr:word32.λflag:aux_mod_type.λval:byte8.
   opt_map … (mem_update t (mem_desc ? t s) (chk_desc ? t s) addr val)
-   (λmem.Some ? (set_mem_desc ? t s mem)) 
+   (λmem.Some ? (set_mem_desc ? t s mem))
  | HC08 ⇒ λs:any_status HC08 t.λaddr:word32.λflag:aux_mod_type.λval:byte8.
   opt_map … (mem_update t (mem_desc ? t s) (chk_desc ? t s) addr val)
    (λmem.Some ? (set_mem_desc ? t s mem))
  | HCS08 ⇒ λs:any_status HCS08 t.λaddr:word32.λflag:aux_mod_type.λval:byte8.
   opt_map … (mem_update t (mem_desc ? t s) (chk_desc ? t s) addr val)
-   (λmem.Some ? (set_mem_desc ? t s mem)) 
+   (λmem.Some ? (set_mem_desc ? t s mem))
  | RS08 ⇒ λs:any_status RS08 t.λaddr:word32.λflag:aux_mod_type.λval:byte8.
   RS08_memory_filter_write t s addr val
  | IP2022 ⇒ λs:any_status IP2022 t.λaddr:word32.λflag:aux_mod_type.λval:byte8.
@@ -75,10 +75,10 @@ ndefinition memory_filter_write_bit ≝
  return λm:mcu_type.any_status m t → word32 → oct → bool → option (any_status m t) with
  [ HC05 ⇒ λs:any_status HC05 t.λaddr:word32.λsub:oct.λval:bool.
   opt_map … (mem_update_bit t (mem_desc ? t s) (chk_desc ? t s) addr sub val)
-   (λmem.Some ? (set_mem_desc ? t s mem)) 
+    (λmem.Some ? (set_mem_desc ? t s mem))
  | HC08 ⇒ λs:any_status HC08 t.λaddr:word32.λsub:oct.λval:bool.
   opt_map … (mem_update_bit t (mem_desc ? t s) (chk_desc ? t s) addr sub val)
-   (λmem.Some ? (set_mem_desc ? t s mem))
+    (λmem.Some ? (set_mem_desc ? t s mem))
  | HCS08 ⇒ λs:any_status HCS08 t.λaddr:word32.λsub:oct.λval:bool.
   opt_map … (mem_update_bit t (mem_desc ? t s) (chk_desc ? t s) addr sub val)
    (λmem.Some ? (set_mem_desc ? t s mem)) 
diff --git a/helm/software/matita/contribs/ng_assembly/emulator/status/IP2022_status.ma b/helm/software/matita/contribs/ng_assembly/emulator/status/IP2022_status.ma
index 875ee2477..4a4a20eb1 100755
--- a/helm/software/matita/contribs/ng_assembly/emulator/status/IP2022_status.ma
+++ b/helm/software/matita/contribs/ng_assembly/emulator/status/IP2022_status.ma
@@ -215,6 +215,9 @@ ndefinition set_addr_reg_IP2022 ≝
   (c_flag_IP2022 alu)
   (skip_mode_IP2022 alu).
 
+ndefinition get_addr_reg_IP2022 ≝
+λalu.get_addrarray (addrsel_reg_IP2022 alu) (addr_array_IP2022 alu).
+
 (* setter specifico IP2022 di CALL *)
 ndefinition set_call_reg_IP2022 ≝
 λalu.λcall':word16.
@@ -236,6 +239,29 @@ ndefinition set_call_reg_IP2022 ≝
   (c_flag_IP2022 alu)
   (skip_mode_IP2022 alu).
 
+ndefinition get_call_reg_IP2022 ≝
+λalu.getn_array16T x0 ? (call_stack_IP2022 alu).
+
+ndefinition set_call_stack_IP2022 ≝
+λalu.λcall':aux_callstack_type.
+ mk_alu_IP2022
+  (acc_low_reg_IP2022 alu)
+  (mulh_reg_IP2022 alu)
+  (addrsel_reg_IP2022 alu)
+  (addr_array_IP2022 alu)
+  call'
+  (ip_reg_IP2022 alu)
+  (dp_reg_IP2022 alu)
+  (data_reg_IP2022 alu)
+  (sp_reg_IP2022 alu)
+  (pc_reg_IP2022 alu)
+  (speed_reg_IP2022 alu)
+  (page_reg_IP2022 alu)
+  (h_flag_IP2022 alu)
+  (z_flag_IP2022 alu)
+  (c_flag_IP2022 alu)
+  (skip_mode_IP2022 alu).
+
 ndefinition push_call_reg_IP2022 ≝
 λalu.λcall':word16.
  mk_alu_IP2022
@@ -257,27 +283,8 @@ ndefinition push_call_reg_IP2022 ≝
   (skip_mode_IP2022 alu).
 
 ndefinition pop_call_reg_IP2022 ≝
-λalu.
- match pop_callstack (call_stack_IP2022 alu) with
-  [ pair val call' ⇒
- pair … val
-        (mk_alu_IP2022
-         (acc_low_reg_IP2022 alu)
-         (mulh_reg_IP2022 alu)
-         (addrsel_reg_IP2022 alu)
-         (addr_array_IP2022 alu)
-         call'
-         (ip_reg_IP2022 alu)
-         (dp_reg_IP2022 alu)
-         (data_reg_IP2022 alu)
-         (sp_reg_IP2022 alu)
-         (pc_reg_IP2022 alu)
-         (speed_reg_IP2022 alu)
-         (page_reg_IP2022 alu)
-         (h_flag_IP2022 alu)
-         (z_flag_IP2022 alu)
-         (c_flag_IP2022 alu)
-         (skip_mode_IP2022 alu)) ].
+λalu.match pop_callstack (call_stack_IP2022 alu) with
+      [ pair val call' ⇒ pair … val (set_call_stack_IP2022 alu call') ].
 
 (* setter specifico IP2022 di IP *)
 ndefinition set_ip_reg_IP2022 ≝
diff --git a/helm/software/matita/contribs/ng_assembly/emulator/status/status_getter.ma b/helm/software/matita/contribs/ng_assembly/emulator/status/status_getter.ma
index 1f4e5aa5a..b2c2b46a7 100755
--- a/helm/software/matita/contribs/ng_assembly/emulator/status/status_getter.ma
+++ b/helm/software/matita/contribs/ng_assembly/emulator/status/status_getter.ma
@@ -150,7 +150,7 @@ ndefinition get_addr_reg ≝
  | HC08 ⇒ λalu.None ?
  | HCS08 ⇒ λalu.None ?
  | RS08 ⇒ λalu.None ?
- | IP2022 ⇒ λalu.Some ? (get_addrarray (addrsel_reg_IP2022 alu) (addr_array_IP2022 alu)) ]
+ | IP2022 ⇒ λalu.Some ? (get_addr_reg_IP2022 alu) ]
  (alu m t s).
 
 (* getter di CALL, non esiste sempre *)
@@ -162,39 +162,9 @@ ndefinition get_call_reg ≝
  | HC08 ⇒ λalu.None ?
  | HCS08 ⇒ λalu.None ?
  | RS08 ⇒ λalu.None ?
- | IP2022 ⇒ λalu.Some ? (getn_array16T x0 ? (call_stack_IP2022 alu)) ]
+ | IP2022 ⇒ λalu.Some ? (get_call_reg_IP2022 alu) ]
  (alu m t s).
 
-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_callstack (call_stack_IP2022 (alu IP2022 t s)) with
-   [ pair val call' ⇒ Some ? (pair … val
-    (set_alu IP2022 t s
-     (mk_alu_IP2022
-      (acc_low_reg_IP2022 (alu IP2022 t s))
-      (mulh_reg_IP2022 (alu IP2022 t s))
-      (addrsel_reg_IP2022 (alu IP2022 t s))
-      (addr_array_IP2022 (alu IP2022 t s))
-      call'
-      (ip_reg_IP2022 (alu IP2022 t s))
-      (dp_reg_IP2022 (alu IP2022 t s))
-      (data_reg_IP2022 (alu IP2022 t s))
-      (sp_reg_IP2022 (alu IP2022 t s))
-      (pc_reg_IP2022 (alu IP2022 t s))
-      (speed_reg_IP2022 (alu IP2022 t s))
-      (page_reg_IP2022 (alu IP2022 t s))
-      (h_flag_IP2022 (alu IP2022 t s))
-      (z_flag_IP2022 (alu IP2022 t s))
-      (c_flag_IP2022 (alu IP2022 t s))
-      (skip_mode_IP2022 (alu IP2022 t s))))) ]].
-
 (* getter di IP, non esiste sempre *)
 ndefinition get_ip_reg ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.
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 e28410878..3a25c0f38 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
@@ -69,7 +69,7 @@ ndefinition set_clk_desc ≝
 
 (* 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
@@ -77,82 +77,134 @@ ndefinition set_acc_8_low_reg ≝
   | 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').
+  ] (alu m t s) val).
 
 (* REGISTRO X *)
 
+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 ?
-             | IP2022 ⇒ 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 *)
 
+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 ?
-             | IP2022 ⇒ 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 *)
 
+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 ?
-             | IP2022 ⇒ 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 *)
 
+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 ?
-             | IP2022 ⇒ Some ? set_sp_reg_IP2022 ])
- (λ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 *)
@@ -171,351 +223,498 @@ ndefinition set_pc_reg ≝
 
 (* REGISTRO SPC *)
 
+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
-             | IP2022 ⇒ None ? ])
- (λ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: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'))).
+λ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.λmulh':byte8.
- match set_mulh_reg m t s mulh' with
+λ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: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'))).
+λ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.λaddrsel':byte8.
- match set_addrsel_reg m t s addrsel' with
+λ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: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'))).
+λ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.λaddr':word24.
- match set_addr_reg m t s addr' with
+λ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: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'))).
+λ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.λcall':word16.
- match set_call_reg m t s call' with
+λ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: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'))).
+λ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.
+λm:mcu_type.λt.
  match m
-  return λm.Πt.any_status m t → option (ProdT word16 (any_status m t))
+  return λm.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')) ]
+  [ 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: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'))).
+λ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.λip':word16.
- match set_ip_reg m t s ip' with
+λ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: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'))).
+λ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.λdp':word16.
- match set_dp_reg m t s dp' with
+λ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: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'))).
+λ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.λdata':word16.
- match set_data_reg m t s data' with
+λ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: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'))).
+λ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.λspeed':exadecim.
- match set_speed_reg m t s speed' with
+λ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: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'))).
+λ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.λpage':oct.
- match set_page_reg m t s page' with
+λ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 *)
 
+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
-             | IP2022 ⇒ None ? ])
- (λ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 *)
 
+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
-             | IP2022 ⇒ None ? ])
- (λ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 *)
 
-(* setter forte di 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: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'))).
+λ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.λskipmode':bool.
- match set_skip_mode m t s skipmode' with
+λ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 *)
 
+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 ?
-             | IP2022 ⇒ 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 *)
 
+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 ?
-             | IP2022 ⇒ Some ? set_h_flag_IP2022 ])
- (λ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 *)
 
+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 ?
-             | IP2022 ⇒ 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 *)
 
+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 ?
-             | IP2022 ⇒ 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 *)
@@ -548,19 +747,33 @@ ndefinition set_c_flag ≝
 
 (* FLAG IRQ *)
 
+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 ?
-             | IP2022 ⇒ 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' ].
diff --git a/helm/software/matita/contribs/ng_assembly/num/word24.ma b/helm/software/matita/contribs/ng_assembly/num/word24.ma
index 94954244b..c0e0d935c 100755
--- a/helm/software/matita/contribs/ng_assembly/num/word24.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/word24.ma
@@ -104,10 +104,12 @@ ndefinition xor_w24 ≝
 (* operatore Most Significant Bit *)
 ndefinition getMSB_w24 ≝ λw:word24.getMSB_b8 (w24x w).
 ndefinition setMSB_w24 ≝ λw:word24.mk_word24 (setMSB_b8 (w24x w)) (w24h w) (w24l w).
+ndefinition clrMSB_w24 ≝ λw:word24.mk_word24 (clrMSB_b8 (w24x w)) (w24h w) (w24l w).
 
 (* operatore Least Significant Bit *)
 ndefinition getLSB_w24 ≝ λw:word24.getLSB_b8 (w24l w).
 ndefinition setLSB_w24 ≝ λw:word24.mk_word24 (w24x w) (w24h w) (setLSB_b8 (w24l w)).
+ndefinition clrLSB_w24 ≝ λw:word24.mk_word24 (w24x w) (w24h w) (clrLSB_b8 (w24l w)).
 
 (* operatore rotazione destra con carry *)
 ndefinition rcr_w24 ≝
-- 
2.39.2