matita/matita/contribs/ng_assembly/emulator/status/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 "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,pseudo,mode,clks,cur_pc = fetch eseguito *)
  37 ndefinition aux_clk_type ≝ λm:mcu_type.Prod5T byte8 (aux_pseudo_type m) (aux_im_type m) byte8 word16.
  38
  39 (* tipo processore dipendente dalla mcu, varia solo la ALU *)
  40 nrecord any_status (mcu:mcu_type) (t:memory_impl): Type ≝
  41  {
  42  alu : match mcu with
  43   [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08
  44   | IP2022 ⇒ alu_IP2022 ];
  45
  46  (* descritore della memoria *)
  47  mem_desc : aux_mem_type t;
  48  (* descrittore del tipo di memoria installata *)
  49  chk_desc : aux_chk_type t;
  50  (* descrittore del clik *)
  51  clk_desc : option (aux_clk_type mcu)
  52  }.
  53
  54 (* evitare di mostrare la memoria/descrittore che impalla il visualizzatore *)
  55 notation > "{hvbox('Alu' ≝ alu ; break 'Clk' ≝ clk)}" non associative with precedence 80
  56  for @{ 'mk_any_status $alu $mem $chk $clk }.
  57 interpretation "mk_any_status" 'mk_any_status alu mem chk clk =
  58  (mk_any_status alu mem chk clk).
  59
  60 (* ******************** *)
  61 (* CONFRONTO FRA STATUS *)
  62 (* ******************** *)
  63
  64 ndefinition eq_alu ≝
  65 λm:mcu_type.
  66  match m
  67   return λm.
  68    match m with
  69     [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08
  70     | IP2022 ⇒ alu_IP2022 ] →
  71    match m with
  72     [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08
  73     | IP2022 ⇒ alu_IP2022 ] →
  74    bool
  75  with
  76   [ HC05 ⇒ eq_HC05_alu
  77   | HC08 ⇒ eq_HC08_alu
  78   | HCS08 ⇒ eq_HC08_alu
  79   | RS08 ⇒ eq_RS08_alu
  80   | IP2022 ⇒ eq_IP2022_alu
  81   ].
  82
  83 (* confronto di una regione di memoria [addr1 ; ... ; addrn] *)
  84 nlet rec forall_memory_ranged
  85  (t:memory_impl)
  86  (chk1:aux_chk_type t) (chk2:aux_chk_type t)
  87  (mem1:aux_mem_type t) (mem2:aux_mem_type t)
  88  (addrl:list word32) on addrl ≝
  89  match addrl return λ_.bool with
  90   [ nil ⇒ true
  91   | cons hd tl ⇒ (eq_option byte8 eq_b8 (mem_read t mem1 chk1 hd)
  92                                         (mem_read t mem2 chk2 hd)) ⊗
  93                  (forall_memory_ranged t chk1 chk2 mem1 mem2 tl)
  94   ].
  95
  96 ndefinition eq_clk ≝ λm.eq_option … (eq_quintuple … eq_b8 (eq_pseudo m) (eq_im m) eq_b8 eq_w16).
  97
  98 (* generalizzazione del confronto fra stati *)
  99 ndefinition eq_anystatus ≝
 100 λm:mcu_type.λt:memory_impl.λs1,s2:any_status m t.λaddrl:list word32.
 101  (* 1) confronto della ALU *)
 102  (eq_alu m (alu m t s1) (alu m t s2)) ⊗
 103  (* 2) confronto della memoria in [inf,inf+n] *)
 104  (forall_memory_ranged t (chk_desc m t s1) (chk_desc m t s2)
 105                          (mem_desc m t s1) (mem_desc m t s2) addrl) ⊗
 106  (* 3) confronto del clik *)
 107  (eq_clk m (clk_desc m t s1) (clk_desc m t s2)).