helm/software/matita/contribs/ng_assembly/emulator/status/HC08_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'HC08/HCS08 *)
  30 nrecord alu_HC08: Type ≝
  31  {
  32  (* A: registo accumulatore *)
  33  acc_low_reg_HC08 : byte8;
  34  (* X: registro indice parte bassa *)
  35  indX_low_reg_HC08 : byte8;
  36  (* H: registro indice parte alta *)
  37  indX_high_reg_HC08 : byte8;
  38  (* SP: registo stack pointer *)
  39  sp_reg_HC08 : word16;
  40  (* PC: registro program counter *)
  41  pc_reg_HC08 : word16;
  42
  43  (* V: flag overflow *)
  44  v_flag_HC08 : bool;
  45  (* H: flag semi-carry (somma nibble basso) *)
  46  h_flag_HC08 : bool;
  47  (* I: flag mascheramento degli interrupt mascherabili: 1=mascherati *)
  48  i_flag_HC08 : bool;
  49  (* N: flag segno/negativita' *)
  50  n_flag_HC08 : bool;
  51  (* Z: flag zero *)
  52  z_flag_HC08 : bool;
  53  (* C: flag carry *)
  54  c_flag_HC08 : bool;
  55
  56  (* IRQ: flag che simula il pin esterno IRQ *)
  57  irq_flag_HC08 : bool
  58  }.
  59
  60 notation "{hvbox('A_Reg' ≝ acclow ; break 'X_Reg' ≝ indxlow ; break 'H_Reg' ≝ indxhigh ; break 'Sp_Reg' ≝ sp ; break 'Pc_Reg' ≝ pc ; break 'V_Flag' ≝ vfl ; break 'H_Flag' ≝ hfl ; break 'I_Flag' ≝ ifl ; break 'N_Flag' ≝ nfl ; break 'Z_Flag' ≝ zfl ; break 'C_Flag' ≝ cfl ; break 'IRQ_Flag' ≝ irqfl)}"
  61  non associative with precedence 80 for
  62  @{ 'mk_alu_HC08 $acclow $indxlow $indxhigh $sp $pc $vfl $hfl $ifl $nfl $zfl $cfl $irqfl }.
  63 interpretation "mk_alu_HC08" 'mk_alu_HC08 acclow indxlow indxhigh sp pc vfl hfl ifl nfl zfl cfl irqfl =
  64  (mk_alu_HC08 acclow indxlow indxhigh sp pc vfl hfl ifl nfl zfl cfl irqfl).
  65
  66 (* ****** *)
  67 (* SETTER *)
  68 (* ****** *)
  69
  70 (* setter specifico HC08/HCS08 di A *)
  71 ndefinition set_acc_8_low_reg_HC08 ≝
  72 λalu.λacclow':byte8.
  73  mk_alu_HC08
  74   acclow'
  75   (indX_low_reg_HC08 alu)
  76   (indX_high_reg_HC08 alu)
  77   (sp_reg_HC08 alu)
  78   (pc_reg_HC08 alu)
  79   (v_flag_HC08 alu)
  80   (h_flag_HC08 alu)
  81   (i_flag_HC08 alu)
  82   (n_flag_HC08 alu)
  83   (z_flag_HC08 alu)
  84   (c_flag_HC08 alu)
  85   (irq_flag_HC08 alu).
  86
  87 (* setter specifico HC08/HCS08 di X *)
  88 ndefinition set_indX_8_low_reg_HC08 ≝
  89 λalu.λindxlow':byte8.
  90  mk_alu_HC08
  91   (acc_low_reg_HC08 alu)
  92   indxlow'
  93   (indX_high_reg_HC08 alu)
  94   (sp_reg_HC08 alu)
  95   (pc_reg_HC08 alu)
  96   (v_flag_HC08 alu)
  97   (h_flag_HC08 alu)
  98   (i_flag_HC08 alu)
  99   (n_flag_HC08 alu)
 100   (z_flag_HC08 alu)
 101   (c_flag_HC08 alu)
 102   (irq_flag_HC08 alu).
 103
 104 (* setter specifico HC08/HCS08 di H *)
 105 ndefinition set_indX_8_high_reg_HC08 ≝
 106 λalu.λindxhigh':byte8.
 107  mk_alu_HC08
 108   (acc_low_reg_HC08 alu)
 109   (indX_low_reg_HC08 alu)
 110   indxhigh'
 111   (sp_reg_HC08 alu)
 112   (pc_reg_HC08 alu)
 113   (v_flag_HC08 alu)
 114   (h_flag_HC08 alu)
 115   (i_flag_HC08 alu)
 116   (n_flag_HC08 alu)
 117   (z_flag_HC08 alu)
 118   (c_flag_HC08 alu)
 119   (irq_flag_HC08 alu).
 120
 121 (* setter specifico HC08/HCS08 di H:X *)
 122 ndefinition set_indX_16_reg_HC08 ≝
 123 λalu.λindx16:word16.
 124  mk_alu_HC08
 125   (acc_low_reg_HC08 alu)
 126   (cnL ? indx16)
 127   (cnH ? indx16)
 128   (sp_reg_HC08 alu)
 129   (pc_reg_HC08 alu)
 130   (v_flag_HC08 alu)
 131   (h_flag_HC08 alu)
 132   (i_flag_HC08 alu)
 133   (n_flag_HC08 alu)
 134   (z_flag_HC08 alu)
 135   (c_flag_HC08 alu)
 136   (irq_flag_HC08 alu).
 137
 138 (* setter specifico HC08/HCS08 di SP *)
 139 ndefinition set_sp_reg_HC08 ≝
 140 λalu.λsp':word16.
 141  mk_alu_HC08
 142   (acc_low_reg_HC08 alu)
 143   (indX_low_reg_HC08 alu)
 144   (indX_high_reg_HC08 alu)
 145   sp'
 146   (pc_reg_HC08 alu)
 147   (v_flag_HC08 alu)
 148   (h_flag_HC08 alu)
 149   (i_flag_HC08 alu)
 150   (n_flag_HC08 alu)
 151   (z_flag_HC08 alu)
 152   (c_flag_HC08 alu)
 153   (irq_flag_HC08 alu).
 154
 155 (* setter specifico HC08/HCS08 di PC *)
 156 ndefinition set_pc_reg_HC08 ≝
 157 λalu.λpc':word16.
 158  mk_alu_HC08
 159   (acc_low_reg_HC08 alu)
 160   (indX_low_reg_HC08 alu)
 161   (indX_high_reg_HC08 alu)
 162   (sp_reg_HC08 alu)
 163   pc'
 164   (v_flag_HC08 alu)
 165   (h_flag_HC08 alu)
 166   (i_flag_HC08 alu)
 167   (n_flag_HC08 alu)
 168   (z_flag_HC08 alu)
 169   (c_flag_HC08 alu)
 170   (irq_flag_HC08 alu).
 171
 172 (* setter specifico HC08/HCS08 di V *)
 173 ndefinition set_v_flag_HC08 ≝
 174 λalu.λvfl':bool.
 175  mk_alu_HC08
 176   (acc_low_reg_HC08 alu)
 177   (indX_low_reg_HC08 alu)
 178   (indX_high_reg_HC08 alu)
 179   (sp_reg_HC08 alu)
 180   (pc_reg_HC08 alu)
 181   vfl'
 182   (h_flag_HC08 alu)
 183   (i_flag_HC08 alu)
 184   (n_flag_HC08 alu)
 185   (z_flag_HC08 alu)
 186   (c_flag_HC08 alu)
 187   (irq_flag_HC08 alu).
 188
 189 (* setter specifico HC08/HCS08 di H *)
 190 ndefinition set_h_flag_HC08 ≝
 191 λalu.λhfl':bool.
 192  mk_alu_HC08
 193   (acc_low_reg_HC08 alu)
 194   (indX_low_reg_HC08 alu)
 195   (indX_high_reg_HC08 alu)
 196   (sp_reg_HC08 alu)
 197   (pc_reg_HC08 alu)
 198   (v_flag_HC08 alu)
 199   hfl'
 200   (i_flag_HC08 alu)
 201   (n_flag_HC08 alu)
 202   (z_flag_HC08 alu)
 203   (c_flag_HC08 alu)
 204   (irq_flag_HC08 alu).
 205
 206 (* setter specifico HC08/HCS08 di I *)
 207 ndefinition set_i_flag_HC08 ≝
 208 λalu.λifl':bool.
 209  mk_alu_HC08
 210   (acc_low_reg_HC08 alu)
 211   (indX_low_reg_HC08 alu)
 212   (indX_high_reg_HC08 alu)
 213   (sp_reg_HC08 alu)
 214   (pc_reg_HC08 alu)
 215   (v_flag_HC08 alu)
 216   (h_flag_HC08 alu)
 217   ifl'
 218   (n_flag_HC08 alu)
 219   (z_flag_HC08 alu)
 220   (c_flag_HC08 alu)
 221   (irq_flag_HC08 alu).
 222
 223 (* setter specifico HC08/HCS08 di N *)
 224 ndefinition set_n_flag_HC08 ≝
 225 λalu.λnfl':bool.
 226  mk_alu_HC08
 227   (acc_low_reg_HC08 alu)
 228   (indX_low_reg_HC08 alu)
 229   (indX_high_reg_HC08 alu)
 230   (sp_reg_HC08 alu)
 231   (pc_reg_HC08 alu)
 232   (v_flag_HC08 alu)
 233   (h_flag_HC08 alu)
 234   (i_flag_HC08 alu)
 235   nfl'
 236   (z_flag_HC08 alu)
 237   (c_flag_HC08 alu)
 238   (irq_flag_HC08 alu).
 239
 240 (* setter specifico HC08/HCS08 di Z *)
 241 ndefinition set_z_flag_HC08 ≝
 242 λalu.λzfl':bool.
 243  mk_alu_HC08
 244   (acc_low_reg_HC08 alu)
 245   (indX_low_reg_HC08 alu)
 246   (indX_high_reg_HC08 alu)
 247   (sp_reg_HC08 alu)
 248   (pc_reg_HC08 alu)
 249   (v_flag_HC08 alu)
 250   (h_flag_HC08 alu)
 251   (i_flag_HC08 alu)
 252   (n_flag_HC08 alu)
 253   zfl'
 254   (c_flag_HC08 alu)
 255   (irq_flag_HC08 alu).
 256
 257 (* setter specifico HC08/HCS08 di C *)
 258 ndefinition set_c_flag_HC08 ≝
 259 λalu.λcfl':bool.
 260  mk_alu_HC08
 261   (acc_low_reg_HC08 alu)
 262   (indX_low_reg_HC08 alu)
 263   (indX_high_reg_HC08 alu)
 264   (sp_reg_HC08 alu)
 265   (pc_reg_HC08 alu)
 266   (v_flag_HC08 alu)
 267   (h_flag_HC08 alu)
 268   (i_flag_HC08 alu)
 269   (n_flag_HC08 alu)
 270   (z_flag_HC08 alu)
 271   cfl'
 272   (irq_flag_HC08 alu).
 273
 274 (* setter specifico HC08/HCS08 di IRQ *)
 275 ndefinition set_irq_flag_HC08 ≝
 276 λalu.λirqfl':bool.
 277  mk_alu_HC08
 278   (acc_low_reg_HC08 alu)
 279   (indX_low_reg_HC08 alu)
 280   (indX_high_reg_HC08 alu)
 281   (sp_reg_HC08 alu)
 282   (pc_reg_HC08 alu)
 283   (v_flag_HC08 alu)
 284   (h_flag_HC08 alu)
 285   (i_flag_HC08 alu)
 286   (n_flag_HC08 alu)
 287   (z_flag_HC08 alu)
 288   (c_flag_HC08 alu)
 289   irqfl'.
 290
 291 (* ***************** *)
 292 (* CONFRONTO FRA ALU *)
 293 (* ***************** *)
 294
 295 (* confronto registro per registro dell'HC08 *)
 296 ndefinition eq_HC08_alu ≝
 297 λalu1,alu2:alu_HC08.
 298  (eq_b8 (acc_low_reg_HC08 alu1) (acc_low_reg_HC08 alu2)) ⊗
 299  (eq_b8 (indX_low_reg_HC08 alu1) (indX_low_reg_HC08 alu2)) ⊗
 300  (eq_b8 (indX_high_reg_HC08 alu1) (indX_high_reg_HC08 alu2)) ⊗
 301  (eq_w16 (sp_reg_HC08 alu1) (sp_reg_HC08 alu2)) ⊗
 302  (eq_w16 (pc_reg_HC08 alu1) (pc_reg_HC08 alu2)) ⊗
 303  (eq_bool (v_flag_HC08 alu1) (v_flag_HC08 alu2)) ⊗
 304  (eq_bool (h_flag_HC08 alu1) (h_flag_HC08 alu2)) ⊗
 305  (eq_bool (i_flag_HC08 alu1) (i_flag_HC08 alu2)) ⊗
 306  (eq_bool (n_flag_HC08 alu1) (n_flag_HC08 alu2)) ⊗
 307  (eq_bool (z_flag_HC08 alu1) (z_flag_HC08 alu2)) ⊗
 308  (eq_bool (c_flag_HC08 alu1) (c_flag_HC08 alu2)) ⊗
 309  (eq_bool (irq_flag_HC08 alu1) (irq_flag_HC08 alu2)).