matita/matita/contribs/ng_assembly2/emulator/multivm/multivm.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/multivm/Freescale_multivm.ma".
  24 include "emulator/multivm/IP2022_multivm.ma".
  25 include "emulator/read_write/fetch.ma".
  26
  27 (* raccordo *)
  28 ndefinition execute_any ≝
  29 λm.match m
  30     return λm.aux_pseudo_type m → Πt.any_status m t → word16 →
  31               aux_im_type m → option (ProdT (any_status m t) word16)
  32    with
  33  [ HC05 ⇒ λps:aux_pseudo_type ?.Freescale_execute_any ps ?
  34  | HC08 ⇒ λps:aux_pseudo_type ?.Freescale_execute_any ps ?
  35  | HCS08 ⇒ λps:aux_pseudo_type ?.Freescale_execute_any ps ?
  36  | RS08 ⇒ λps:aux_pseudo_type ?.Freescale_execute_any ps ?
  37  | IP2022 ⇒ λps:aux_pseudo_type ?.IP2022_execute_any ps ?
  38  ].
  39
  40 (* raccordo *)
  41 ndefinition check_susp ≝
  42 λm.match m
  43     return λm.aux_pseudo_type m → option susp_type
  44    with
  45  [ HC05 ⇒ Freescale_check_susp
  46  | HC08 ⇒ Freescale_check_susp
  47  | HCS08 ⇒ Freescale_check_susp
  48  | RS08 ⇒ Freescale_check_susp
  49  | IP2022 ⇒ IP2022_check_susp
  50  ].
  51
  52 (* raccordo *)
  53 ndefinition check_skip ≝
  54 λm.match m
  55     return λm.aux_pseudo_type m → bool
  56    with
  57  [ HC05 ⇒ Freescale_check_skip
  58  | HC08 ⇒ Freescale_check_skip
  59  | HCS08 ⇒ Freescale_check_skip
  60  | RS08 ⇒ Freescale_check_skip
  61  | IP2022 ⇒ IP2022_check_skip
  62  ].
  63
  64 (* motiplicatore del ciclo di durata *)
  65 (* 0 = sospensione *)
  66 ndefinition clk_mult ≝
  67 λm.match m
  68     return λm.Πt.any_status m t → nat
  69    with
  70  [ HC05 ⇒ Freescale_clk_mult HC05
  71  | HC08 ⇒ Freescale_clk_mult HC08
  72  | HCS08 ⇒ Freescale_clk_mult HCS08
  73  | RS08 ⇒ Freescale_clk_mult RS08
  74  | IP2022 ⇒ IP2022_clk_mult
  75  ].
  76
  77 (* **** *)
  78 (* TICK *)
  79 (* **** *)
  80
  81 (* - errore: errore+stato (seguira' reset o …, cmq lo stato non va buttato)
  82    - sospensione: sospensione+stato (seguira' resume o …)
  83    - ok: stato *)
  84 ninductive tick_result (A:Type) : Type ≝
  85   TickERR   : A → error_type → tick_result A
  86 | TickSUSP  : A → susp_type → tick_result A
  87 | TickOK    : A → tick_result A.
  88
  89 (* l'esecuzione e' considerata atomica quindi nel caso di un'instruzione
  90    da 3 cicli la successione sara'
  91      ([fetch/decode] s,clk:None) →
  92      (               s,clk:Some 1,pseudo,mode,3,cur_pc) →
  93      (               s,clk:Some 2,pseudo,mode,3,cur_pc) →
  94      ([execute]      s',clk:None) *)
  95 ndefinition tick_execute ≝
  96 λm,t.λs:any_status m t.
  97 λps:aux_pseudo_type m.λi:aux_im_type m.
  98 λcur_pc:word16.
  99  match execute_any m ps t s cur_pc i with
 100   (* errore! fine esecuzione *)
 101   [ None ⇒ TickERR ? (set_clk_desc … s (None ?)) ILL_FETCH_AD
 102   (* ok, aggiornamento centralizzato *)
 103   | Some S_newPC ⇒ match S_newPC with
 104    [ pair s_tmp1 new_pc ⇒
 105     (* clk azzerato *)
 106     let s_tmp2 ≝ set_clk_desc … s_tmp1 (None ?) in
 107     (* aggiornamento pc *)
 108     let s_tmp3 ≝ match eqc ? (get_pc_reg … s) (get_pc_reg … s_tmp1) with
 109                   (* ok, new_pc → pc *)
 110                   [ true ⇒ set_pc_reg … s_tmp2 new_pc
 111                   (* effetto collaterale modifica pc! scartare new_pc *)
 112                   | false ⇒ s_tmp2 ] in
 113     match check_susp m ps with
 114      (* esecuzione continua *)
 115      [ None ⇒ TickOK ? s_tmp3
 116      (* esecuzione sospesa *)
 117      | Some susp ⇒ TickSUSP ? s_tmp3 susp
 118      ]]].
 119
 120 (* avanza fra fetch / countdown / execute *)
 121 ndefinition tick_skip_aux ≝
 122 λm,t.λs:any_status m t.
 123  match get_skip_mode … s with
 124   [ None ⇒ false
 125   | Some b ⇒ b ].
 126
 127 (* descrittore del fetch PSEUDO + INSTR_MODE + OPCODE + CICLI *)
 128
 129 (* descrittore del click = stato di avanzamento dell'esecuzione *)
 130 (* 1) None = istruzione eseguita, attesa del fetch *)
 131 (* 2) Some cur_clk,clks,pseudo,mode,cur_pc = fetch eseguito *)
 132 ndefinition tick ≝
 133 λm,t.λs:any_status m t.
 134  match clk_desc … s with
 135   (* e' il momento del fetch *)
 136   [ None ⇒ match fetch … s with
 137    (* errore nel fetch/decode? riportato in output, nessun avanzamento *)
 138    [ FetchERR err ⇒ TickERR ? s err
 139    (* nessun errore nel fetch *)
 140    | FetchOK finfo cur_pc ⇒ match tick_skip_aux … s with
 141     (* skip mode! *)
 142     [ true ⇒ TickOK ? (set_clk_desc …
 143                        (set_pc_reg …
 144                         (match check_skip m (fst4T … finfo) with
 145                          [ true ⇒ s | false ⇒ setweak_skip_mode … s false ]) cur_pc) (None ?))
 146     (* ciclo normale: applicare divisore a numero reale di cicli *)
 147     | false ⇒
 148      let real_clk ≝ (clk_mult … s)*(fth4T … finfo) in
 149      match real_clk with
 150       (* 0 = stop *)
 151       [ O ⇒ TickSUSP ? s STOP_MODE
 152       | S clk' ⇒ match clk' with
 153        (* un solo clk, execute subito *)
 154        [ O ⇒ tick_execute … s (fst4T … finfo) (snd4T … finfo) cur_pc
 155        (* piu' clk, execute rimandata *)
 156        | S clk'' ⇒ TickOK ? (set_clk_desc … s
 157                             (Some ? (quintuple … nat1 real_clk
 158                                                  (fst4T … finfo) (snd4T … finfo) cur_pc)))
 159        ]
 160       ]
 161     ]
 162    ]
 163   (* fetch gia' eseguito, e' il turno di execute? *)
 164   | Some sinfo ⇒ match eqc ? (S (fst5T … sinfo)) (snd5T … sinfo) with
 165    (* si *)
 166    [ true ⇒ tick_execute … s (thd5T … sinfo) (fth5T … sinfo) (fft5T … sinfo)
 167    (* no, avanzamento cur_clk *)
 168    | false ⇒ TickOK ? (set_clk_desc … s
 169                        (Some ? (quintuple … (S (fst5T … sinfo)) (snd5T … sinfo)
 170                                             (thd5T … sinfo) (fth5T … sinfo) (fft5T … sinfo))))
 171    ]
 172   ].
 173
 174 (* ********** *)
 175 (* ESECUZIONE *)
 176 (* ********** *)
 177
 178 nlet rec execute (m:mcu_type) (t:memory_impl) (s:tick_result (any_status m t)) (n:nat) on n ≝
 179  match s with
 180   [ TickERR s' error ⇒ TickERR ? s' error
 181   | TickSUSP s' susp ⇒ TickSUSP ? s' susp
 182   | TickOK s'        ⇒ match n with [ O ⇒ TickOK ? s' | S n' ⇒ execute m t (tick m t s') n' ]
 183   ].
 184
 185 nlemma breakpoint_err : ∀m,t,s,err,n.execute m t (TickERR ? s err) n = TickERR ? s err.
 186  #m; #t; #s; #err; #n;
 187  ncases n;
 188  ##[ ##2: #n1; ##]
 189  nnormalize;
 190  napply refl_eq.
 191 nqed.
 192
 193 nlemma breakpoint_susp : ∀m,t,s,susp,n.execute m t (TickSUSP ? s susp) n = TickSUSP ? s susp.
 194  #m; #t; #s; #susp; #n;
 195  ncases n;
 196  ##[ ##2: #n1; ##]
 197  nnormalize;
 198  napply refl_eq.
 199 nqed.
 200
 201 nlemma breakpoint :
 202  ∀m,t,n1,n2,s. execute m t s (n1 + n2) = execute m t (execute m t s n1) n2.
 203  #m; #t; #n1;
 204  nelim n1;
 205  ##[ ##1: nnormalize; #n2; #s; ncases s; nnormalize; ##[ ##1,2: #x ##] #y; napply refl_eq
 206  ##| ##2: #n3; #H; #n2; #s; ncases s;
 207           ##[ ##1: #x; #y; nnormalize; nrewrite > (breakpoint_err m t x y n2); napply refl_eq
 208           ##| ##2: #x; #y; nnormalize; nrewrite > (breakpoint_susp m t x y n2); napply refl_eq
 209           ##| ##3: #x; nrewrite > (Sn_p_n_to_S_npn n3 n2);
 210                    nchange with ((execute m t (tick m t x) (n3+n2)) =
 211                                  (execute m t (execute m t (tick m t x) n3) n2));
 212                    nrewrite > (H n2 (tick m t x));
 213                    napply refl_eq
 214           ##]
 215  ##]
 216 nqed.