--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(* Progetto FreeScale *)
+(* *)
+(* Sviluppato da: *)
+(* Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* *)
+(* Questo materiale fa parte della tesi: *)
+(* "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale" *)
+(* *)
+(* data ultima modifica 15/11/2007 *)
+(* ********************************************************************** *)
+
+include "freescale/opcode_base.ma".
+
+(* ********************************************* *)
+(* STRUMENTI PER LE DIMOSTRAZIONI DI CORRETTEZZA *)
+(* ********************************************* *)
+
+(* su tutta la lista quante volte compare il byte *)
+nlet rec get_byte_count (m:mcu_type) (b:byte8) (c:nat)
+ (l:list (Prod4T (any_opcode m) instr_mode byte8_or_word16 byte8)) on l ≝
+ match l with
+ [ nil ⇒ c
+ | cons hd tl ⇒ match thd4T ???? hd with
+ [ Byte b' ⇒ match eq_b8 b b' with
+ [ true ⇒ get_byte_count m b (S c) tl
+ | false ⇒ get_byte_count m b c tl
+ ]
+ | Word _ ⇒ get_byte_count m b c tl
+ ]
+ ].
+
+(* su tutta la lista quante volte compare la word (0x9E+byte) *)
+nlet rec get_word_count (m:mcu_type) (b:byte8) (c:nat)
+ (l:list (Prod4T (any_opcode m) instr_mode byte8_or_word16 byte8)) on l ≝
+ match l with
+ [ nil ⇒ c
+ | cons hd tl ⇒ match thd4T ???? hd with
+ [ Byte _ ⇒ get_word_count m b c tl
+ | Word w ⇒ match eq_w16 〈〈x9,xE〉:b〉 w with
+ [ true ⇒ get_word_count m b (S c) tl
+ | false ⇒ get_word_count m b c tl
+ ]
+ ]
+ ].
+
+(* su tutta la lista quante volte compare lo pseudocodice *)
+nlet rec get_pseudo_count (m:mcu_type) (o:opcode) (c:nat)
+ (l:list (Prod4T (any_opcode m) instr_mode byte8_or_word16 byte8)) on l ≝
+ match l with
+ [ nil ⇒ c
+ | cons hd tl ⇒ match fst4T ???? hd with
+ [ anyOP o' ⇒ match eq_op o o' with
+ [ true ⇒ get_pseudo_count m o (S c) tl
+ | false ⇒ get_pseudo_count m o c tl
+ ]
+ ]
+ ].
+
+(* su tutta la lista quante volte compare la modalita' *)
+nlet rec get_mode_count (m:mcu_type) (i:instr_mode) (c:nat)
+ (l:list (Prod4T (any_opcode m) instr_mode byte8_or_word16 byte8)) on l ≝
+ match l with
+ [ nil ⇒ c
+ | cons hd tl ⇒ match eq_instrmode (snd4T ???? hd) i with
+ [ true ⇒ get_mode_count m i (S c) tl
+ | false ⇒ get_mode_count m i c tl
+ ]
+ ].
+
+(* b e' non implementato? *)
+nlet rec test_not_impl_byte (b:byte8) (l:list byte8) on l ≝
+ match l with
+ [ nil ⇒ false
+ | cons hd tl ⇒ match eq_b8 b hd with
+ [ true ⇒ true
+ | false ⇒ test_not_impl_byte b tl
+ ]
+ ].
+
+(* o e' non implementato? *)
+nlet rec test_not_impl_pseudo (o:opcode) (l:list opcode) on l ≝
+ match l with
+ [ nil ⇒ false
+ | cons hd tl ⇒ match eq_op o hd with
+ [ true ⇒ true
+ | false ⇒ test_not_impl_pseudo o tl
+ ]
+ ].
+
+(* i e' non implementato? *)
+nlet rec test_not_impl_mode (i:instr_mode) (l:list instr_mode) on l ≝
+ match l with
+ [ nil ⇒ false
+ | cons hd tl ⇒ match eq_instrmode i hd with
+ [ true ⇒ true
+ | false ⇒ test_not_impl_mode i tl
+ ]
+ ].
+
+(* su tutta la lista quante volte compare la coppia opcode,instr_mode *)
+nlet rec get_OpIm_count (m:mcu_type) (o:any_opcode m) (i:instr_mode) (c:nat)
+ (l:list (Prod4T (any_opcode m) instr_mode byte8_or_word16 byte8)) on l ≝
+ match l with
+ [ nil ⇒ c
+ | cons hd tl ⇒
+ match (eq_anyop m o (fst4T ???? hd)) ⊗
+ (eq_instrmode i (snd4T ???? hd)) with
+ [ true ⇒ get_OpIm_count m o i (S c) tl
+ | false ⇒ get_OpIm_count m o i c tl
+ ]
+ ].
+
+(* iteratore sugli opcode *)
+ndefinition forall_opcode ≝ λP.
+ P ADC ⊗ P ADD ⊗ P AIS ⊗ P AIX ⊗ P AND ⊗ P ASL ⊗ P ASR ⊗ P BCC ⊗
+ P BCLRn ⊗ P BCS ⊗ P BEQ ⊗ P BGE ⊗ P BGND ⊗ P BGT ⊗ P BHCC ⊗ P BHCS ⊗
+ P BHI ⊗ P BIH ⊗ P BIL ⊗ P BIT ⊗ P BLE ⊗ P BLS ⊗ P BLT ⊗ P BMC ⊗
+ P BMI ⊗ P BMS ⊗ P BNE ⊗ P BPL ⊗ P BRA ⊗ P BRCLRn ⊗ P BRN ⊗ P BRSETn ⊗
+ P BSETn ⊗ P BSR ⊗ P CBEQA ⊗ P CBEQX ⊗ P CLC ⊗ P CLI ⊗ P CLR ⊗ P CMP ⊗
+ P COM ⊗ P CPHX ⊗ P CPX ⊗ P DAA ⊗ P DBNZ ⊗ P DEC ⊗ P DIV ⊗ P EOR ⊗
+ P INC ⊗ P JMP ⊗ P JSR ⊗ P LDA ⊗ P LDHX ⊗ P LDX ⊗ P LSR ⊗ P MOV ⊗
+ P MUL ⊗ P NEG ⊗ P NOP ⊗ P NSA ⊗ P ORA ⊗ P PSHA ⊗ P PSHH ⊗ P PSHX ⊗
+ P PULA ⊗ P PULH ⊗ P PULX ⊗ P ROL ⊗ P ROR ⊗ P RSP ⊗ P RTI ⊗ P RTS ⊗
+ P SBC ⊗ P SEC ⊗ P SEI ⊗ P SHA ⊗ P SLA ⊗ P STA ⊗ P STHX ⊗ P STOP ⊗
+ P STX ⊗ P SUB ⊗ P SWI ⊗ P TAP ⊗ P TAX ⊗ P TPA ⊗ P TST ⊗ P TSX ⊗
+ P TXA ⊗ P TXS ⊗ P WAIT.
+
+(* iteratore sulle modalita' *)
+ndefinition forall_instr_mode ≝ λP.
+ P MODE_INH
+⊗ P MODE_INHA
+⊗ P MODE_INHX
+⊗ P MODE_INHH
+
+⊗ P MODE_INHX0ADD
+⊗ P MODE_INHX1ADD
+⊗ P MODE_INHX2ADD
+
+⊗ P MODE_IMM1
+⊗ P MODE_IMM1EXT
+⊗ P MODE_IMM2
+⊗ P MODE_DIR1
+⊗ P MODE_DIR2
+⊗ P MODE_IX0
+⊗ P MODE_IX1
+⊗ P MODE_IX2
+⊗ P MODE_SP1
+⊗ P MODE_SP2
+
+⊗ P MODE_DIR1_to_DIR1
+⊗ P MODE_IMM1_to_DIR1
+⊗ P MODE_IX0p_to_DIR1
+⊗ P MODE_DIR1_to_IX0p
+
+⊗ P MODE_INHA_and_IMM1
+⊗ P MODE_INHX_and_IMM1
+⊗ P MODE_IMM1_and_IMM1
+⊗ P MODE_DIR1_and_IMM1
+⊗ P MODE_IX0_and_IMM1
+⊗ P MODE_IX0p_and_IMM1
+⊗ P MODE_IX1_and_IMM1
+⊗ P MODE_IX1p_and_IMM1
+⊗ P MODE_SP1_and_IMM1
+
+⊗ forall_oct (λo. P (MODE_DIRn o))
+⊗ forall_oct (λo. P (MODE_DIRn_and_IMM1 o))
+⊗ forall_exadecim (λe. P (MODE_TNY e))
+⊗ forall_bitrigesim (λt. P (MODE_SRT t)).
projects / helm.git / blobdiff