matita/matita/contribs/ng_assembly2/emulator/status/RS08_status_base.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  x_map_RS08 : byte8;
  48  (* PS: registro selezione di pagina *)
  49  (* serve a indirizzare la finestra RAM di 64b [0x00C0-0x00FF] *)
  50  (* su tutta la memoria installata [0x0000-0x3FFF]: [00pp pppp ppxx xxxx] *)
  51  (* NB: in realta' e' mappato in memoria e non risiede nella ALU *)
  52  (* la lettura/scrittura avviene tramite la locazione [0x001F] *)
  53  ps_map_RS08 : byte8;
  54
  55  (* Z: flag zero *)
  56  z_flag_RS08 : bool;
  57  (* C: flag carry *)
  58  c_flag_RS08 : bool
  59  }.
  60
  61 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)}"
  62  non associative with precedence 80 for
  63  @{ 'mk_alu_RS08 $acclow $pc $pcm $spc $xm $psm $zfl $cfl }.
  64 interpretation "mk_alu_RS08" 'mk_alu_RS08 acclow pc pcm spc xm psm zfl cfl =
  65  (mk_alu_RS08 acclow pc pcm spc xm psm zfl cfl).
  66
  67 (* ****** *)
  68 (* SETTER *)
  69 (* ****** *)
  70
  71 (* setter specifico RS08 di A *)
  72 ndefinition set_acc_8_low_reg_RS08 ≝
  73 λalu.λacclow':byte8.
  74  mk_alu_RS08
  75   acclow'
  76   (pc_reg_RS08 alu)
  77   (pc_mask_RS08 alu)
  78   (spc_reg_RS08 alu)
  79   (x_map_RS08 alu)
  80   (ps_map_RS08 alu)
  81   (z_flag_RS08 alu)
  82   (c_flag_RS08 alu).
  83
  84 (* setter specifico RS08 di PC, effettua PC∧mask *)
  85 ndefinition set_pc_reg_RS08 ≝
  86 λalu.λpc':word16.
  87  mk_alu_RS08
  88   (acc_low_reg_RS08 alu)
  89   (andc ? pc' (pc_mask_RS08 alu))
  90   (pc_mask_RS08 alu)
  91   (spc_reg_RS08 alu)
  92   (x_map_RS08 alu)
  93   (ps_map_RS08 alu)
  94   (z_flag_RS08 alu)
  95   (c_flag_RS08 alu).
  96
  97 (* setter specifico RS08 di SPC, effettua SPC∧mask *)
  98 ndefinition set_spc_reg_RS08 ≝
  99 λalu.λspc':word16.
 100  mk_alu_RS08
 101   (acc_low_reg_RS08 alu)
 102   (pc_reg_RS08 alu)
 103   (pc_mask_RS08 alu)
 104   (andc ? spc' (pc_mask_RS08 alu))
 105   (x_map_RS08 alu)
 106   (ps_map_RS08 alu)
 107   (z_flag_RS08 alu)
 108   (c_flag_RS08 alu).
 109
 110 (* setter specifico RS08 di memory mapped X *)
 111 ndefinition set_x_map_RS08 ≝
 112 λalu.λxm':byte8.
 113  mk_alu_RS08
 114   (acc_low_reg_RS08 alu)
 115   (pc_reg_RS08 alu)
 116   (pc_mask_RS08 alu)
 117   (spc_reg_RS08 alu)
 118   xm'
 119   (ps_map_RS08 alu)
 120   (z_flag_RS08 alu)
 121   (c_flag_RS08 alu).
 122
 123 (* setter specifico RS08 di memory mapped PS *)
 124 ndefinition set_ps_map_RS08 ≝
 125 λalu.λpsm':byte8.
 126  mk_alu_RS08
 127   (acc_low_reg_RS08 alu)
 128   (pc_reg_RS08 alu)
 129   (pc_mask_RS08 alu)
 130   (spc_reg_RS08 alu)
 131   (x_map_RS08 alu)
 132   psm'
 133   (z_flag_RS08 alu)
 134   (c_flag_RS08 alu).
 135
 136 (* setter sprcifico RS08 di Z *)
 137 ndefinition set_z_flag_RS08 ≝
 138 λalu.λzfl':bool.
 139  mk_alu_RS08
 140   (acc_low_reg_RS08 alu)
 141   (pc_reg_RS08 alu)
 142   (pc_mask_RS08 alu)
 143   (spc_reg_RS08 alu)
 144   (x_map_RS08 alu)
 145   (ps_map_RS08 alu)
 146   zfl'
 147   (c_flag_RS08 alu).
 148
 149 (* setter specifico RS08 di C *)
 150 ndefinition set_c_flag_RS08 ≝
 151 λalu.λcfl':bool.
 152  mk_alu_RS08
 153   (acc_low_reg_RS08 alu)
 154   (pc_reg_RS08 alu)
 155   (pc_mask_RS08 alu)
 156   (spc_reg_RS08 alu)
 157   (x_map_RS08 alu)
 158   (ps_map_RS08 alu)
 159   (z_flag_RS08 alu)
 160   cfl'.
 161
 162 (* ***************** *)
 163 (* CONFRONTO FRA ALU *)
 164 (* ***************** *)
 165
 166 (* confronto registro per registro dell'RS08 *)
 167 ndefinition eq_RS08_alu ≝
 168 λalu1,alu2:alu_RS08.
 169  (eqc ? (acc_low_reg_RS08 alu1) (acc_low_reg_RS08 alu2)) ⊗
 170  (eqc ? (pc_reg_RS08 alu1) (pc_reg_RS08 alu2)) ⊗
 171  (eqc ? (pc_mask_RS08 alu1) (pc_mask_RS08 alu2)) ⊗
 172  (eqc ? (spc_reg_RS08 alu1) (spc_reg_RS08 alu2)) ⊗
 173  (eqc ? (x_map_RS08 alu1) (x_map_RS08 alu2)) ⊗
 174  (eqc ? (ps_map_RS08 alu1) (ps_map_RS08 alu2)) ⊗
 175  (eqc ? (z_flag_RS08 alu1) (z_flag_RS08 alu2)) ⊗
 176  (eqc ? (c_flag_RS08 alu1) (c_flag_RS08 alu2)).
 177
 178 ndefinition forall_RS08_alu ≝ λP:alu_RS08 → bool.
 179  forallc ? (λr1.forallc ? (λr2.
 180  forallc ? (λr3.forallc ? (λr4.
 181  forallc ? (λr5.forallc ? (λr6.
 182  forallc ? (λr7.forallc ? (λr8.
 183  P (mk_alu_RS08 r1 r2 r3 r4 r5 r6 r7 r8))))))))).