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/HC05_opcode.ma".
24 include "emulator/opcodes/HC05_instr_mode.ma".
25 include "emulator/opcodes/HC08_opcode.ma".
26 include "emulator/opcodes/HC08_instr_mode.ma".
27 include "emulator/opcodes/HCS08_opcode.ma".
28 include "emulator/opcodes/RS08_opcode.ma".
29 include "emulator/opcodes/RS08_instr_mode.ma".
30 include "emulator/opcodes/IP2022_opcode.ma".
31 include "emulator/opcodes/IP2022_instr_mode.ma".
32 include "emulator/opcodes/byte_or_word.ma".
33 include "common/list.ma".
35 (* ********************************************** *)
36 (* MATTONI BASE PER DEFINIRE LE TABELLE DELLE MCU *)
37 (* ********************************************** *)
39 (* enumerazione delle ALU *)
40 ninductive mcu_type: Type ≝
47 ndefinition eq_mcutype ≝
50 [ HC05 ⇒ match m2 with [ HC05 ⇒ true | _ ⇒ false ]
51 | HC08 ⇒ match m2 with [ HC08 ⇒ true | _ ⇒ false ]
52 | HCS08 ⇒ match m2 with [ HCS08 ⇒ true | _ ⇒ false ]
53 | RS08 ⇒ match m2 with [ RS08 ⇒ true | _ ⇒ false ]
54 | IP2022 ⇒ match m2 with [ IP2022 ⇒ true | _ ⇒ false ]
57 ndefinition aux_op_type ≝
58 λmcu:mcu_type.match mcu with
61 | HCS08 ⇒ HCS08_opcode
63 | IP2022 ⇒ IP2022_opcode
66 ndefinition aux_im_type ≝
67 λmcu:mcu_type.match mcu with
68 [ HC05 ⇒ HC05_instr_mode
69 | HC08 ⇒ HC08_instr_mode
70 | HCS08 ⇒ HC08_instr_mode
71 | RS08 ⇒ RS08_instr_mode
72 | IP2022 ⇒ IP2022_instr_mode
78 return λm.aux_op_type m → aux_op_type m → bool
84 | IP2022 ⇒ eq_IP2022_op
90 return λm.aux_im_type m → aux_im_type m → bool
96 | IP2022 ⇒ eq_IP2022_im
99 ndefinition forall_op ≝
102 return λm.(aux_op_type m → bool) → bool
104 [ HC05 ⇒ forall_HC05_op
105 | HC08 ⇒ forall_HC08_op
106 | HCS08 ⇒ forall_HCS08_op
107 | RS08 ⇒ forall_RS08_op
108 | IP2022 ⇒ forall_IP2022_op
111 ndefinition forall_im ≝
114 return λm.(aux_im_type m → bool) → bool
116 [ HC05 ⇒ forall_HC05_im
117 | HC08 ⇒ forall_HC08_im
118 | HCS08 ⇒ forall_HC08_im
119 | RS08 ⇒ forall_RS08_im
120 | IP2022 ⇒ forall_IP2022_im
123 (* ********************************************* *)
124 (* STRUMENTI PER LE DIMOSTRAZIONI DI CORRETTEZZA *)
125 (* ********************************************* *)
127 ndefinition aux_table_type ≝ λmcu:mcu_type.Prod4T (aux_op_type mcu) (aux_im_type mcu) byte8_or_word16 byte8.
129 (* su tutta la lista quante volte compare il byte *)
130 nlet rec get_byte_count (m:mcu_type) (b:byte8) (c:word16) (l:list (aux_table_type m)) on l ≝
133 | cons hd tl ⇒ match thd4T … hd with
134 [ Byte b' ⇒ match eq_b8 b b' with
135 [ true ⇒ get_byte_count m b (succ_w16 c) tl
136 | false ⇒ get_byte_count m b c tl
138 | Word _ ⇒ get_byte_count m b c tl
142 (* su tutta la lista quante volte compare la word *)
143 nlet rec get_word_count (m:mcu_type) (w:word16) (c:word16) (l:list (aux_table_type m)) on l ≝
146 | cons hd tl ⇒ match thd4T … hd with
147 [ Byte _ ⇒ get_word_count m w c tl
148 | Word w' ⇒ match eq_w16 w w' with
149 [ true ⇒ get_word_count m w (succ_w16 c) tl
150 | false ⇒ get_word_count m w c tl
155 (* su tutta la lista quante volte compare lo pseudocodice *)
156 nlet rec get_pseudo_count (m:mcu_type) (o:aux_op_type m) (c:word16) (l:list (aux_table_type m)) on l ≝
159 | cons hd tl ⇒ match eq_op m o (fst4T … hd) with
160 [ true ⇒ get_pseudo_count m o (succ_w16 c) tl
161 | false ⇒ get_pseudo_count m o c tl
165 (* su tutta la lista quante volte compare la modalita' *)
166 nlet rec get_mode_count (m:mcu_type) (i:aux_im_type m) (c:word16) (l:list (aux_table_type m)) on l ≝
169 | cons hd tl ⇒ match eq_im m i (snd4T … hd) with
170 [ true ⇒ get_mode_count m i (succ_w16 c) tl
171 | false ⇒ get_mode_count m i c tl
175 (* b e' non implementato? *)
176 nlet rec test_not_impl_byte (b:byte8) (l:list byte8) on l ≝
179 | cons hd tl ⇒ match eq_b8 b hd with
181 | false ⇒ test_not_impl_byte b tl
185 (* su tutta la lista quante volte compare la coppia opcode,instr_mode *)
186 nlet rec get_OpIm_count (m:mcu_type) (o:aux_op_type m) (i:aux_im_type m) (c:word16) (l:list (aux_table_type m)) on l ≝
190 match (eq_op m o (fst4T … hd)) ⊗
191 (eq_im m i (snd4T … hd)) with
192 [ true ⇒ get_OpIm_count m o i (succ_w16 c) tl
193 | false ⇒ get_OpIm_count m o i c tl