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 (* Ultima modifica: 05/08/2009 *)
21 (* ********************************************************************** *)
23 include "freescale/opcode_base.ma".
24 include "common/list.ma".
26 (* ********************************************* *)
27 (* STRUMENTI PER LE DIMOSTRAZIONI DI CORRETTEZZA *)
28 (* ********************************************* *)
30 (* su tutta la lista quante volte compare il byte *)
31 nlet rec get_byte_count (m:mcu_type) (b:byte8) (c:word16)
32 (l:list (Prod4T (any_opcode m) instr_mode byte8_or_word16 byte8)) on l ≝
35 | cons hd tl ⇒ match thd4T … hd with
36 [ Byte b' ⇒ match eq_b8 b b' with
37 [ true ⇒ get_byte_count m b (succ_w16 c) tl
38 | false ⇒ get_byte_count m b c tl
40 | Word _ ⇒ get_byte_count m b c tl
44 (* su tutta la lista quante volte compare la word (0x9E+byte) *)
45 nlet rec get_word_count (m:mcu_type) (b:byte8) (c:word16)
46 (l:list (Prod4T (any_opcode m) instr_mode byte8_or_word16 byte8)) on l ≝
49 | cons hd tl ⇒ match thd4T … hd with
50 [ Byte _ ⇒ get_word_count m b c tl
51 | Word w ⇒ match eq_w16 〈〈x9,xE〉:b〉 w with
52 [ true ⇒ get_word_count m b (succ_w16 c) tl
53 | false ⇒ get_word_count m b c tl
58 (* su tutta la lista quante volte compare lo pseudocodice *)
59 nlet rec get_pseudo_count (m:mcu_type) (o:opcode) (c:word16)
60 (l:list (Prod4T (any_opcode m) instr_mode byte8_or_word16 byte8)) on l ≝
63 | cons hd tl ⇒ match fst4T … hd with
64 [ anyOP o' ⇒ match eq_op o o' with
65 [ true ⇒ get_pseudo_count m o (succ_w16 c) tl
66 | false ⇒ get_pseudo_count m o c tl
71 (* su tutta la lista quante volte compare la modalita' *)
72 nlet rec get_mode_count (m:mcu_type) (i:instr_mode) (c:word16)
73 (l:list (Prod4T (any_opcode m) instr_mode byte8_or_word16 byte8)) on l ≝
76 | cons hd tl ⇒ match eq_im (snd4T … hd) i with
77 [ true ⇒ get_mode_count m i (succ_w16 c) tl
78 | false ⇒ get_mode_count m i c tl
82 (* b e' non implementato? *)
83 nlet rec test_not_impl_byte (b:byte8) (l:list byte8) on l ≝
86 | cons hd tl ⇒ match eq_b8 b hd with
88 | false ⇒ test_not_impl_byte b tl
92 (* o e' non implementato? *)
93 nlet rec test_not_impl_pseudo (o:opcode) (l:list opcode) on l ≝
96 | cons hd tl ⇒ match eq_op o hd with
98 | false ⇒ test_not_impl_pseudo o tl
102 (* i e' non implementato? *)
103 nlet rec test_not_impl_mode (i:instr_mode) (l:list instr_mode) on l ≝
106 | cons hd tl ⇒ match eq_im i hd with
108 | false ⇒ test_not_impl_mode i tl
112 (* su tutta la lista quante volte compare la coppia opcode,instr_mode *)
113 nlet rec get_OpIm_count (m:mcu_type) (o:any_opcode m) (i:instr_mode) (c:word16)
114 (l:list (Prod4T (any_opcode m) instr_mode byte8_or_word16 byte8)) on l ≝
118 match (eq_anyop m o (fst4T … hd)) ⊗
119 (eq_im i (snd4T … hd)) with
120 [ true ⇒ get_OpIm_count m o i (succ_w16 c) tl
121 | false ⇒ get_OpIm_count m o i c tl
125 (* iteratore sugli opcode *)
126 ndefinition forall_op ≝ λP.
127 P ADC ⊗ P ADD ⊗ P AIS ⊗ P AIX ⊗ P AND ⊗ P ASL ⊗ P ASR ⊗ P BCC ⊗
128 P BCLRn ⊗ P BCS ⊗ P BEQ ⊗ P BGE ⊗ P BGND ⊗ P BGT ⊗ P BHCC ⊗ P BHCS ⊗
129 P BHI ⊗ P BIH ⊗ P BIL ⊗ P BIT ⊗ P BLE ⊗ P BLS ⊗ P BLT ⊗ P BMC ⊗
130 P BMI ⊗ P BMS ⊗ P BNE ⊗ P BPL ⊗ P BRA ⊗ P BRCLRn ⊗ P BRN ⊗ P BRSETn ⊗
131 P BSETn ⊗ P BSR ⊗ P CBEQA ⊗ P CBEQX ⊗ P CLC ⊗ P CLI ⊗ P CLR ⊗ P CMP ⊗
132 P COM ⊗ P CPHX ⊗ P CPX ⊗ P DAA ⊗ P DBNZ ⊗ P DEC ⊗ P DIV ⊗ P EOR ⊗
133 P INC ⊗ P JMP ⊗ P JSR ⊗ P LDA ⊗ P LDHX ⊗ P LDX ⊗ P LSR ⊗ P MOV ⊗
134 P MUL ⊗ P NEG ⊗ P NOP ⊗ P NSA ⊗ P ORA ⊗ P PSHA ⊗ P PSHH ⊗ P PSHX ⊗
135 P PULA ⊗ P PULH ⊗ P PULX ⊗ P ROL ⊗ P ROR ⊗ P RSP ⊗ P RTI ⊗ P RTS ⊗
136 P SBC ⊗ P SEC ⊗ P SEI ⊗ P SHA ⊗ P SLA ⊗ P STA ⊗ P STHX ⊗ P STOP ⊗
137 P STX ⊗ P SUB ⊗ P SWI ⊗ P TAP ⊗ P TAX ⊗ P TPA ⊗ P TST ⊗ P TSX ⊗
138 P TXA ⊗ P TXS ⊗ P WAIT.
140 (* iteratore sulle modalita' *)
141 ndefinition forall_im ≝ λP.
162 ⊗ P MODE_DIR1_to_DIR1
163 ⊗ P MODE_IMM1_to_DIR1
164 ⊗ P MODE_IX0p_to_DIR1
165 ⊗ P MODE_DIR1_to_IX0p
167 ⊗ P MODE_INHA_and_IMM1
168 ⊗ P MODE_INHX_and_IMM1
169 ⊗ P MODE_IMM1_and_IMM1
170 ⊗ P MODE_DIR1_and_IMM1
171 ⊗ P MODE_IX0_and_IMM1
172 ⊗ P MODE_IX0p_and_IMM1
173 ⊗ P MODE_IX1_and_IMM1
174 ⊗ P MODE_IX1p_and_IMM1
175 ⊗ P MODE_SP1_and_IMM1
177 ⊗ forall_oct (λo. P (MODE_DIRn o))
178 ⊗ forall_oct (λo. P (MODE_DIRn_and_IMM1 o))
179 ⊗ forall_ex (λe. P (MODE_TNY e))
180 ⊗ forall_bit (λt. P (MODE_SRT t)).