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