X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly2%2Femulator%2Fread_write%2FIP2022_read_write.ma;fp=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly2%2Femulator%2Fread_write%2FIP2022_read_write.ma;h=297142866c61129a25afad9c0553f690c2dd4264;hb=67303bc29318bd94a31903a92a2127697c5de84e;hp=0000000000000000000000000000000000000000;hpb=cacd19eb7ce2395301b31ed3932b4cd7c23ca90e;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly2/emulator/read_write/IP2022_read_write.ma b/helm/software/matita/contribs/ng_assembly2/emulator/read_write/IP2022_read_write.ma
new file mode 100755
index 000000000..297142866
--- /dev/null
+++ b/helm/software/matita/contribs/ng_assembly2/emulator/read_write/IP2022_read_write.ma
@@ -0,0 +1,287 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(*                          Progetto FreeScale                            *)
+(*                                                                        *)
+(*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
+(*   Sviluppo: 2008-2010                                                  *)
+(*                                                                        *)
+(* ********************************************************************** *)
+
+include "emulator/read_write/read_write_base.ma".
+include "emulator/status/status_setter.ma".
+
+ndefinition IP2022_ADDRSEL_loc ≝ 〈〈x0,x0〉:〈x0,x2〉〉.
+ndefinition IP2022_ADDRX_loc   ≝ 〈〈x0,x0〉:〈x0,x3〉〉.
+ndefinition IP2022_IPH_loc     ≝ 〈〈x0,x0〉:〈x0,x4〉〉.
+ndefinition IP2022_IPL_loc     ≝ 〈〈x0,x0〉:〈x0,x5〉〉.
+ndefinition IP2022_SPH_loc     ≝ 〈〈x0,x0〉:〈x0,x6〉〉.
+ndefinition IP2022_SPL_loc     ≝ 〈〈x0,x0〉:〈x0,x7〉〉.
+ndefinition IP2022_PCH_loc     ≝ 〈〈x0,x0〉:〈x0,x8〉〉.
+ndefinition IP2022_PCL_loc     ≝ 〈〈x0,x0〉:〈x0,x9〉〉.
+ndefinition IP2022_W_loc       ≝ 〈〈x0,x0〉:〈x0,xA〉〉.
+ndefinition IP2022_STATUS_loc  ≝ 〈〈x0,x0〉:〈x0,xB〉〉.
+ndefinition IP2022_DPH_loc     ≝ 〈〈x0,x0〉:〈x0,xC〉〉.
+ndefinition IP2022_DPL_loc     ≝ 〈〈x0,x0〉:〈x0,xD〉〉.
+ndefinition IP2022_SPEED_loc   ≝ 〈〈x0,x0〉:〈x0,xE〉〉.
+ndefinition IP2022_MULH_loc    ≝ 〈〈x0,x0〉:〈x0,xF〉〉.
+ndefinition IP2022_ADDRH_loc   ≝ 〈〈x0,x0〉:〈x1,x0〉〉.
+ndefinition IP2022_ADDRL_loc   ≝ 〈〈x0,x0〉:〈x1,x1〉〉.
+ndefinition IP2022_DATAH_loc   ≝ 〈〈x0,x0〉:〈x1,x2〉〉.
+ndefinition IP2022_DATAL_loc   ≝ 〈〈x0,x0〉:〈x1,x3〉〉.
+ndefinition IP2022_CALLH_loc   ≝ 〈〈x0,x0〉:〈x1,x4〉〉.
+ndefinition IP2022_CALLL_loc   ≝ 〈〈x0,x0〉:〈x1,x5〉〉.
+
+(* **** *)
+(* READ *)
+(* **** *)
+
+(* NB: non ci sono strane indirezioni, solo registri memory mapped da intercettare *)
+ndefinition IP2022_memory_filter_read_aux ≝
+λt:memory_impl.λs:any_status IP2022 t.λaddr:word16.
+λT:Type.λfREG:byte8 → option T.λfMEM:word16 → option T.
+(* intercettare le locazioni memory mapped *)
+ match eqc ? addr IP2022_ADDRSEL_loc with
+  [ true ⇒ fREG (addrsel_reg_IP2022 (alu … s))
+  | false ⇒
+ match eqc ? addr IP2022_ADDRX_loc with
+  [ true ⇒ fREG (w24x (get_addrarray (addrsel_reg_IP2022 (alu … s))
+                                     (addr_array_IP2022 (alu … s))))
+  | false ⇒
+ match eqc ? addr IP2022_IPH_loc with
+  [ true ⇒ fREG (cnH ? (ip_reg_IP2022 (alu … s)))
+  | false ⇒
+ match eqc ? addr IP2022_IPL_loc with
+  [ true ⇒ fREG (cnL ? (ip_reg_IP2022 (alu … s)))
+  | false ⇒
+ match eqc ? addr IP2022_SPH_loc with
+  [ true ⇒ fREG (cnH ? (sp_reg_IP2022 (alu … s)))
+  | false ⇒
+ match eqc ? addr IP2022_SPL_loc with
+  [ true ⇒ fREG (cnL ? (sp_reg_IP2022 (alu … s)))
+  | false ⇒
+ match eqc ? addr IP2022_PCH_loc with
+  [ true ⇒ fREG (cnH ? (pc_reg_IP2022 (alu … s)))
+  | false ⇒
+ match eqc ? addr IP2022_PCL_loc with
+  [ true ⇒ fREG (cnL ? (pc_reg_IP2022 (alu … s)))
+  | false ⇒
+ match eqc ? addr IP2022_W_loc with
+  [ true ⇒ fREG (acc_low_reg_IP2022 (alu … s))
+  | false ⇒
+ (* PAGE[7:5] Z[2] H[1] C [0] *)
+ match eqc ? addr IP2022_STATUS_loc with
+  [ true ⇒ fREG 〈(rolc ? (ex_of_oct (page_reg_IP2022 (alu … s)))),
+                 (orc ? (orc ? (match z_flag_IP2022 (alu … s) with
+                                 [ true ⇒ x4 | false ⇒ x0 ])
+                               (match h_flag_IP2022 (alu … s) with
+                                 [ true ⇒ x2 | false ⇒ x0 ]))
+                        (match c_flag_IP2022 (alu … s) with
+                          [ true ⇒ x1 | false ⇒ x0 ]))〉
+  | false ⇒
+ match eqc ? addr IP2022_DPH_loc with
+  [ true ⇒ fREG (cnH ? (dp_reg_IP2022 (alu … s)))
+  | false ⇒
+ match eqc ? addr IP2022_DPL_loc with
+  [ true ⇒ fREG (cnL ? (dp_reg_IP2022 (alu … s)))
+  | false ⇒
+ (* SPEED[3:0] *)
+ match eqc ? addr IP2022_SPEED_loc with
+  [ true ⇒ fREG (extu_b8 (speed_reg_IP2022 (alu … s)))
+  | false ⇒
+ match eqc ? addr IP2022_MULH_loc with
+  [ true ⇒ fREG (mulh_reg_IP2022 (alu … s))
+  | false ⇒
+ match eqc ? addr IP2022_ADDRH_loc with
+  [ true ⇒ fREG (w24h (get_addrarray (addrsel_reg_IP2022 (alu … s))
+                                     (addr_array_IP2022 (alu … s))))
+  | false ⇒
+ match eqc ? addr IP2022_ADDRL_loc with
+  [ true ⇒ fREG (w24l (get_addrarray (addrsel_reg_IP2022 (alu … s))
+                                     (addr_array_IP2022 (alu … s))))
+  | false ⇒
+ match eqc ? addr IP2022_DATAH_loc with
+  [ true ⇒ fREG (cnH ? (data_reg_IP2022 (alu … s)))
+  | false ⇒
+ match eqc ? addr IP2022_DATAL_loc with
+  [ true ⇒ fREG (cnL ? (data_reg_IP2022 (alu … s)))
+  | false ⇒
+ match eqc ? addr IP2022_CALLH_loc with
+  [ true ⇒ fREG (cnH ? (getn_array16T x0 ? (call_stack_IP2022 (alu … s))))
+  | false ⇒
+ match eqc ? addr IP2022_CALLL_loc with
+  [ true ⇒ fREG (cnL ? (getn_array16T x0 ? (call_stack_IP2022 (alu … s))))
+(* accesso normale *)
+  | false ⇒ fMEM addr
+  ]]]]]]]]]]]]]]]]]]]].
+
+(* lettura IP2022 di un byte *)
+ndefinition IP2022_memory_filter_read ≝
+λt:memory_impl.λs:any_status IP2022 t.λaddr:word16.
+ IP2022_memory_filter_read_aux t s addr byte8
+  (λb.Some byte8 b)
+  (mem_read t (mem_desc … s) (chk_desc … s) o0).
+
+(* lettura IP2022 di un bit *)
+ndefinition IP2022_memory_filter_read_bit ≝
+λt:memory_impl.λs:any_status IP2022 t.λaddr:word16.λsub:oct.
+ IP2022_memory_filter_read_aux t s addr bool
+  (λb.Some bool (getn_array8T sub bool (bits_of_byte8 b)))
+  (λa.mem_read_bit t (mem_desc … s) (chk_desc … s) o0 a sub).
+
+(* ***** *)
+(* WRITE *)
+(* ***** *)
+
+ndefinition high_write_aux_w16 ≝
+λf:byte8 → byte8.λw:word16.〈(f (cnH ? w)):(cnL ? w)〉.
+
+ndefinition lowc_write_aux_w16 ≝
+λf:byte8 → byte8.λw:word16.λflag:aux_mod_type.
+ 〈((match flag with
+    [ auxMode_ok ⇒ λx.x
+    | auxMode_inc ⇒ succc ?
+    | auxMode_dec ⇒ predc ? ]) (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)〉.
+
+ndefinition high_write_aux_w24 ≝
+λf:byte8 → byte8.λw:word24.〈(w24x w);(f (w24h w));(w24l w)〉.
+
+ndefinition low_write_aux_w24 ≝
+λf:byte8 → byte8.λw:word24.λflag:aux_mod_type.
+ match (match flag with
+         [ auxMode_ok ⇒ λx.x
+         | auxMode_inc ⇒ succc ?
+         | auxMode_dec ⇒ predc ? ]) 〈(w24x w):(w24h w)〉 with
+  [ 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:word16.λflag:aux_mod_type.
+λfREG:byte8 → byte8.λfMEM:word16 → option (aux_mem_type t).
+(* intercettare le locazioni memory mapped *)
+ match eqc ? addr IP2022_ADDRSEL_loc with
+  [ true ⇒ set_addrsel_reg … s (fREG (addrsel_reg_IP2022 (alu … s)))
+  | false ⇒ 
+ match eqc ? 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))))
+  | false ⇒
+ match eqc ? addr IP2022_IPH_loc with
+  [ true ⇒ set_ip_reg … s (high_write_aux_w16 fREG (ip_reg_IP2022 (alu … s)))
+  | false ⇒
+ match eqc ? addr IP2022_IPL_loc with
+  [ true ⇒ set_ip_reg … s (lowc_write_aux_w16 fREG (ip_reg_IP2022 (alu … s)) flag)
+  | false ⇒
+ match eqc ? addr IP2022_SPH_loc with
+  [ true ⇒ set_sp_reg … s (high_write_aux_w16 fREG (sp_reg_IP2022 (alu … s)))
+  | false ⇒
+ match eqc ? addr IP2022_SPL_loc with
+  [ true ⇒ set_sp_reg … s (lowc_write_aux_w16 fREG (sp_reg_IP2022 (alu … s)) flag)
+  | false ⇒
+ match eqc ? addr IP2022_PCL_loc with
+  [ true ⇒ Some ? (set_pc_reg … s (lowc_write_aux_w16 fREG (pc_reg_IP2022 (alu … s)) flag))
+  | false ⇒
+ match eqc ? addr IP2022_W_loc with
+  [ true ⇒ Some ? (set_acc_8_low_reg … s (fREG (acc_low_reg_IP2022 (alu … s))))
+  | false ⇒
+ match eqc ? addr IP2022_DPH_loc with
+  [ true ⇒ set_dp_reg … s (high_write_aux_w16 fREG (dp_reg_IP2022 (alu … s)))
+  | false ⇒
+ match eqc ? addr IP2022_DPL_loc with
+  [ true ⇒ set_dp_reg … s (lowc_write_aux_w16 fREG (dp_reg_IP2022 (alu … s)) flag)
+  | false ⇒
+ match eqc ? addr IP2022_MULH_loc with
+  [ true ⇒ set_mulh_reg … s (fREG (mulh_reg_IP2022 (alu … s)))
+  | false ⇒
+ match eqc ? addr IP2022_ADDRH_loc with
+  [ true ⇒ set_addr_reg … s (high_write_aux_w24 fREG (get_addrarray (addrsel_reg_IP2022 (alu … s))
+                                                                    (addr_array_IP2022 (alu … s))))
+  | false ⇒
+ match eqc ? addr IP2022_ADDRL_loc with
+  [ true ⇒ set_addr_reg … s (low_write_aux_w24 fREG (get_addrarray (addrsel_reg_IP2022 (alu … s))
+                                                                   (addr_array_IP2022 (alu … s))) flag)
+  | false ⇒
+ match eqc ? 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 eqc ? addr IP2022_DATAL_loc with
+  [ true ⇒ set_data_reg … s (lownc_write_aux_w16 fREG (data_reg_IP2022 (alu … s)))
+  | false ⇒
+ match eqc ? 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 eqc ? addr IP2022_CALLL_loc with
+  [ true ⇒ set_call_reg … s (lownc_write_aux_w16 fREG (getn_array16T x0 ? (call_stack_IP2022 (alu … s))))
+(* accesso normale *)
+  | false ⇒ opt_map … (fMEM addr)
+             (λmem'.Some ? (set_mem_desc … s mem'))
+  ]]]]]]]]]]]]]]]]].
+
+(* scrittura IP2022 di un byte *)
+ndefinition IP2022_memory_filter_write ≝
+λt:memory_impl.λs:any_status IP2022 t.
+λaddr:word16.λflag:aux_mod_type.λval:byte8.
+ (* PAGE[7:5] Z[2] H[1] C [0] *)
+ match eqc ? 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))))
+ (* accesso a registro_non_spezzato/normale *)
+  | false ⇒ IP2022_memory_filter_write_aux t s addr flag
+             (λb.val)
+             (λa.mem_update t (mem_desc … s) (chk_desc … s) o0 a val) ].
+
+(* scrittura IP2022 di un bit *)
+ndefinition IP2022_memory_filter_write_bit ≝
+λt:memory_impl.λs:any_status IP2022 t.
+λaddr:word16.λsub:oct.λval:bool.
+ (* PAGE[7:5] Z[2] H[1] C [0] *)
+ match eqc ? addr IP2022_STATUS_loc with
+  [ true ⇒ Some ? (set_alu … s
+   (match sub with
+     [ o0 ⇒ set_page_reg_IP2022 (alu … s)
+                                ((match val with [ true ⇒ or_oct o4 | false ⇒ and_oct o3 ])
+                                  (page_reg_IP2022 (alu … s)))
+     | o1 ⇒ set_page_reg_IP2022 (alu … s)
+                                ((match val with [ true ⇒ or_oct o2 | false ⇒ and_oct o5 ])
+                                  (page_reg_IP2022 (alu … s)))
+     | o2 ⇒ set_page_reg_IP2022 (alu … s) 
+                                ((match val with [ true ⇒ or_oct o1 | false ⇒ and_oct o6 ])
+                                  (page_reg_IP2022 (alu … s)))
+     | o5 ⇒ set_z_flag_IP2022 (alu … s) val
+     | o6 ⇒ set_h_flag_IP2022 (alu … s) val
+     | o7 ⇒ set_c_flag_IP2022 (alu … s) val
+     | _ ⇒ alu … s ]))
+ (* accesso a registro_non_spezzato/normale *)
+  | false ⇒ IP2022_memory_filter_write_aux t s addr auxMode_ok
+             (λb.byte8_of_bits (setn_array8T sub bool (bits_of_byte8 b) val))
+             (λa.mem_update_bit t (mem_desc … s) (chk_desc … s) o0 a sub val) ].