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: Cosimo Oliboni, oliboni@cs.unibo.it *)
19 (* Cosimo Oliboni, oliboni@cs.unibo.it *)
21 (* ********************************************************************** *)
23 include "freescale/opcode_base.ma".
25 (* ********************************************* *)
26 (* STRUMENTI PER LE DIMOSTRAZIONI DI CORRETTEZZA *)
27 (* ********************************************* *)
29 (* su tutta la lista quante volte compare il byte *)
30 nlet rec get_byte_count (m:mcu_type) (b:byte8) (c:nat)
31 (l:list (Prod4T (any_opcode m) instr_mode byte8_or_word16 byte8)) on l ≝
34 | cons hd tl ⇒ match thd4T ???? hd with
35 [ Byte b' ⇒ match eq_b8 b b' with
36 [ true ⇒ get_byte_count m b (S c) tl
37 | false ⇒ get_byte_count m b c tl
39 | Word _ ⇒ get_byte_count m b c tl
43 (* su tutta la lista quante volte compare la word (0x9E+byte) *)
44 nlet rec get_word_count (m:mcu_type) (b:byte8) (c:nat)
45 (l:list (Prod4T (any_opcode m) instr_mode byte8_or_word16 byte8)) on l ≝
48 | cons hd tl ⇒ match thd4T ???? hd with
49 [ Byte _ ⇒ get_word_count m b c tl
50 | Word w ⇒ match eq_w16 〈〈x9,xE〉:b〉 w with
51 [ true ⇒ get_word_count m b (S c) tl
52 | false ⇒ get_word_count m b c tl
57 (* su tutta la lista quante volte compare lo pseudocodice *)
58 nlet rec get_pseudo_count (m:mcu_type) (o:opcode) (c:nat)
59 (l:list (Prod4T (any_opcode m) instr_mode byte8_or_word16 byte8)) on l ≝
62 | cons hd tl ⇒ match fst4T ???? hd with
63 [ anyOP o' ⇒ match eq_op o o' with
64 [ true ⇒ get_pseudo_count m o (S c) tl
65 | false ⇒ get_pseudo_count m o c tl
70 (* su tutta la lista quante volte compare la modalita' *)
71 nlet rec get_mode_count (m:mcu_type) (i:instr_mode) (c:nat)
72 (l:list (Prod4T (any_opcode m) instr_mode byte8_or_word16 byte8)) on l ≝
75 | cons hd tl ⇒ match eq_instrmode (snd4T ???? hd) i with
76 [ true ⇒ get_mode_count m i (S c) tl
77 | false ⇒ get_mode_count m i c tl
81 (* b e' non implementato? *)
82 nlet rec test_not_impl_byte (b:byte8) (l:list byte8) on l ≝
85 | cons hd tl ⇒ match eq_b8 b hd with
87 | false ⇒ test_not_impl_byte b tl
91 (* o e' non implementato? *)
92 nlet rec test_not_impl_pseudo (o:opcode) (l:list opcode) on l ≝
95 | cons hd tl ⇒ match eq_op o hd with
97 | false ⇒ test_not_impl_pseudo o tl
101 (* i e' non implementato? *)
102 nlet rec test_not_impl_mode (i:instr_mode) (l:list instr_mode) on l ≝
105 | cons hd tl ⇒ match eq_instrmode i hd with
107 | false ⇒ test_not_impl_mode i tl
111 (* su tutta la lista quante volte compare la coppia opcode,instr_mode *)
112 nlet rec get_OpIm_count (m:mcu_type) (o:any_opcode m) (i:instr_mode) (c:nat)
113 (l:list (Prod4T (any_opcode m) instr_mode byte8_or_word16 byte8)) on l ≝
117 match (eq_anyop m o (fst4T ???? hd)) ⊗
118 (eq_instrmode i (snd4T ???? hd)) with
119 [ true ⇒ get_OpIm_count m o i (S c) tl
120 | false ⇒ get_OpIm_count m o i c tl
124 (* iteratore sugli opcode *)
125 ndefinition forall_opcode ≝ λP.
126 P ADC ⊗ P ADD ⊗ P AIS ⊗ P AIX ⊗ P AND ⊗ P ASL ⊗ P ASR ⊗ P BCC ⊗
127 P BCLRn ⊗ P BCS ⊗ P BEQ ⊗ P BGE ⊗ P BGND ⊗ P BGT ⊗ P BHCC ⊗ P BHCS ⊗
128 P BHI ⊗ P BIH ⊗ P BIL ⊗ P BIT ⊗ P BLE ⊗ P BLS ⊗ P BLT ⊗ P BMC ⊗
129 P BMI ⊗ P BMS ⊗ P BNE ⊗ P BPL ⊗ P BRA ⊗ P BRCLRn ⊗ P BRN ⊗ P BRSETn ⊗
130 P BSETn ⊗ P BSR ⊗ P CBEQA ⊗ P CBEQX ⊗ P CLC ⊗ P CLI ⊗ P CLR ⊗ P CMP ⊗
131 P COM ⊗ P CPHX ⊗ P CPX ⊗ P DAA ⊗ P DBNZ ⊗ P DEC ⊗ P DIV ⊗ P EOR ⊗
132 P INC ⊗ P JMP ⊗ P JSR ⊗ P LDA ⊗ P LDHX ⊗ P LDX ⊗ P LSR ⊗ P MOV ⊗
133 P MUL ⊗ P NEG ⊗ P NOP ⊗ P NSA ⊗ P ORA ⊗ P PSHA ⊗ P PSHH ⊗ P PSHX ⊗
134 P PULA ⊗ P PULH ⊗ P PULX ⊗ P ROL ⊗ P ROR ⊗ P RSP ⊗ P RTI ⊗ P RTS ⊗
135 P SBC ⊗ P SEC ⊗ P SEI ⊗ P SHA ⊗ P SLA ⊗ P STA ⊗ P STHX ⊗ P STOP ⊗
136 P STX ⊗ P SUB ⊗ P SWI ⊗ P TAP ⊗ P TAX ⊗ P TPA ⊗ P TST ⊗ P TSX ⊗
137 P TXA ⊗ P TXS ⊗ P WAIT.
139 (* iteratore sulle modalita' *)
140 ndefinition forall_instr_mode ≝ λP.
161 ⊗ P MODE_DIR1_to_DIR1
162 ⊗ P MODE_IMM1_to_DIR1
163 ⊗ P MODE_IX0p_to_DIR1
164 ⊗ P MODE_DIR1_to_IX0p
166 ⊗ P MODE_INHA_and_IMM1
167 ⊗ P MODE_INHX_and_IMM1
168 ⊗ P MODE_IMM1_and_IMM1
169 ⊗ P MODE_DIR1_and_IMM1
170 ⊗ P MODE_IX0_and_IMM1
171 ⊗ P MODE_IX0p_and_IMM1
172 ⊗ P MODE_IX1_and_IMM1
173 ⊗ P MODE_IX1p_and_IMM1
174 ⊗ P MODE_SP1_and_IMM1
176 ⊗ forall_oct (λo. P (MODE_DIRn o))
177 ⊗ forall_oct (λo. P (MODE_DIRn_and_IMM1 o))
178 ⊗ forall_exadecim (λe. P (MODE_TNY e))
179 ⊗ forall_bitrigesim (λt. P (MODE_SRT t)).