X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Femulator%2Fread_write%2FIP2022_load_write.ma;h=f7040de6dcc15fb6f467045b79d5b321bdb5e803;hb=e880d6eab5e1700f4a625ddcd7d0fa8f0cce2dcc;hp=5e9a7d23189f8bf1ce50dabd734486af612200d6;hpb=ced2abc1e3fe84d5bbfa9ccb2ebf46f253279ebe;p=helm.git

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..f7040de6d 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))〉).
+ mem_read_s … s (rol_w32 〈〈〈x8,x1〉:〈x0,x0〉〉.(get_pc_reg … s)〉).
+
+(* 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,16 +41,16 @@ 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 *)
@@ -110,3 +116,156 @@ ndefinition mode_FR1_write ≝
 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).
+
+(* ************************************** *)
+(* 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.λ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)
+                  (λ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 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 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.λ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)
+                      (λ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)
+                       (λ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)
+                       (λ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)
+                       (λ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)
+                       (λ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.λ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 flag writeb)
+                       (λs'.Some ? (pair … s' cur_pc))
+(* FR, W → FR *)
+   | MODE_FR1_and_W ⇒ opt_map … (mode_FR1_write t s 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 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 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.λ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 ?
+   ].