matitaB/matita/contribs/ng_assembly2/emulator/status/HC05_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'HC05 *)
  30 nrecord alu_HC05: Type ≝
  31  {
  32  (* A: registo accumulatore *)
  33  acc_low_reg_HC05 : byte8;
  34  (* X: registro indice *)
  35  indX_low_reg_HC05 : byte8;
  36  (* SP: registo stack pointer *)
  37  sp_reg_HC05 : word16;
  38  (* modificatori di SP: per esempio e' definito come 0000000011xxxxxxb *)
  39  (* la logica della sua costruzione e' quindi (SP∧mask)∨fix *)
  40  (* totalmente racchiusa nella ALU, bastera' fare get(set(SP)) *)
  41  sp_mask_HC05 : word16;
  42  sp_fix_HC05 : word16;
  43  (* PC: registro program counter *)
  44  pc_reg_HC05 : word16;
  45  (* modificatore di PC: per esempio e' definito come 00xxxxxxxxxxxxxxb *)
  46  (* la logica della sua costruzione e' quindi (PC∧mask) *)
  47  (* totalmente racchiusa nella ALU, bastera' fare get(set(PC)) *)
  48  pc_mask_HC05 : word16;
  49
  50  (* H: flag semi-carry (somma nibble basso) *)
  51  h_flag_HC05 : bool;
  52  (* I: flag mascheramento degli interrupt mascherabili: 1=mascherati *)
  53  i_flag_HC05 : bool;
  54  (* N: flag segno/negativita' *)
  55  n_flag_HC05 : bool;
  56  (* Z: flag zero *)
  57  z_flag_HC05 : bool;
  58  (* C: flag carry *)
  59  c_flag_HC05 : bool;
  60
  61  (* IRQ: flag che simula il pin esterno IRQ *)
  62  irq_flag_HC05 : bool
  63  }.
  64
  65 notation "{hvbox('A_Reg' ≝ acclow ; break 'X_Reg' ≝ indxlow ; break 'Sp_Reg' ≝ sp ; break 'Sp_Mask' ≝ spm ; break 'Sp_Fix' ≝ spf ; break 'Pc_Reg' ≝ pc ; break 'Pc_Mask' ≝ pcm ; break 'H_Flag' ≝ hfl ; break 'I_Flag' ≝ ifl ; break 'N_Flag' ≝ nfl ; break 'Z_Flag' ≝ zfl ; break 'C_Flag' ≝ cfl ; break 'IRQ_Flag' ≝ irqfl)}"
  66  non associative with precedence 80 for
  67  @{ 'mk_alu_HC05 $acclow $indxlow $sp $spm $spf $pc $pcm $hfl $ifl $nfl $zfl $cfl $irqfl }.
  68 interpretation "mk_alu_HC05" 'mk_alu_HC05 acclow indxlow sp spm spf pc pcm hfl ifl nfl zfl cfl irqfl =
  69  (mk_alu_HC05 acclow indxlow sp spm spf pc pcm hfl ifl nfl zfl cfl irqfl).
  70
  71 (* ****** *)
  72 (* SETTER *)
  73 (* ****** *)
  74
  75 (* setter specifico HC05 di A *)
  76 ndefinition set_acc_8_low_reg_HC05 ≝
  77 λalu.λacclow':byte8.
  78  mk_alu_HC05
  79   acclow'
  80   (indX_low_reg_HC05 alu)
  81   (sp_reg_HC05 alu)
  82   (sp_mask_HC05 alu)
  83   (sp_fix_HC05 alu)
  84   (pc_reg_HC05 alu)
  85   (pc_mask_HC05 alu)
  86   (h_flag_HC05 alu)
  87   (i_flag_HC05 alu)
  88   (n_flag_HC05 alu)
  89   (z_flag_HC05 alu)
  90   (c_flag_HC05 alu)
  91   (irq_flag_HC05 alu).
  92
  93 (* setter specifico HC05 di X *)
  94 ndefinition set_indX_8_low_reg_HC05 ≝
  95 λalu.λindxlow':byte8.
  96  mk_alu_HC05
  97   (acc_low_reg_HC05 alu)
  98   indxlow'
  99   (sp_reg_HC05 alu)
 100   (sp_mask_HC05 alu)
 101   (sp_fix_HC05 alu)
 102   (pc_reg_HC05 alu)
 103   (pc_mask_HC05 alu)
 104   (h_flag_HC05 alu)
 105   (i_flag_HC05 alu)
 106   (n_flag_HC05 alu)
 107   (z_flag_HC05 alu)
 108   (c_flag_HC05 alu)
 109   (irq_flag_HC05 alu).
 110
 111 (* setter specifico HC05 di SP, effettua (SP∧mask)∨fix *)
 112 ndefinition set_sp_reg_HC05 ≝
 113 λalu.λsp':word16.
 114  mk_alu_HC05
 115   (acc_low_reg_HC05 alu)
 116   (indX_low_reg_HC05 alu)
 117   (orc ? (andc ? sp' (sp_mask_HC05 alu)) (sp_fix_HC05 alu))
 118   (sp_mask_HC05 alu)
 119   (sp_fix_HC05 alu)
 120   (pc_reg_HC05 alu)
 121   (pc_mask_HC05 alu)
 122   (h_flag_HC05 alu)
 123   (i_flag_HC05 alu)
 124   (n_flag_HC05 alu)
 125   (z_flag_HC05 alu)
 126   (c_flag_HC05 alu)
 127   (irq_flag_HC05 alu).
 128
 129 (* setter specifico HC05 di PC, effettua PC∧mask *)
 130 ndefinition set_pc_reg_HC05 ≝
 131 λalu.λpc':word16.
 132  mk_alu_HC05
 133   (acc_low_reg_HC05 alu)
 134   (indX_low_reg_HC05 alu)
 135   (sp_reg_HC05 alu)
 136   (sp_mask_HC05 alu)
 137   (sp_fix_HC05 alu)
 138   (andc ? pc' (pc_mask_HC05 alu))
 139   (pc_mask_HC05 alu)
 140   (h_flag_HC05 alu)
 141   (i_flag_HC05 alu)
 142   (n_flag_HC05 alu)
 143   (z_flag_HC05 alu)
 144   (c_flag_HC05 alu)
 145   (irq_flag_HC05 alu).
 146
 147 (* setter specifico HC05 di H *)
 148 ndefinition set_h_flag_HC05 ≝
 149 λalu.λhfl':bool.
 150  mk_alu_HC05
 151   (acc_low_reg_HC05 alu)
 152   (indX_low_reg_HC05 alu)
 153   (sp_reg_HC05 alu)
 154   (sp_mask_HC05 alu)
 155   (sp_fix_HC05 alu)
 156   (pc_reg_HC05 alu)
 157   (pc_mask_HC05 alu)
 158   hfl'
 159   (i_flag_HC05 alu)
 160   (n_flag_HC05 alu)
 161   (z_flag_HC05 alu)
 162   (c_flag_HC05 alu)
 163   (irq_flag_HC05 alu).
 164
 165 (* setter specifico HC05 di I *)
 166 ndefinition set_i_flag_HC05 ≝
 167 λalu.λifl':bool.
 168  mk_alu_HC05
 169   (acc_low_reg_HC05 alu)
 170   (indX_low_reg_HC05 alu)
 171   (sp_reg_HC05 alu)
 172   (sp_mask_HC05 alu)
 173   (sp_fix_HC05 alu)
 174   (pc_reg_HC05 alu)
 175   (pc_mask_HC05 alu)
 176   (h_flag_HC05 alu)
 177   ifl'
 178   (n_flag_HC05 alu)
 179   (z_flag_HC05 alu)
 180   (c_flag_HC05 alu)
 181   (irq_flag_HC05 alu).
 182
 183 (* setter specifico HC05 di N *)
 184 ndefinition set_n_flag_HC05 ≝
 185 λalu.λnfl':bool.
 186  mk_alu_HC05
 187   (acc_low_reg_HC05 alu)
 188   (indX_low_reg_HC05 alu)
 189   (sp_reg_HC05 alu)
 190   (sp_mask_HC05 alu)
 191   (sp_fix_HC05 alu)
 192   (pc_reg_HC05 alu)
 193   (pc_mask_HC05 alu)
 194   (h_flag_HC05 alu)
 195   (i_flag_HC05 alu)
 196   nfl'
 197   (z_flag_HC05 alu)
 198   (c_flag_HC05 alu)
 199   (irq_flag_HC05 alu).
 200
 201 (* setter specifico HC05 di Z *)
 202 ndefinition set_z_flag_HC05 ≝
 203 λalu.λzfl':bool.
 204  mk_alu_HC05
 205   (acc_low_reg_HC05 alu)
 206   (indX_low_reg_HC05 alu)
 207   (sp_reg_HC05 alu)
 208   (sp_mask_HC05 alu)
 209   (sp_fix_HC05 alu)
 210   (pc_reg_HC05 alu)
 211   (pc_mask_HC05 alu)
 212   (h_flag_HC05 alu)
 213   (i_flag_HC05 alu)
 214   (n_flag_HC05 alu)
 215   zfl'
 216   (c_flag_HC05 alu)
 217   (irq_flag_HC05 alu).
 218
 219 (* setter specifico HC05 di C *)
 220 ndefinition set_c_flag_HC05 ≝
 221 λalu.λcfl':bool.
 222  mk_alu_HC05
 223   (acc_low_reg_HC05 alu)
 224   (indX_low_reg_HC05 alu)
 225   (sp_reg_HC05 alu)
 226   (sp_mask_HC05 alu)
 227   (sp_fix_HC05 alu)
 228   (pc_reg_HC05 alu)
 229   (pc_mask_HC05 alu)
 230   (h_flag_HC05 alu)
 231   (i_flag_HC05 alu)
 232   (n_flag_HC05 alu)
 233   (z_flag_HC05 alu)
 234   cfl'
 235   (irq_flag_HC05 alu).
 236
 237 (* setter specifico HC05 di IRQ *)
 238 ndefinition set_irq_flag_HC05 ≝
 239 λalu.λirqfl':bool.
 240  mk_alu_HC05
 241   (acc_low_reg_HC05 alu)
 242   (indX_low_reg_HC05 alu)
 243   (sp_reg_HC05 alu)
 244   (sp_mask_HC05 alu)
 245   (sp_fix_HC05 alu)
 246   (pc_reg_HC05 alu)
 247   (pc_mask_HC05 alu)
 248   (h_flag_HC05 alu)
 249   (i_flag_HC05 alu)
 250   (n_flag_HC05 alu)
 251   (z_flag_HC05 alu)
 252   (c_flag_HC05 alu)
 253   irqfl'.
 254
 255 (* ***************** *)
 256 (* CONFRONTO FRA ALU *)
 257 (* ***************** *)
 258
 259 (* confronto registro per registro dell'HC05 *)
 260 ndefinition eq_HC05_alu ≝
 261 λalu1,alu2:alu_HC05.
 262  (eqc ? (acc_low_reg_HC05 alu1) (acc_low_reg_HC05 alu2)) ⊗
 263  (eqc ? (indX_low_reg_HC05 alu1) (indX_low_reg_HC05 alu2)) ⊗
 264  (eqc ? (sp_reg_HC05 alu1) (sp_reg_HC05 alu2)) ⊗
 265  (eqc ? (sp_mask_HC05 alu1) (sp_mask_HC05 alu2)) ⊗
 266  (eqc ? (sp_fix_HC05 alu1) (sp_fix_HC05 alu2)) ⊗
 267  (eqc ? (pc_reg_HC05 alu1) (pc_reg_HC05 alu2)) ⊗
 268  (eqc ? (pc_mask_HC05 alu1) (pc_mask_HC05 alu2)) ⊗
 269  (eqc ? (h_flag_HC05 alu1) (h_flag_HC05 alu2)) ⊗
 270  (eqc ? (i_flag_HC05 alu1) (i_flag_HC05 alu2)) ⊗
 271  (eqc ? (n_flag_HC05 alu1) (n_flag_HC05 alu2)) ⊗
 272  (eqc ? (z_flag_HC05 alu1) (z_flag_HC05 alu2)) ⊗
 273  (eqc ? (c_flag_HC05 alu1) (c_flag_HC05 alu2)) ⊗
 274  (eqc ? (irq_flag_HC05 alu1) (irq_flag_HC05 alu2)).
 275
 276 ndefinition forall_HC05_alu ≝ λP:alu_HC05 → bool.
 277  forallc ? (λr1.forallc ? (λr2.
 278  forallc ? (λr3.forallc ? (λr4.
 279  forallc ? (λr5.forallc ? (λr6.
 280  forallc ? (λr7.forallc ? (λr8.
 281  forallc ? (λr9.forallc ? (λr10.
 282  forallc ? (λr11.forallc ? (λr12.
 283  forallc ? (λr13.P (mk_alu_HC05 r1 r2 r3 r4 r5 r6 r7 r8 r9 r10 r11 r12 r13)))))))))))))).