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 (* Sviluppo: 2008-2010 *)
21 (* ********************************************************************** *)
23 include "num/bool.ma".
25 (* ********************************************** *)
26 (* MATTONI BASE PER DEFINIRE LE TABELLE DELLE MCU *)
27 (* ********************************************** *)
29 (* enumerazione delle istruzioni *)
30 ninductive IP2022_opcode: Type ≝
31 ADD : IP2022_opcode (* add *)
32 | ADDC : IP2022_opcode (* add with carry *)
33 | AND : IP2022_opcode (* and *)
34 | BREAK : IP2022_opcode (* enter break mode *)
35 | BREAKX : IP2022_opcode (* enter break mode, after skip *)
36 | CALL : IP2022_opcode (* subroutine call *)
37 | CLR : IP2022_opcode (* clear *)
38 | CLRB : IP2022_opcode (* clear bit *)
39 | CMP : IP2022_opcode (* set flags according to sub *)
40 | CSE : IP2022_opcode (* confront & skip if equal *)
41 | CSNE : IP2022_opcode (* confront & skip if not equal *)
42 | CWDT : IP2022_opcode (* clear watch dog -- not impl. ERR *)
43 | DEC : IP2022_opcode (* decrement *)
44 | DECSNZ : IP2022_opcode (* decrement & skip if not zero *)
45 | DECSZ : IP2022_opcode (* decrement & skip if zero *)
46 | FERASE : IP2022_opcode (* flash erase -- not impl. ERR *)
47 | FREAD : IP2022_opcode (* flash read -- not impl. ERR *)
48 | FWRITE : IP2022_opcode (* flash write -- not impl. ERR *)
49 | INC : IP2022_opcode (* increment *)
50 | INCSNZ : IP2022_opcode (* increment & skip if not zero *)
51 | INCSZ : IP2022_opcode (* increment & skip if zero *)
52 | INT : IP2022_opcode (* interrupt -- not impl. ERR *)
53 | IREAD : IP2022_opcode (* memory read *)
54 | IREADI : IP2022_opcode (* memory read & inc *)
55 | IWRITE : IP2022_opcode (* memory write *)
56 | IWRITEI : IP2022_opcode (* memory write & inc *)
57 | JMP : IP2022_opcode (* jump *)
58 | LOADH : IP2022_opcode (* load Data Pointer High *)
59 | LOADL : IP2022_opcode (* load Data Pointer Low *)
60 | MOV : IP2022_opcode (* move *)
61 | MULS : IP2022_opcode (* signed mul *)
62 | MULU : IP2022_opcode (* unsigned mul *)
63 | NOP : IP2022_opcode (* nop *)
64 | NOT : IP2022_opcode (* not *)
65 | OR : IP2022_opcode (* or *)
66 | PAGE : IP2022_opcode (* set Page Register *)
67 | POP : IP2022_opcode (* pop *)
68 | PUSH : IP2022_opcode (* push *)
69 | RET : IP2022_opcode (* subroutine ret *)
70 | RETI : IP2022_opcode (* interrupt ret -- not impl. ERR *)
71 | RETNP : IP2022_opcode (* subroutine ret & don't restore Page Register *)
72 | RETW : IP2022_opcode (* subroutine ret & load W Register *)
73 | RL : IP2022_opcode (* rotate left *)
74 | RR : IP2022_opcode (* rotate right *)
75 | SB : IP2022_opcode (* skip if bit set *)
76 | SETB : IP2022_opcode (* set bit *)
77 | SNB : IP2022_opcode (* skip if bit not set *)
78 | SPEED : IP2022_opcode (* set Speed Register *)
79 | SUB : IP2022_opcode (* sub *)
80 | SUBC : IP2022_opcode (* sub with carry *)
81 | SWAP : IP2022_opcode (* swap xxxxyyyy → yyyyxxxx *)
82 | TEST : IP2022_opcode (* set flags according to zero test *)
83 | XOR : IP2022_opcode (* xor *)
86 ndefinition eq_IP2022_op ≝
87 λop1,op2:IP2022_opcode.
89 [ ADD ⇒ match op2 with [ ADD ⇒ true | _ ⇒ false ] | ADDC ⇒ match op2 with [ ADDC ⇒ true | _ ⇒ false ]
90 | AND ⇒ match op2 with [ AND ⇒ true | _ ⇒ false ] | BREAK ⇒ match op2 with [ BREAK ⇒ true | _ ⇒ false ]
91 | BREAKX ⇒ match op2 with [ BREAKX ⇒ true | _ ⇒ false ] | CALL ⇒ match op2 with [ CALL ⇒ true | _ ⇒ false ]
92 | CLR ⇒ match op2 with [ CLR ⇒ true | _ ⇒ false ] | CLRB ⇒ match op2 with [ CLRB ⇒ true | _ ⇒ false ]
93 | CMP ⇒ match op2 with [ CMP ⇒ true | _ ⇒ false ] | CSE ⇒ match op2 with [ CSE ⇒ true | _ ⇒ false ]
94 | CSNE ⇒ match op2 with [ CSNE ⇒ true | _ ⇒ false ] | CWDT ⇒ match op2 with [ CWDT ⇒ true | _ ⇒ false ]
95 | DEC ⇒ match op2 with [ DEC ⇒ true | _ ⇒ false ] | DECSNZ ⇒ match op2 with [ DECSNZ ⇒ true | _ ⇒ false ]
96 | DECSZ ⇒ match op2 with [ DECSZ ⇒ true | _ ⇒ false ] | FERASE ⇒ match op2 with [ FERASE ⇒ true | _ ⇒ false ]
97 | FREAD ⇒ match op2 with [ FREAD ⇒ true | _ ⇒ false ] | FWRITE ⇒ match op2 with [ FWRITE ⇒ true | _ ⇒ false ]
98 | INC ⇒ match op2 with [ INC ⇒ true | _ ⇒ false ] | INCSNZ ⇒ match op2 with [ INCSNZ ⇒ true | _ ⇒ false ]
99 | INCSZ ⇒ match op2 with [ INCSZ ⇒ true | _ ⇒ false ] | INT ⇒ match op2 with [ INT ⇒ true | _ ⇒ false ]
100 | IREAD ⇒ match op2 with [ IREAD ⇒ true | _ ⇒ false ] | IREADI ⇒ match op2 with [ IREADI ⇒ true | _ ⇒ false ]
101 | IWRITE ⇒ match op2 with [ IWRITE ⇒ true | _ ⇒ false ] | IWRITEI ⇒ match op2 with [ IWRITEI ⇒ true | _ ⇒ false ]
102 | JMP ⇒ match op2 with [ JMP ⇒ true | _ ⇒ false ] | LOADH ⇒ match op2 with [ LOADH ⇒ true | _ ⇒ false ]
103 | LOADL ⇒ match op2 with [ LOADL ⇒ true | _ ⇒ false ] | MOV ⇒ match op2 with [ MOV ⇒ true | _ ⇒ false ]
104 | MULS ⇒ match op2 with [ MULS ⇒ true | _ ⇒ false ] | MULU ⇒ match op2 with [ MULU ⇒ true | _ ⇒ false ]
105 | NOP ⇒ match op2 with [ NOP ⇒ true | _ ⇒ false ] | NOT ⇒ match op2 with [ NOT ⇒ true | _ ⇒ false ]
106 | OR ⇒ match op2 with [ OR ⇒ true | _ ⇒ false ] | PAGE ⇒ match op2 with [ PAGE ⇒ true | _ ⇒ false ]
107 | POP ⇒ match op2 with [ POP ⇒ true | _ ⇒ false ] | PUSH ⇒ match op2 with [ PUSH ⇒ true | _ ⇒ false ]
108 | RET ⇒ match op2 with [ RET ⇒ true | _ ⇒ false ] | RETI ⇒ match op2 with [ RETI ⇒ true | _ ⇒ false ]
109 | RETNP ⇒ match op2 with [ RETNP ⇒ true | _ ⇒ false ] | RETW ⇒ match op2 with [ RETW ⇒ true | _ ⇒ false ]
110 | RL ⇒ match op2 with [ RL ⇒ true | _ ⇒ false ] | RR ⇒ match op2 with [ RR ⇒ true | _ ⇒ false ]
111 | SB ⇒ match op2 with [ SB ⇒ true | _ ⇒ false ] | SETB ⇒ match op2 with [ SETB ⇒ true | _ ⇒ false ]
112 | SNB ⇒ match op2 with [ SNB ⇒ true | _ ⇒ false ] | SPEED ⇒ match op2 with [ SPEED ⇒ true | _ ⇒ false ]
113 | SUB ⇒ match op2 with [ SUB ⇒ true | _ ⇒ false ] | SUBC ⇒ match op2 with [ SUBC ⇒ true | _ ⇒ false ]
114 | SWAP ⇒ match op2 with [ SWAP ⇒ true | _ ⇒ false ] | TEST ⇒ match op2 with [ TEST ⇒ true | _ ⇒ false ]
115 | XOR ⇒ match op2 with [ XOR ⇒ true | _ ⇒ false ]
118 (* iteratore sugli opcode *)
119 ndefinition forall_IP2022_op ≝ λP:IP2022_opcode → bool.
120 P ADD ⊗ P ADDC ⊗ P AND ⊗ P BREAK ⊗ P BREAKX ⊗ P CALL ⊗ P CLR ⊗ P CLRB ⊗
121 P CMP ⊗ P CSE ⊗ P CSNE ⊗ P CWDT ⊗ P DEC ⊗ P DECSNZ ⊗ P DECSZ ⊗ P FERASE ⊗
122 P FREAD ⊗ P FWRITE ⊗ P INC ⊗ P INCSNZ ⊗ P INCSZ ⊗ P INT ⊗ P IREAD ⊗ P IREADI ⊗
123 P IWRITE ⊗ P IWRITEI ⊗ P JMP ⊗ P LOADH ⊗ P LOADL ⊗ P MOV ⊗ P MULS ⊗ P MULU ⊗
124 P NOP ⊗ P NOT ⊗ P OR ⊗ P PAGE ⊗ P POP ⊗ P PUSH ⊗ P RET ⊗ P RETI ⊗
125 P RETNP ⊗ P RETW ⊗ P RL ⊗ P RR ⊗ P SB ⊗ P SETB ⊗ P SNB ⊗ P SPEED ⊗
126 P SUB ⊗ P SUBC ⊗ P SWAP ⊗ P TEST ⊗ P XOR.