freescale porting

[helm.git] / helm / software / matita / contribs / ng_assembly / emulator / status / IP2022_status.ma

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 ad920e71f7b6857d3bf03199c9596afbcca74098..875ee24773e93df30d687139ab296a87f736d639 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/emulator/status/IP2022_status.ma
+++ b/helm/software/matita/contribs/ng_assembly/emulator/status/IP2022_status.ma
@@ -42,11 +42,11 @@ ndefinition new_callstack ≝
 
 ndefinition pop_callstack ≝
 λcs:aux_callstack_type.
- pair ?? (a16_1 ? cs)
-         (mk_Array16T ? (a16_2 ? cs)  (a16_3 ? cs)  (a16_4 ? cs)  (a16_5 ? cs)
-                        (a16_6 ? cs)  (a16_7 ? cs)  (a16_8 ? cs)  (a16_9 ? cs)
-                        (a16_10 ? cs) (a16_11 ? cs) (a16_12 ? cs) (a16_13 ? cs)
-                        (a16_14 ? cs) (a16_15 ? cs) (a16_16 ? cs) 〈〈xF,xF〉:〈xF,xF〉〉).
+ pair … (a16_1 ? cs)
+        (mk_Array16T ? (a16_2 ? cs)  (a16_3 ? cs)  (a16_4 ? cs)  (a16_5 ? cs)
+                       (a16_6 ? cs)  (a16_7 ? cs)  (a16_8 ? cs)  (a16_9 ? cs)
+                       (a16_10 ? cs) (a16_11 ? cs) (a16_12 ? cs) (a16_13 ? cs)
+                       (a16_14 ? cs) (a16_15 ? cs) (a16_16 ? cs) 〈〈xF,xF〉:〈xF,xF〉〉).
 
 ndefinition push_callstack ≝
 λcs:aux_callstack_type.λtop.
@@ -66,19 +66,13 @@ ndefinition new_addrarray ≝
               (〈〈x0,x0〉;〈x0,x0〉;〈x0,x0〉〉) (〈〈x0,x0〉;〈x0,x0〉;〈x0,x0〉〉)
               (〈〈x0,x0〉;〈x0,x0〉;〈x0,x0〉〉) (〈〈x0,x0〉;〈x0,x0〉;〈x0,x0〉〉).
 
-ndefinition get_low3bits ≝
-λaddrsel:byte8.
- match cnL ? addrsel with
-  [ x0 ⇒ o0 | x1 ⇒ o1 | x2 ⇒ o2 | x3 ⇒ o3 | x4 ⇒ o4 | x5 ⇒ o5 | x6 ⇒ o6 | x7 ⇒ o7
-  | x8 ⇒ o0 | x9 ⇒ o1 | xA ⇒ o2 | xB ⇒ o3 | xC ⇒ o4 | xD ⇒ o5 | xE ⇒ o6 | xF ⇒ o7 ].
-
 ndefinition get_addrarray ≝
 λaddrsel:byte8.λaa:aux_addrarray_type.
- getn_array8T (get_low3bits addrsel) ? aa.
+ getn_array8T (oct_of_exL (cnL ? addrsel)) ? aa.
 
 ndefinition set_addrarray ≝
 λaddrsel:byte8.λaa:aux_addrarray_type.λv.
- setn_array8T (get_low3bits addrsel) ? aa v.
+ setn_array8T (oct_of_exL (cnL ? addrsel)) ? aa v.
 
 (* *********************************** *)
 (* STATUS INTERNO DEL PROCESSORE (ALU) *)
@@ -262,6 +256,29 @@ ndefinition push_call_reg_IP2022 ≝
   (c_flag_IP2022 alu)
   (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)) ].
+
 (* setter specifico IP2022 di IP *)
 ndefinition set_ip_reg_IP2022 ≝
 λalu.λip':word16.