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 (* CONFRONTO FRA ALU *)
  73 (* ***************** *)
  74
  75 (* confronto registro per registro dell'RS08 *)
  76 ndefinition eq_RS08_alu ≝
  77 λalu1,alu2:alu_RS08.
  78  (eq_b8 (acc_low_reg_RS08 alu1) (acc_low_reg_RS08 alu2)) ⊗
  79  (eq_w16 (pc_reg_RS08 alu1) (pc_reg_RS08 alu2)) ⊗
  80  (eq_w16 (pc_mask_RS08 alu1) (pc_mask_RS08 alu2)) ⊗
  81  (eq_w16 (spc_reg_RS08 alu1) (spc_reg_RS08 alu2)) ⊗
  82  (eq_b8 (x_map_RS08 alu1) (x_map_RS08 alu2)) ⊗
  83  (eq_b8 (ps_map_RS08 alu1) (ps_map_RS08 alu2)) ⊗
  84  (eq_bool (z_flag_RS08 alu1) (z_flag_RS08 alu2)) ⊗
  85  (eq_bool (c_flag_RS08 alu1) (c_flag_RS08 alu2)).