1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* ********************************************************************** *)
16 (* Progetto FreeScale *)
18 (* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
19 (* Sviluppo: 2008-2010 *)
21 (* ********************************************************************** *)
23 include "emulator/multivm/Freescale_multivm.ma".
24 include "emulator/multivm/IP2022_multivm.ma".
25 include "emulator/read_write/fetch.ma".
28 ndefinition execute_any ≝
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)
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 ?
41 ndefinition check_susp_ps ≝
43 return λm.aux_pseudo_type m → option susp_type
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
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
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
67 ndefinition check_skip ≝
69 return λm.aux_pseudo_type m → bool
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
82 (* - errore: errore+stato (seguira' reset o …, cmq lo stato non va buttato)
83 - sospensione: sospensione+stato (seguira' resume o …)
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.
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.
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 ⇒
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
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
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
138 [ true ⇒ TickOK ? (set_clk_desc …
140 (match check_skip m (fst4T … info) with
141 [ true ⇒ s | false ⇒ setweak_skip_mode … s false ]) cur_pc) (None ?))
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)))
153 (* fetch gia' eseguito, e' il turno di execute? *)
154 | Some info ⇒ match eq_b8 (succ_b8 (fst5T … info)) (fth5T … info) with
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))))
168 nlet rec execute (m:mcu_type) (t:memory_impl) (s:tick_result (any_status m t)) (n:nat) on n ≝
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' ]