]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/library/freescale/table_HC08_tests.ma
An unimplemented case of clearbody is now implemented.
[helm.git] / helm / software / matita / library / freescale / table_HC08_tests.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 (* ********************************************************************** *)
16 (*                           Progetto FreeScale                           *)
17 (*                                                                        *)
18 (* Sviluppato da:                                                         *)
19 (*   Cosimo Oliboni, oliboni@cs.unibo.it                                  *)
20 (*                                                                        *)
21 (* Questo materiale fa parte della tesi:                                  *)
22 (*   "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale"   *)
23 (*                                                                        *)
24 (*                    data ultima modifica 15/11/2007                     *)
25 (* ********************************************************************** *)
26
27 include "freescale/table_HC08.ma".
28
29 (* CORRETTEZZA *)
30
31 (* HC08: opcode non implementati come da manuale (byte) *)
32 definition HC08_not_impl_byte ≝
33  [〈x3,x2〉;〈x3,xE〉
34  ;〈x8,x2〉;〈x8,xD〉
35  ;〈x9,x6〉;〈x9,xE〉
36  ;〈xA,xC〉
37  ].
38
39 lemma ok_byte_table_HC08 : forall_byte8 (λb.
40  (test_not_impl_byte b HC08_not_impl_byte     ⊙ eqb (get_byte_count HC08 b 0 opcode_table_HC08) 1) ⊗
41  (⊖ (test_not_impl_byte b HC08_not_impl_byte) ⊙ eqb (get_byte_count HC08 b 0 opcode_table_HC08) 0))
42  = true.
43  reflexivity.
44 qed.
45
46 (* HC08: opcode non implementati come da manuale (0x9E+byte) *)
47 definition HC08_not_impl_word ≝
48  [〈x0,x0〉;〈x0,x1〉;〈x0,x2〉;〈x0,x3〉;〈x0,x4〉;〈x0,x5〉;〈x0,x6〉;〈x0,x7〉
49  ;〈x0,x8〉;〈x0,x9〉;〈x0,xA〉;〈x0,xB〉;〈x0,xC〉;〈x0,xD〉;〈x0,xE〉;〈x0,xF〉
50  ;〈x1,x0〉;〈x1,x1〉;〈x1,x2〉;〈x1,x3〉;〈x1,x4〉;〈x1,x5〉;〈x1,x6〉;〈x1,x7〉
51  ;〈x1,x8〉;〈x1,x9〉;〈x1,xA〉;〈x1,xB〉;〈x1,xC〉;〈x1,xD〉;〈x1,xE〉;〈x1,xF〉
52  ;〈x2,x0〉;〈x2,x1〉;〈x2,x2〉;〈x2,x3〉;〈x2,x4〉;〈x2,x5〉;〈x2,x6〉;〈x2,x7〉
53  ;〈x2,x8〉;〈x2,x9〉;〈x2,xA〉;〈x2,xB〉;〈x2,xC〉;〈x2,xD〉;〈x2,xE〉;〈x2,xF〉
54  ;〈x3,x0〉;〈x3,x1〉;〈x3,x2〉;〈x3,x3〉;〈x3,x4〉;〈x3,x5〉;〈x3,x6〉;〈x3,x7〉
55  ;〈x3,x8〉;〈x3,x9〉;〈x3,xA〉;〈x3,xB〉;〈x3,xC〉;〈x3,xD〉;〈x3,xE〉;〈x3,xF〉
56  ;〈x4,x0〉;〈x4,x1〉;〈x4,x2〉;〈x4,x3〉;〈x4,x4〉;〈x4,x5〉;〈x4,x6〉;〈x4,x7〉
57  ;〈x4,x8〉;〈x4,x9〉;〈x4,xA〉;〈x4,xB〉;〈x4,xC〉;〈x4,xD〉;〈x4,xE〉;〈x4,xF〉
58  ;〈x5,x0〉;〈x5,x1〉;〈x5,x2〉;〈x5,x3〉;〈x5,x4〉;〈x5,x5〉;〈x5,x6〉;〈x5,x7〉
59  ;〈x5,x8〉;〈x5,x9〉;〈x5,xA〉;〈x5,xB〉;〈x5,xC〉;〈x5,xD〉;〈x5,xE〉;〈x5,xF〉
60  ;〈x6,x2〉;〈x6,x5〉;〈x6,xE〉
61  ;〈x7,x0〉;〈x7,x1〉;〈x7,x2〉;〈x7,x3〉;〈x7,x4〉;〈x7,x5〉;〈x7,x6〉;〈x7,x7〉
62  ;〈x7,x8〉;〈x7,x9〉;〈x7,xA〉;〈x7,xB〉;〈x7,xC〉;〈x7,xD〉;〈x7,xE〉;〈x7,xF〉
63  ;〈x8,x0〉;〈x8,x1〉;〈x8,x2〉;〈x8,x3〉;〈x8,x4〉;〈x8,x5〉;〈x8,x6〉;〈x8,x7〉
64  ;〈x8,x8〉;〈x8,x9〉;〈x8,xA〉;〈x8,xB〉;〈x8,xC〉;〈x8,xD〉;〈x8,xE〉;〈x8,xF〉
65  ;〈x9,x0〉;〈x9,x1〉;〈x9,x2〉;〈x9,x3〉;〈x9,x4〉;〈x9,x5〉;〈x9,x6〉;〈x9,x7〉
66  ;〈x9,x8〉;〈x9,x9〉;〈x9,xA〉;〈x9,xB〉;〈x9,xC〉;〈x9,xD〉;〈x9,xE〉;〈x9,xF〉
67  ;〈xA,x0〉;〈xA,x1〉;〈xA,x2〉;〈xA,x3〉;〈xA,x4〉;〈xA,x5〉;〈xA,x6〉;〈xA,x7〉
68  ;〈xA,x8〉;〈xA,x9〉;〈xA,xA〉;〈xA,xB〉;〈xA,xC〉;〈xA,xD〉;〈xA,xE〉;〈xA,xF〉
69  ;〈xB,x0〉;〈xB,x1〉;〈xB,x2〉;〈xB,x3〉;〈xB,x4〉;〈xB,x5〉;〈xB,x6〉;〈xB,x7〉
70  ;〈xB,x8〉;〈xB,x9〉;〈xB,xA〉;〈xB,xB〉;〈xB,xC〉;〈xB,xD〉;〈xB,xE〉;〈xB,xF〉
71  ;〈xC,x0〉;〈xC,x1〉;〈xC,x2〉;〈xC,x3〉;〈xC,x4〉;〈xC,x5〉;〈xC,x6〉;〈xC,x7〉
72  ;〈xC,x8〉;〈xC,x9〉;〈xC,xA〉;〈xC,xB〉;〈xC,xC〉;〈xC,xD〉;〈xC,xE〉;〈xC,xF〉
73  ;〈xD,xC〉;〈xD,xD〉
74  ;〈xE,xC〉;〈xE,xD〉
75  ;〈xF,x0〉;〈xF,x1〉;〈xF,x2〉;〈xF,x3〉;〈xF,x4〉;〈xF,x5〉;〈xF,x6〉;〈xF,x7〉
76  ;〈xF,x8〉;〈xF,x9〉;〈xF,xA〉;〈xF,xB〉;〈xF,xC〉;〈xF,xD〉;〈xF,xE〉;〈xF,xF〉
77  ].
78
79 lemma ok_word_table_HC08 : forall_byte8 (λb.
80  (test_not_impl_byte b HC08_not_impl_word     ⊙ eqb (get_word_count HC08 b 0 opcode_table_HC08) 1) ⊗
81  (⊖ (test_not_impl_byte b HC08_not_impl_word) ⊙ eqb (get_word_count HC08 b 0 opcode_table_HC08) 0))
82  = true.
83  reflexivity.
84 qed.
85
86 (* HC08: pseudocodici non implementati come da manuale *)
87 definition HC08_not_impl_pseudo ≝
88  [ BGND ; SHA ; SLA ].
89
90 lemma ok_pseudo_table_HC08 : forall_opcode (λo.
91  (test_not_impl_pseudo o HC08_not_impl_pseudo     ⊙ leb 1 (get_pseudo_count HC08 o 0 opcode_table_HC08)) ⊗
92  (⊖ (test_not_impl_pseudo o HC08_not_impl_pseudo) ⊙ eqb (get_pseudo_count HC08 o 0 opcode_table_HC08) 0))
93  = true.
94  reflexivity.
95 qed.
96
97 (* HC08: modalita' non implementate come da manuale *)
98 definition HC08_not_impl_mode ≝
99  [ MODE_TNY x0 ; MODE_TNY x1 ; MODE_TNY x2 ; MODE_TNY x3
100  ; MODE_TNY x4 ; MODE_TNY x5 ; MODE_TNY x6 ; MODE_TNY x7
101  ; MODE_TNY x8 ; MODE_TNY x9 ; MODE_TNY xA ; MODE_TNY xB
102  ; MODE_TNY xC ; MODE_TNY xD ; MODE_TNY xE ; MODE_TNY xF
103  ; MODE_SRT t00 ; MODE_SRT t01 ; MODE_SRT t02 ; MODE_SRT t03
104  ; MODE_SRT t04 ; MODE_SRT t05 ; MODE_SRT t06 ; MODE_SRT t07
105  ; MODE_SRT t08 ; MODE_SRT t09 ; MODE_SRT t0A ; MODE_SRT t0B
106  ; MODE_SRT t0C ; MODE_SRT t0D ; MODE_SRT t0E ; MODE_SRT t0F
107  ; MODE_SRT t10 ; MODE_SRT t11 ; MODE_SRT t12 ; MODE_SRT t13
108  ; MODE_SRT t14 ; MODE_SRT t15 ; MODE_SRT t16 ; MODE_SRT t17
109  ; MODE_SRT t18 ; MODE_SRT t19 ; MODE_SRT t1A ; MODE_SRT t1B
110  ; MODE_SRT t1C ; MODE_SRT t1D ; MODE_SRT t1E ; MODE_SRT t1F ].
111
112 lemma ok_mode_table_HC08 : forall_instr_mode (λi.
113  (test_not_impl_mode i HC08_not_impl_mode     ⊙ leb 1 (get_mode_count HC08 i 0 opcode_table_HC08)) ⊗
114  (⊖ (test_not_impl_mode i HC08_not_impl_mode) ⊙ eqb (get_mode_count HC08 i 0 opcode_table_HC08) 0))
115  = true.
116  reflexivity.
117 qed.
118
119 lemma ok_OpIm_table_HC08 :
120  forall_instr_mode (λi:instr_mode.
121  forall_opcode     (λop:opcode.
122   leb (get_OpIm_count HC08 (anyOP HC08 op) i 0 opcode_table_HC08) 1)) = true.
123  reflexivity.
124 qed.
125