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 ≝
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
53 ndefinition check_skip ≝
55 return λm.aux_pseudo_type m → bool
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
64 (* motiplicatore del ciclo di durata *)
66 ndefinition clk_mult ≝
68 return λm.Πt.any_status m t → nat
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
81 (* - errore: errore+stato (seguira' reset o …, cmq lo stato non va buttato)
82 - sospensione: sospensione+stato (seguira' resume o …)
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.
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.
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 ⇒
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
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
127 (* descrittore del fetch PSEUDO + INSTR_MODE + OPCODE + CICLI *)
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 *)
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
142 [ true ⇒ TickOK ? (set_clk_desc …
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 *)
148 let real_clk ≝ (clk_mult … s)*(fth4T … finfo) in
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)))
163 (* fetch gia' eseguito, e' il turno di execute? *)
164 | Some sinfo ⇒ match eqc ? (S (fst5T … sinfo)) (snd5T … sinfo) with
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))))
178 nlet rec execute (m:mcu_type) (t:memory_impl) (s:tick_result (any_status m t)) (n:nat) on n ≝
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' ]
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;
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;
202 ∀m,t,n1,n2,s. execute m t s (n1 + n2) = execute m t (execute m t s n1) n2.
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));