freescale porting

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

diff --git a/helm/software/matita/contribs/ng_assembly/emulator/status/RS08_status.ma b/helm/software/matita/contribs/ng_assembly/emulator/status/RS08_status.ma
index a02971f4c6a0a1376e5c3faa2c9020e7fe358e28..2b84717f832523f834e5d04b54d730650ef3cfc9 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/emulator/status/RS08_status.ma
+++ b/helm/software/matita/contribs/ng_assembly/emulator/status/RS08_status.ma
@@ -68,6 +68,101 @@ notation "{hvbox('A_Reg' ≝ acclow ; break 'Pc_Reg' ≝ pc ; break 'Pc_Mask' 
 interpretation "mk_alu_RS08" 'mk_alu_RS08 acclow pc pcm spc xm psm zfl cfl =
  (mk_alu_RS08 acclow pc pcm spc xm psm zfl cfl).
 
+(* ****** *)
+(* SETTER *)
+(* ****** *)
+
+(* 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 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 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 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).
+
+(* 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 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 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'.
+
 (* ***************** *)
 (* CONFRONTO FRA ALU *)
 (* ***************** *)