helm/software/matita/contribs/ng_assembly2/emulator/status/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 "emulator/memory/memory_abs.ma".
  24 include "emulator/status/HC05_status.ma".
  25 include "emulator/status/HC08_status.ma".
  26 include "emulator/status/RS08_status.ma".
  27 include "emulator/status/IP2022_status.ma".
  28 include "emulator/opcodes/pseudo.ma".
  29
  30 (* *********************************** *)
  31 (* STATUS INTERNO DEL PROCESSORE (ALU) *)
  32 (* *********************************** *)
  33
  34 (* descrittore del click = stato di avanzamento dell'esecuzione *)
  35 (* 1) None = istruzione eseguita, attesa del fetch *)
  36 (* 2) Some cur_clk,clks,pseudo,mode,cur_pc = fetch eseguito *)
  37 ndefinition aux_clk_type ≝ λm:mcu_type.Prod5T nat nat (aux_pseudo_type m) (aux_im_type m) word16.
  38
  39 nlemma clk_is_comparable : mcu_type → comparable.
  40  #m; @ (aux_clk_type m)
  41   ##[ napply (zeroc (quintuple_is_comparable nat_is_comparable nat_is_comparable (pseudo_is_comparable m) (im_is_comparable m) word16_is_comparable))
  42   ##| napply (forallc (quintuple_is_comparable nat_is_comparable nat_is_comparable (pseudo_is_comparable m) (im_is_comparable m) word16_is_comparable))
  43   ##| napply (eqc (quintuple_is_comparable nat_is_comparable nat_is_comparable (pseudo_is_comparable m) (im_is_comparable m) word16_is_comparable))
  44   ##| napply (eqc_to_eq (quintuple_is_comparable nat_is_comparable nat_is_comparable (pseudo_is_comparable m) (im_is_comparable m) word16_is_comparable))
  45   ##| napply (eq_to_eqc (quintuple_is_comparable nat_is_comparable nat_is_comparable (pseudo_is_comparable m) (im_is_comparable m) word16_is_comparable))
  46   ##| napply (neqc_to_neq (quintuple_is_comparable nat_is_comparable nat_is_comparable (pseudo_is_comparable m) (im_is_comparable m) word16_is_comparable))
  47   ##| napply (neq_to_neqc (quintuple_is_comparable nat_is_comparable nat_is_comparable (pseudo_is_comparable m) (im_is_comparable m) word16_is_comparable))
  48   ##| napply (decidable_c (quintuple_is_comparable nat_is_comparable nat_is_comparable (pseudo_is_comparable m) (im_is_comparable m) word16_is_comparable))
  49   ##| napply (symmetric_eqc (quintuple_is_comparable nat_is_comparable nat_is_comparable (pseudo_is_comparable m) (im_is_comparable m) word16_is_comparable))
  50   ##]
  51 nqed.
  52
  53 unification hint 0 ≔ M:mcu_type ⊢ carr (clk_is_comparable M) ≡ aux_clk_type M.
  54
  55 (* descritture della alu *)
  56 ndefinition aux_alu_type ≝
  57 λm.match m with
  58  [ HC05 ⇒ alu_HC05
  59  | HC08 ⇒ alu_HC08
  60  | HCS08 ⇒ alu_HC08
  61  | RS08 ⇒ alu_RS08
  62  | IP2022 ⇒ alu_IP2022
  63  ].
  64
  65 nlemma alu_is_comparable : mcu_type → comparable.
  66  #m; @ (aux_alu_type m)
  67   ##[ nelim m;
  68       ##[ napply (zeroc aluHC05_is_comparable)
  69       ##| napply (zeroc aluHC08_is_comparable)
  70       ##| napply (zeroc aluHC08_is_comparable)
  71       ##| napply (zeroc aluRS08_is_comparable)
  72       ##| napply (zeroc aluIP2022_is_comparable) ##]
  73   ##| nelim m;
  74       ##[ napply (forallc aluHC05_is_comparable)
  75       ##| napply (forallc aluHC08_is_comparable)
  76       ##| napply (forallc aluHC08_is_comparable)
  77       ##| napply (forallc aluRS08_is_comparable)
  78       ##| napply (forallc aluIP2022_is_comparable) ##]
  79   ##| nelim m;
  80       ##[ napply (eqc aluHC05_is_comparable)
  81       ##| napply (eqc aluHC08_is_comparable)
  82       ##| napply (eqc aluHC08_is_comparable)
  83       ##| napply (eqc aluRS08_is_comparable)
  84       ##| napply (eqc aluIP2022_is_comparable) ##]
  85   ##| nelim m;
  86       ##[ napply (eqc_to_eq aluHC05_is_comparable)
  87       ##| napply (eqc_to_eq aluHC08_is_comparable)
  88       ##| napply (eqc_to_eq aluHC08_is_comparable)
  89       ##| napply (eqc_to_eq aluRS08_is_comparable)
  90       ##| napply (eqc_to_eq aluIP2022_is_comparable) ##]
  91   ##| nelim m;
  92       ##[ napply (eq_to_eqc aluHC05_is_comparable)
  93       ##| napply (eq_to_eqc aluHC08_is_comparable)
  94       ##| napply (eq_to_eqc aluHC08_is_comparable)
  95       ##| napply (eq_to_eqc aluRS08_is_comparable)
  96       ##| napply (eq_to_eqc aluIP2022_is_comparable) ##]
  97   ##| nelim m;
  98       ##[ napply (neqc_to_neq aluHC05_is_comparable)
  99       ##| napply (neqc_to_neq aluHC08_is_comparable)
 100       ##| napply (neqc_to_neq aluHC08_is_comparable)
 101       ##| napply (neqc_to_neq aluRS08_is_comparable)
 102       ##| napply (neqc_to_neq aluIP2022_is_comparable) ##]
 103   ##| nelim m;
 104       ##[ napply (neq_to_neqc aluHC05_is_comparable)
 105       ##| napply (neq_to_neqc aluHC08_is_comparable)
 106       ##| napply (neq_to_neqc aluHC08_is_comparable)
 107       ##| napply (neq_to_neqc aluRS08_is_comparable)
 108       ##| napply (neq_to_neqc aluIP2022_is_comparable) ##]
 109   ##| nelim m;
 110       ##[ napply (decidable_c aluHC05_is_comparable)
 111       ##| napply (decidable_c aluHC08_is_comparable)
 112       ##| napply (decidable_c aluHC08_is_comparable)
 113       ##| napply (decidable_c aluRS08_is_comparable)
 114       ##| napply (decidable_c aluIP2022_is_comparable) ##]
 115   ##| nelim m;
 116       ##[ napply (symmetric_eqc aluHC05_is_comparable)
 117       ##| napply (symmetric_eqc aluHC08_is_comparable)
 118       ##| napply (symmetric_eqc aluHC08_is_comparable)
 119       ##| napply (symmetric_eqc aluRS08_is_comparable)
 120       ##| napply (symmetric_eqc aluIP2022_is_comparable) ##]
 121   ##]
 122 nqed.
 123
 124 unification hint 0 ≔ M:mcu_type ⊢ carr (alu_is_comparable M) ≡ aux_alu_type M.
 125
 126 (* tipo processore dipendente dalla mcu, varia solo la ALU *)
 127 nrecord any_status (mcu:mcu_type) (t:memory_impl): Type ≝
 128  {
 129  (* descrittore della alu *)
 130  alu : aux_alu_type mcu;
 131  (* descritore della memoria *)
 132  mem_desc : aux_mem_type t;
 133  (* descrittore del tipo di memoria installata *)
 134  chk_desc : aux_chk_type t;
 135  (* descrittore del clik *)
 136  clk_desc : option (aux_clk_type mcu)
 137  }.
 138
 139 (* evitare di mostrare la memoria/descrittore che impalla il visualizzatore *)
 140 notation > "{hvbox('Alu' ≝ alu ; break 'Clk' ≝ clk)}" non associative with precedence 80
 141  for @{ 'mk_any_status $alu $mem $chk $clk }.
 142 interpretation "mk_any_status" 'mk_any_status alu mem chk clk =
 143  (mk_any_status alu mem chk clk).
 144
 145 (* ******************** *)
 146 (* CONFRONTO FRA STATUS *)
 147 (* ******************** *)
 148
 149 ndefinition eq_anystatus ≝
 150 λm,t.λs1,s2:any_status m t.
 151  (eqc ? (alu … s1) (alu … s2)) ⊗
 152  (eqc ? (mem_desc … s1) (mem_desc … s2)) ⊗
 153  (eqc ? (chk_desc … s1) (chk_desc … s2)) ⊗
 154  (eqc ? (clk_desc … s1) (clk_desc … s2)).
 155
 156 ndefinition forall_anystatus ≝ λm,t.λP:any_status m t → bool.
 157  forallc ? (λr1.forallc ? (λr2.
 158  forallc ? (λr3.forallc ? (λr4.
 159  P (mk_any_status m t r1 r2 r3 r4))))).
 160
 161 (* confronto di una regione di memoria [addr1 ; ... ; addrn] *)
 162 nlet rec forall_memory_ranged
 163  (t:memory_impl)
 164  (chk1:aux_chk_type t) (chk2:aux_chk_type t)
 165  (mem1:aux_mem_type t) (mem2:aux_mem_type t)
 166  (sel:oct) (addrl:list word16) on addrl ≝
 167  match addrl return λ_.bool with
 168   [ nil ⇒ true
 169   | cons hd tl ⇒ (eqc ? (mem_read t mem1 chk1 sel hd) (mem_read t mem2 chk2 sel hd)) ⊗
 170                  (forall_memory_ranged t chk1 chk2 mem1 mem2 sel tl)
 171   ].