helm/software/matita/contribs/ng_assembly/emulator/status/RS08_status.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* ********************************************************************** *)
  16 (*                          Progetto FreeScale                            *)
  17 (*                                                                        *)
  18 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
  19 (*   Sviluppo: 2008-2010                                                  *)
  20 (*                                                                        *)
  21 (* ********************************************************************** *)
  22
  23 include "num/word16.ma".
  24
  25 (* *********************************** *)
  26 (* STATUS INTERNO DEL PROCESSORE (ALU) *)
  27 (* *********************************** *)
  28
  29 (* ALU dell'RS08 *)
  30 nrecord alu_RS08: Type ≝
  31  {
  32  (* A: registo accumulatore *)
  33  acc_low_reg_RS08 : byte8;
  34  (* PC: registro program counter *)
  35  pc_reg_RS08 : word16;
  36  (* modificatore di PC: per esempio e' definito come 00xxxxxxxxxxxxxxb *)
  37  (* la logica della sua costruzione e' quindi (PC∧mask) *)
  38  (* totalmente racchiusa nella ALU, bastera' fare get(set(PC)) *)
  39  pc_mask_RS08 : word16;
  40  (* SPC: registro shadow program counter *)
  41  (* NB: il suo modificatore e' lo stesso di PC *)
  42  spc_reg_RS08 : word16;
  43
  44  (* X: registro indice parte bassa *)
  45  (* NB: in realta' e' mappato in memoria e non risiede nella ALU *)
  46  (* la lettura/scrittura avviene tramite la locazione [0x000F] *)
  47  (* la funzione memory_filter_read/write si occupera' di intercettare *)
  48  (* e deviare sul registro le letture/scritture (modulo load_write) *)
  49  x_map_RS08 : byte8;
  50  (* PS: registro selezione di pagina *)
  51  (* serve a indirizzare la finestra RAM di 64b [0x00C0-0x00FF] *)
  52  (* su tutta la memoria installata [0x0000-0x3FFF]: [00pp pppp ppxx xxxx] *)
  53  (* NB: in realta' e' mappato in memoria e non risiede nella ALU *)
  54  (* la lettura/scrittura avviene tramite la locazione [0x001F] *)
  55  (* la funzione memory_filter_read/write si occupera' di intercettare *)
  56  (* e deviare sul registro le letture/scritture (modulo load_write) *)
  57  ps_map_RS08 : byte8;
  58
  59  (* Z: flag zero *)
  60  z_flag_RS08 : bool;
  61  (* C: flag carry *)
  62  c_flag_RS08 : bool
  63  }.
  64
  65 notation "{hvbox('A_Reg' ≝ acclow ; break 'Pc_Reg' ≝ pc ; break 'Pc_Mask' ≝ pcm ; break 'Spc_Reg' ≝ spc ; break 'X_Map' ≝ xm ; break 'Ps_Map' ≝ psm ; break 'Z_Flag' ≝ zfl ; break 'C_Flag' ≝ cfl)}"
  66  non associative with precedence 80 for
  67  @{ 'mk_alu_RS08 $acclow $pc $pcm $spc $xm $psm $zfl $cfl }.
  68 interpretation "mk_alu_RS08" 'mk_alu_RS08 acclow pc pcm spc xm psm zfl cfl =
  69  (mk_alu_RS08 acclow pc pcm spc xm psm zfl cfl).
  70
  71 (* ****** *)
  72 (* SETTER *)
  73 (* ****** *)
  74
  75 (* setter specifico RS08 di A *)
  76 ndefinition set_acc_8_low_reg_RS08 ≝
  77 λalu.λacclow':byte8.
  78  mk_alu_RS08
  79   acclow'
  80   (pc_reg_RS08 alu)
  81   (pc_mask_RS08 alu)
  82   (spc_reg_RS08 alu)
  83   (x_map_RS08 alu)
  84   (ps_map_RS08 alu)
  85   (z_flag_RS08 alu)
  86   (c_flag_RS08 alu).
  87
  88 (* setter specifico RS08 di PC, effettua PC∧mask *)
  89 ndefinition set_pc_reg_RS08 ≝
  90 λalu.λpc':word16.
  91  mk_alu_RS08
  92   (acc_low_reg_RS08 alu)
  93   (and_w16 pc' (pc_mask_RS08 alu))
  94   (pc_mask_RS08 alu)
  95   (spc_reg_RS08 alu)
  96   (x_map_RS08 alu)
  97   (ps_map_RS08 alu)
  98   (z_flag_RS08 alu)
  99   (c_flag_RS08 alu).
 100
 101 (* setter specifico RS08 di SPC, effettua SPC∧mask *)
 102 ndefinition set_spc_reg_RS08 ≝
 103 λalu.λspc':word16.
 104  mk_alu_RS08
 105   (acc_low_reg_RS08 alu)
 106   (pc_reg_RS08 alu)
 107   (pc_mask_RS08 alu)
 108   (and_w16 spc' (pc_mask_RS08 alu))
 109   (x_map_RS08 alu)
 110   (ps_map_RS08 alu)
 111   (z_flag_RS08 alu)
 112   (c_flag_RS08 alu).
 113
 114 (* setter specifico RS08 di memory mapped X *)
 115 ndefinition set_x_map_RS08 ≝
 116 λalu.λxm':byte8.
 117  mk_alu_RS08
 118   (acc_low_reg_RS08 alu)
 119   (pc_reg_RS08 alu)
 120   (pc_mask_RS08 alu)
 121   (spc_reg_RS08 alu)
 122   xm'
 123   (ps_map_RS08 alu)
 124   (z_flag_RS08 alu)
 125   (c_flag_RS08 alu).
 126
 127 (* setter specifico RS08 di memory mapped PS *)
 128 ndefinition set_ps_map_RS08 ≝
 129 λalu.λpsm':byte8.
 130  mk_alu_RS08
 131   (acc_low_reg_RS08 alu)
 132   (pc_reg_RS08 alu)
 133   (pc_mask_RS08 alu)
 134   (spc_reg_RS08 alu)
 135   (x_map_RS08 alu)
 136   psm'
 137   (z_flag_RS08 alu)
 138   (c_flag_RS08 alu).
 139
 140 (* setter sprcifico RS08 di Z *)
 141 ndefinition set_z_flag_RS08 ≝
 142 λalu.λzfl':bool.
 143  mk_alu_RS08
 144   (acc_low_reg_RS08 alu)
 145   (pc_reg_RS08 alu)
 146   (pc_mask_RS08 alu)
 147   (spc_reg_RS08 alu)
 148   (x_map_RS08 alu)
 149   (ps_map_RS08 alu)
 150   zfl'
 151   (c_flag_RS08 alu).
 152
 153 (* setter specifico RS08 di C *)
 154 ndefinition set_c_flag_RS08 ≝
 155 λalu.λcfl':bool.
 156  mk_alu_RS08
 157   (acc_low_reg_RS08 alu)
 158   (pc_reg_RS08 alu)
 159   (pc_mask_RS08 alu)
 160   (spc_reg_RS08 alu)
 161   (x_map_RS08 alu)
 162   (ps_map_RS08 alu)
 163   (z_flag_RS08 alu)
 164   cfl'.
 165
 166 (* ***************** *)
 167 (* CONFRONTO FRA ALU *)
 168 (* ***************** *)
 169
 170 (* confronto registro per registro dell'RS08 *)
 171 ndefinition eq_RS08_alu ≝
 172 λalu1,alu2:alu_RS08.
 173  (eq_b8 (acc_low_reg_RS08 alu1) (acc_low_reg_RS08 alu2)) ⊗
 174  (eq_w16 (pc_reg_RS08 alu1) (pc_reg_RS08 alu2)) ⊗
 175  (eq_w16 (pc_mask_RS08 alu1) (pc_mask_RS08 alu2)) ⊗
 176  (eq_w16 (spc_reg_RS08 alu1) (spc_reg_RS08 alu2)) ⊗
 177  (eq_b8 (x_map_RS08 alu1) (x_map_RS08 alu2)) ⊗
 178  (eq_b8 (ps_map_RS08 alu1) (ps_map_RS08 alu2)) ⊗
 179  (eq_bool (z_flag_RS08 alu1) (z_flag_RS08 alu2)) ⊗
 180  (eq_bool (c_flag_RS08 alu1) (c_flag_RS08 alu2)).