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/opcodes/Freescale_pseudo.ma".
24 include "emulator/opcodes/Freescale_instr_mode.ma".
25 include "emulator/opcodes/IP2022_pseudo.ma".
26 include "emulator/opcodes/IP2022_instr_mode.ma".
27 include "emulator/opcodes/byte_or_word.ma".
28 include "common/list.ma".
30 (* ********************************************** *)
31 (* MATTONI BASE PER DEFINIRE LE TABELLE DELLE MCU *)
32 (* ********************************************** *)
34 (* enumerazione delle ALU *)
35 ninductive mcu_type: Type ≝
42 ndefinition eq_mcutype ≝
45 [ HC05 ⇒ match m2 with [ HC05 ⇒ true | _ ⇒ false ]
46 | HC08 ⇒ match m2 with [ HC08 ⇒ true | _ ⇒ false ]
47 | HCS08 ⇒ match m2 with [ HCS08 ⇒ true | _ ⇒ false ]
48 | RS08 ⇒ match m2 with [ RS08 ⇒ true | _ ⇒ false ]
49 | IP2022 ⇒ match m2 with [ IP2022 ⇒ true | _ ⇒ false ]
52 ndefinition aux_pseudo_type ≝
53 λmcu:mcu_type.match mcu with
54 [ HC05 ⇒ Freescale_pseudo
55 | HC08 ⇒ Freescale_pseudo
56 | HCS08 ⇒ Freescale_pseudo
57 | RS08 ⇒ Freescale_pseudo
58 | IP2022 ⇒ IP2022_pseudo
61 ndefinition aux_im_type ≝
62 λmcu:mcu_type.match mcu with
63 [ HC05 ⇒ Freescale_instr_mode
64 | HC08 ⇒ Freescale_instr_mode
65 | HCS08 ⇒ Freescale_instr_mode
66 | RS08 ⇒ Freescale_instr_mode
67 | IP2022 ⇒ IP2022_instr_mode
70 ndefinition eq_pseudo ≝
73 return λm.aux_pseudo_type m → aux_pseudo_type m → bool
75 [ HC05 ⇒ eq_Freescale_pseudo
76 | HC08 ⇒ eq_Freescale_pseudo
77 | HCS08 ⇒ eq_Freescale_pseudo
78 | RS08 ⇒ eq_Freescale_pseudo
79 | IP2022 ⇒ eq_IP2022_pseudo
85 return λm.aux_im_type m → aux_im_type m → bool
87 [ HC05 ⇒ eq_Freescale_im
88 | HC08 ⇒ eq_Freescale_im
89 | HCS08 ⇒ eq_Freescale_im
90 | RS08 ⇒ eq_Freescale_im
91 | IP2022 ⇒ eq_IP2022_im
94 ndefinition forall_pseudo ≝
97 return λm.(aux_pseudo_type m → bool) → bool
99 [ HC05 ⇒ forall_Freescale_pseudo
100 | HC08 ⇒ forall_Freescale_pseudo
101 | HCS08 ⇒ forall_Freescale_pseudo
102 | RS08 ⇒ forall_Freescale_pseudo
103 | IP2022 ⇒ forall_IP2022_pseudo
106 ndefinition forall_im ≝
109 return λm.(aux_im_type m → bool) → bool
111 [ HC05 ⇒ forall_Freescale_im
112 | HC08 ⇒ forall_Freescale_im
113 | HCS08 ⇒ forall_Freescale_im
114 | RS08 ⇒ forall_Freescale_im
115 | IP2022 ⇒ forall_IP2022_im
118 (* ********************************************* *)
119 (* STRUMENTI PER LE DIMOSTRAZIONI DI CORRETTEZZA *)
120 (* ********************************************* *)
122 ndefinition aux_table_type ≝ λmcu:mcu_type.Prod4T (aux_pseudo_type mcu) (aux_im_type mcu) byte8_or_word16 byte8.
124 (* su tutta la lista quante volte compare il byte *)
125 nlet rec get_byte_count (m:mcu_type) (b:byte8) (c:word16) (l:list (aux_table_type m)) on l ≝
128 | cons hd tl ⇒ match thd4T … hd with
129 [ Byte b' ⇒ match eq_b8 b b' with
130 [ true ⇒ get_byte_count m b (succ_w16 c) tl
131 | false ⇒ get_byte_count m b c tl
133 | Word _ ⇒ get_byte_count m b c tl
137 (* su tutta la lista quante volte compare la word *)
138 nlet rec get_word_count (m:mcu_type) (w:word16) (c:word16) (l:list (aux_table_type m)) on l ≝
141 | cons hd tl ⇒ match thd4T … hd with
142 [ Byte _ ⇒ get_word_count m w c tl
143 | Word w' ⇒ match eq_w16 w w' with
144 [ true ⇒ get_word_count m w (succ_w16 c) tl
145 | false ⇒ get_word_count m w c tl
150 (* su tutta la lista quante volte compare lo pseudocodice *)
151 nlet rec get_pseudo_count (m:mcu_type) (o:aux_pseudo_type m) (c:word16) (l:list (aux_table_type m)) on l ≝
154 | cons hd tl ⇒ match eq_pseudo m o (fst4T … hd) with
155 [ true ⇒ get_pseudo_count m o (succ_w16 c) tl
156 | false ⇒ get_pseudo_count m o c tl
160 (* su tutta la lista quante volte compare la modalita' *)
161 nlet rec get_mode_count (m:mcu_type) (i:aux_im_type m) (c:word16) (l:list (aux_table_type m)) on l ≝
164 | cons hd tl ⇒ match eq_im m i (snd4T … hd) with
165 [ true ⇒ get_mode_count m i (succ_w16 c) tl
166 | false ⇒ get_mode_count m i c tl
170 (* b e' non implementato? *)
171 nlet rec test_not_impl_byte (b:byte8) (l:list byte8) on l ≝
174 | cons hd tl ⇒ match eq_b8 b hd with
176 | false ⇒ test_not_impl_byte b tl
180 (* su tutta la lista quante volte compare la coppia pseudo,instr_mode *)
181 nlet rec get_PsIm_count (m:mcu_type) (o:aux_pseudo_type m) (i:aux_im_type m) (c:word16) (l:list (aux_table_type m)) on l ≝
185 match (eq_pseudo m o (fst4T … hd)) ⊗
186 (eq_im m i (snd4T … hd)) with
187 [ true ⇒ get_PsIm_count m o i (succ_w16 c) tl
188 | false ⇒ get_PsIm_count m o i c tl
192 (* o e' non implementato? *)
193 nlet rec test_not_impl_pseudo (m:mcu_type) (o:aux_pseudo_type m) (l:list (aux_pseudo_type m)) on l ≝
196 | cons hd tl ⇒ match eq_pseudo m o hd with
198 | false ⇒ test_not_impl_pseudo m o tl
202 (* i e' non implementato? *)
203 nlet rec test_not_impl_mode (m:mcu_type) (i:aux_im_type m) (l:list (aux_im_type m)) on l ≝
206 | cons hd tl ⇒ match eq_im m i hd with
208 | false ⇒ test_not_impl_mode m i tl