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 *)
19 (* Cosimo Oliboni, oliboni@cs.unibo.it *)
21 (* Questo materiale fa parte della tesi: *)
22 (* "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale" *)
24 (* data ultima modifica 15/11/2007 *)
25 (* ********************************************************************** *)
27 include "freescale/opcode_base.ma".
29 (* ********************************************* *)
30 (* STRUMENTI PER LE DIMOSTRAZIONI DI CORRETTEZZA *)
31 (* ********************************************* *)
33 (* su tutta la lista quante volte compare il byte *)
34 nlet rec get_byte_count (m:mcu_type) (b:byte8) (c:nat)
35 (l:list (Prod4T (any_opcode m) instr_mode byte8_or_word16 byte8)) on l ≝
38 | cons hd tl ⇒ match thd4T ???? hd with
39 [ Byte b' ⇒ match eq_b8 b b' with
40 [ true ⇒ get_byte_count m b (S c) tl
41 | false ⇒ get_byte_count m b c tl
43 | Word _ ⇒ get_byte_count m b c tl
47 (* su tutta la lista quante volte compare la word (0x9E+byte) *)
48 nlet rec get_word_count (m:mcu_type) (b:byte8) (c:nat)
49 (l:list (Prod4T (any_opcode m) instr_mode byte8_or_word16 byte8)) on l ≝
52 | cons hd tl ⇒ match thd4T ???? hd with
53 [ Byte _ ⇒ get_word_count m b c tl
54 | Word w ⇒ match eq_w16 〈〈x9,xE〉:b〉 w with
55 [ true ⇒ get_word_count m b (S c) tl
56 | false ⇒ get_word_count m b c tl
61 (* su tutta la lista quante volte compare lo pseudocodice *)
62 nlet rec get_pseudo_count (m:mcu_type) (o:opcode) (c:nat)
63 (l:list (Prod4T (any_opcode m) instr_mode byte8_or_word16 byte8)) on l ≝
66 | cons hd tl ⇒ match fst4T ???? hd with
67 [ anyOP o' ⇒ match eq_op o o' with
68 [ true ⇒ get_pseudo_count m o (S c) tl
69 | false ⇒ get_pseudo_count m o c tl
74 (* su tutta la lista quante volte compare la modalita' *)
75 nlet rec get_mode_count (m:mcu_type) (i:instr_mode) (c:nat)
76 (l:list (Prod4T (any_opcode m) instr_mode byte8_or_word16 byte8)) on l ≝
79 | cons hd tl ⇒ match eq_instrmode (snd4T ???? hd) i with
80 [ true ⇒ get_mode_count m i (S c) tl
81 | false ⇒ get_mode_count m i c tl
85 (* b e' non implementato? *)
86 nlet rec test_not_impl_byte (b:byte8) (l:list byte8) on l ≝
89 | cons hd tl ⇒ match eq_b8 b hd with
91 | false ⇒ test_not_impl_byte b tl
95 (* o e' non implementato? *)
96 nlet rec test_not_impl_pseudo (o:opcode) (l:list opcode) on l ≝
99 | cons hd tl ⇒ match eq_op o hd with
101 | false ⇒ test_not_impl_pseudo o tl
105 (* i e' non implementato? *)
106 nlet rec test_not_impl_mode (i:instr_mode) (l:list instr_mode) on l ≝
109 | cons hd tl ⇒ match eq_instrmode i hd with
111 | false ⇒ test_not_impl_mode i tl
115 (* su tutta la lista quante volte compare la coppia opcode,instr_mode *)
116 nlet rec get_OpIm_count (m:mcu_type) (o:any_opcode m) (i:instr_mode) (c:nat)
117 (l:list (Prod4T (any_opcode m) instr_mode byte8_or_word16 byte8)) on l ≝
121 match (eq_anyop m o (fst4T ???? hd)) ⊗
122 (eq_instrmode i (snd4T ???? hd)) with
123 [ true ⇒ get_OpIm_count m o i (S c) tl
124 | false ⇒ get_OpIm_count m o i c tl
128 (* iteratore sugli opcode *)
129 ndefinition forall_opcode ≝ λP.
130 P ADC ⊗ P ADD ⊗ P AIS ⊗ P AIX ⊗ P AND ⊗ P ASL ⊗ P ASR ⊗ P BCC ⊗
131 P BCLRn ⊗ P BCS ⊗ P BEQ ⊗ P BGE ⊗ P BGND ⊗ P BGT ⊗ P BHCC ⊗ P BHCS ⊗
132 P BHI ⊗ P BIH ⊗ P BIL ⊗ P BIT ⊗ P BLE ⊗ P BLS ⊗ P BLT ⊗ P BMC ⊗
133 P BMI ⊗ P BMS ⊗ P BNE ⊗ P BPL ⊗ P BRA ⊗ P BRCLRn ⊗ P BRN ⊗ P BRSETn ⊗
134 P BSETn ⊗ P BSR ⊗ P CBEQA ⊗ P CBEQX ⊗ P CLC ⊗ P CLI ⊗ P CLR ⊗ P CMP ⊗
135 P COM ⊗ P CPHX ⊗ P CPX ⊗ P DAA ⊗ P DBNZ ⊗ P DEC ⊗ P DIV ⊗ P EOR ⊗
136 P INC ⊗ P JMP ⊗ P JSR ⊗ P LDA ⊗ P LDHX ⊗ P LDX ⊗ P LSR ⊗ P MOV ⊗
137 P MUL ⊗ P NEG ⊗ P NOP ⊗ P NSA ⊗ P ORA ⊗ P PSHA ⊗ P PSHH ⊗ P PSHX ⊗
138 P PULA ⊗ P PULH ⊗ P PULX ⊗ P ROL ⊗ P ROR ⊗ P RSP ⊗ P RTI ⊗ P RTS ⊗
139 P SBC ⊗ P SEC ⊗ P SEI ⊗ P SHA ⊗ P SLA ⊗ P STA ⊗ P STHX ⊗ P STOP ⊗
140 P STX ⊗ P SUB ⊗ P SWI ⊗ P TAP ⊗ P TAX ⊗ P TPA ⊗ P TST ⊗ P TSX ⊗
141 P TXA ⊗ P TXS ⊗ P WAIT.
143 (* iteratore sulle modalita' *)
144 ndefinition forall_instr_mode ≝ λP.
165 ⊗ P MODE_DIR1_to_DIR1
166 ⊗ P MODE_IMM1_to_DIR1
167 ⊗ P MODE_IX0p_to_DIR1
168 ⊗ P MODE_DIR1_to_IX0p
170 ⊗ P MODE_INHA_and_IMM1
171 ⊗ P MODE_INHX_and_IMM1
172 ⊗ P MODE_IMM1_and_IMM1
173 ⊗ P MODE_DIR1_and_IMM1
174 ⊗ P MODE_IX0_and_IMM1
175 ⊗ P MODE_IX0p_and_IMM1
176 ⊗ P MODE_IX1_and_IMM1
177 ⊗ P MODE_IX1p_and_IMM1
178 ⊗ P MODE_SP1_and_IMM1
180 ⊗ forall_oct (λo. P (MODE_DIRn o))
181 ⊗ forall_oct (λo. P (MODE_DIRn_and_IMM1 o))
182 ⊗ forall_exadecim (λe. P (MODE_TNY e))
183 ⊗ forall_bitrigesim (λt. P (MODE_SRT t)).