matita/matita/contribs/ng_assembly/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_ps ≝
  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 ndefinition check_susp_s ≝
  53 λm,t.λs:any_status m t.
  54  opt_map … (get_speed_reg … s)
  55   (λspeed.match eq_ex speed xF with
  56    [ true ⇒ Some ? STOP_MODE
  57    | false ⇒ None ? ]).
  58
  59 ndefinition check_susp ≝
  60 λm,t.λs:any_status m t.λps:aux_pseudo_type m.
  61  match check_susp_s … s with
  62   [ None ⇒ check_susp_ps m ps
  63   | Some susp ⇒ Some ? susp
  64   ].
  65
  66 (* raccordo *)
  67 ndefinition check_skip ≝
  68 λm.match m
  69     return λm.aux_pseudo_type m → bool
  70    with
  71  [ HC05 ⇒ Freescale_check_skip
  72  | HC08 ⇒ Freescale_check_skip
  73  | HCS08 ⇒ Freescale_check_skip
  74  | RS08 ⇒ Freescale_check_skip
  75  | IP2022 ⇒ IP2022_check_skip
  76  ].
  77
  78 (* **** *)
  79 (* TICK *)
  80 (* **** *)
  81
  82 (* - errore: errore+stato (seguira' reset o …, cmq lo stato non va buttato)
  83    - sospensione: sospensione+stato (seguira' resume o …)
  84    - ok: stato *)
  85 ninductive tick_result (A:Type) : Type ≝
  86   TickERR   : A → error_type → tick_result A
  87 | TickSUSP  : A → susp_type → tick_result A
  88 | TickOK    : A → tick_result A.
  89
  90 (* l'esecuzione e' considerata atomica quindi nel caso di un'instruzione
  91    da 3 cicli la successione sara'
  92      ([fetch/decode] s,clk:None) →
  93      (               s,clk:Some 1,pseudo,mode,3,cur_pc) →
  94      (               s,clk:Some 2,pseudo,mode,3,cur_pc) →
  95      ([execute]      s',clk:None) *)
  96 ndefinition tick_execute ≝
  97 λm,t.λs:any_status m t.
  98 λps:aux_pseudo_type m.λi:aux_im_type m.
  99 λcur_pc:word16.
 100  match execute_any m ps t s cur_pc i with
 101   (* errore! fine esecuzione *)
 102   [ None ⇒ TickERR ? (set_clk_desc … s (None ?)) ILL_FETCH_AD
 103   (* ok, aggiornamento centralizzato *)
 104   | Some S_newPC ⇒ match S_newPC with
 105    [ pair s_tmp1 new_pc ⇒
 106     (* clk azzerato *)
 107     let s_tmp2 ≝ set_clk_desc … s_tmp1 (None ?) in
 108     (* aggiornamento pc *)
 109     let s_tmp3 ≝ match eq_w16 (get_pc_reg … s) (get_pc_reg … s_tmp1) with
 110                   (* ok, new_pc → pc *)
 111                   [ true ⇒ set_pc_reg … s_tmp2 new_pc
 112                   (* effetto collaterale modifica pc! scartare new_pc *)
 113                   | false ⇒ s_tmp2 ] in
 114     match check_susp … s ps with
 115      (* esecuzione continua *)
 116      [ None ⇒ TickOK ? s_tmp3
 117      (* esecuzione sospesa *)
 118      | Some susp ⇒ TickSUSP ? s_tmp3 susp
 119      ]]].
 120
 121 (* avanza fra fetch / countdown / execute *)
 122 ndefinition tick_skip_aux ≝
 123 λm,t.λs:any_status m t.
 124  match get_skip_mode … s with
 125   [ None ⇒ false
 126   | Some b ⇒ b ].
 127
 128 ndefinition tick ≝
 129 λm,t.λs:any_status m t.
 130  match clk_desc … s with
 131   (* e' il momento del fetch *)
 132   [ None ⇒ match fetch … s with
 133    (* errore nel fetch/decode? riportato in output, nessun avanzamento *)
 134    [ FetchERR err ⇒ TickERR ? s err
 135    (* nessun errore nel fetch *)
 136    | FetchOK info cur_pc ⇒ match tick_skip_aux … s with
 137     (* skip mode! *)
 138     [ true ⇒ TickOK ? (set_clk_desc …
 139                        (set_pc_reg …
 140                         (match check_skip m (fst4T … info) with
 141                          [ true ⇒ s | false ⇒ setweak_skip_mode … s false ]) cur_pc) (None ?))
 142     (* ciclo normale *)
 143     | false ⇒ match eq_b8 〈x0,x1〉 (fth4T … info) with
 144      (* un solo clk, execute subito *)
 145      [ true ⇒ tick_execute … s (fst4T … info) (snd4T … info) cur_pc
 146      (* piu' clk, execute rimandata *)
 147      | false ⇒ TickOK ? (set_clk_desc … s
 148                          (Some ? (quintuple … 〈x0,x1〉 (fst4T … info) (snd4T … info)
 149                                               (fth4T … info) cur_pc)))
 150      ]
 151     ]
 152    ]
 153   (* fetch gia' eseguito, e' il turno di execute? *)
 154   | Some info ⇒ match eq_b8 (succ_b8 (fst5T … info)) (fth5T … info) with
 155    (* si *)
 156    [ true ⇒ tick_execute … s (snd5T … info) (thd5T … info) (fft5T … info)
 157    (* no, avanzamento cur_clk *)
 158    | false ⇒ TickOK ? (set_clk_desc … s
 159                        (Some ? (quintuple … (succ_b8 (fst5T … info)) (snd5T … info)
 160                                             (thd5T … info) (fth5T … info) (fft5T … info))))
 161    ]
 162   ].
 163
 164 (* ********** *)
 165 (* ESECUZIONE *)
 166 (* ********** *)
 167
 168 nlet rec execute (m:mcu_type) (t:memory_impl) (s:tick_result (any_status m t)) (n:nat) on n ≝
 169  match s with
 170   [ TickERR s' error ⇒ TickERR ? s' error
 171   | TickSUSP s' susp ⇒ TickSUSP ? s' susp
 172   | TickOK s'        ⇒ match n with [ O ⇒ TickOK ? s' | S n' ⇒ execute m t (tick m t s') n' ]
 173   ].