source: Deliverables/D3.3/id-lookup-branch/ASM/ASM.ma @ 3033

Last change on this file since 3033 was 1153, checked in by campbell, 8 years ago

Merge trunk into branch.

File size: 8.7 KB
Line 
1include "ASM/BitVector.ma".
2
3definition Identifier ≝ Word.
4
5inductive addressing_mode: Type[0] ≝
6  DIRECT: Byte → addressing_mode
7| INDIRECT: Bit → addressing_mode
8| EXT_INDIRECT: Bit → addressing_mode
9| REGISTER: BitVector 3 → addressing_mode
10| ACC_A: addressing_mode
11| ACC_B: addressing_mode
12| DPTR: addressing_mode
13| DATA: Byte → addressing_mode
14| DATA16: Word → addressing_mode
15| ACC_DPTR: addressing_mode
16| ACC_PC: addressing_mode
17| EXT_INDIRECT_DPTR: addressing_mode
18| INDIRECT_DPTR: addressing_mode
19| CARRY: addressing_mode
20| BIT_ADDR: Byte → addressing_mode
21| N_BIT_ADDR: Byte → addressing_mode
22| RELATIVE: Byte → addressing_mode
23| ADDR11: Word11 → addressing_mode
24| ADDR16: Word → addressing_mode.
25
26(* dpm: renamed register to registr to avoid clash with brian's types *)
27inductive addressing_mode_tag : Type[0] ≝
28  direct: addressing_mode_tag
29| indirect: addressing_mode_tag
30| ext_indirect: addressing_mode_tag
31| registr: addressing_mode_tag
32| acc_a: addressing_mode_tag
33| acc_b: addressing_mode_tag
34| dptr: addressing_mode_tag
35| data: addressing_mode_tag
36| data16: addressing_mode_tag
37| acc_dptr: addressing_mode_tag
38| acc_pc: addressing_mode_tag
39| ext_indirect_dptr: addressing_mode_tag
40| indirect_dptr: addressing_mode_tag
41| carry: addressing_mode_tag
42| bit_addr: addressing_mode_tag
43| n_bit_addr: addressing_mode_tag
44| relative: addressing_mode_tag
45| addr11: addressing_mode_tag
46| addr16: addressing_mode_tag.
47
48definition eq_a ≝
49  λa, b: addressing_mode_tag.
50    match a with
51      [ direct ⇒ match b with [ direct ⇒ true | _ ⇒ false ]
52      | indirect ⇒ match b with [ indirect ⇒ true | _ ⇒ false ]
53      | ext_indirect ⇒ match b with [ ext_indirect ⇒ true | _ ⇒ false ]
54      | registr ⇒ match b with [ registr ⇒ true | _ ⇒ false ]
55      | acc_a ⇒ match b with [ acc_a ⇒ true | _ ⇒ false ]
56      | acc_b ⇒ match b with [ acc_b ⇒ true | _ ⇒ false ]
57      | dptr ⇒ match b with [ dptr ⇒ true | _ ⇒ false ]
58      | data ⇒ match b with [ data ⇒ true | _ ⇒ false ]
59      | data16 ⇒ match b with [ data16 ⇒ true | _ ⇒ false ]
60      | acc_dptr ⇒ match b with [ acc_dptr ⇒ true | _ ⇒ false ]
61      | acc_pc ⇒ match b with [ acc_pc ⇒ true | _ ⇒ false ]
62      | ext_indirect_dptr ⇒ match b with [ ext_indirect_dptr ⇒ true | _ ⇒ false ]
63      | indirect_dptr ⇒ match b with [ indirect_dptr ⇒ true | _ ⇒ false ]
64      | carry ⇒ match b with [ carry ⇒ true | _ ⇒ false ]
65      | bit_addr ⇒ match b with [ bit_addr ⇒ true | _ ⇒ false ]
66      | n_bit_addr ⇒ match b with [ n_bit_addr ⇒ true | _ ⇒ false ]
67      | relative ⇒ match b with [ relative ⇒ true | _ ⇒ false ]
68      | addr11 ⇒ match b with [ addr11 ⇒ true | _ ⇒ false ]
69      | addr16 ⇒ match b with [ addr16 ⇒ true | _ ⇒ false ]
70      ].
71
72(* to avoid expansion... *)
73let rec is_a (d:addressing_mode_tag) (A:addressing_mode) on d ≝
74  match d with
75   [ direct ⇒ match A with [ DIRECT _ ⇒ true | _ ⇒ false ]
76   | indirect ⇒ match A with [ INDIRECT _ ⇒ true | _ ⇒ false ]
77   | ext_indirect ⇒ match A with [ EXT_INDIRECT _ ⇒ true | _ ⇒ false ]
78   | registr ⇒ match A with [ REGISTER _ ⇒ true | _ ⇒ false ]
79   | acc_a ⇒ match A with [ ACC_A ⇒ true | _ ⇒ false ]
80   | acc_b ⇒ match A with [ ACC_B ⇒ true | _ ⇒ false ]
81   | dptr ⇒ match A with [ DPTR ⇒ true | _ ⇒ false ]
82   | data ⇒ match A with [ DATA _ ⇒ true | _ ⇒ false ]
83   | data16 ⇒ match A with [ DATA16 _ ⇒ true | _ ⇒ false ]
84   | acc_dptr ⇒ match A with [ ACC_DPTR ⇒ true | _ ⇒ false ]
85   | acc_pc ⇒ match A with [ ACC_PC ⇒ true | _ ⇒ false ]
86   | ext_indirect_dptr ⇒ match A with [ EXT_INDIRECT_DPTR ⇒ true | _ ⇒ false ]
87   | indirect_dptr ⇒ match A with [ INDIRECT_DPTR ⇒ true | _ ⇒ false ]
88   | carry ⇒ match A with [ CARRY ⇒ true | _ ⇒ false ]
89   | bit_addr ⇒ match A with [ BIT_ADDR _ ⇒ true | _ ⇒ false ]
90   | n_bit_addr ⇒ match A with [ N_BIT_ADDR _ ⇒ true | _ ⇒ false ]
91   | relative ⇒ match A with [ RELATIVE _ ⇒ true | _ ⇒ false ]
92   | addr11 ⇒ match A with [ ADDR11 _ ⇒ true | _ ⇒ false ]
93   | addr16 ⇒ match A with [ ADDR16 _ ⇒ true | _ ⇒ false ]
94   ].
95
96
97let rec is_in n (l: Vector addressing_mode_tag n) (A:addressing_mode) on l : bool ≝
98 match l return λm.λ_:Vector addressing_mode_tag m.bool with
99  [ VEmpty ⇒ false
100  | VCons m he (tl: Vector addressing_mode_tag m) ⇒
101     is_a he A ∨ is_in ? tl A ].
102
103record subaddressing_mode (n) (l: Vector addressing_mode_tag (S n)) : Type[0] ≝
104{
105  subaddressing_modeel:> addressing_mode;
106  subaddressing_modein: bool_to_Prop (is_in ? l subaddressing_modeel)
107}.
108
109coercion subaddressing_mode : ∀n.∀l:Vector addressing_mode_tag (S n).Type[0]
110 ≝ subaddressing_mode on _l: Vector addressing_mode_tag (S ?) to Type[0].
111
112coercion mk_subaddressing_mode :
113 ∀n.∀l:Vector addressing_mode_tag (S n).∀a:addressing_mode.
114  ∀p:bool_to_Prop (is_in ? l a).subaddressing_mode n l
115 ≝ mk_subaddressing_mode on a:addressing_mode to subaddressing_mode ? ?.
116 
117inductive preinstruction (A: Type[0]) : Type[0] ≝
118  ADD: [[acc_a]] → [[ registr ; direct ; indirect ; data ]] → preinstruction A
119| ADDC: [[acc_a]] → [[ registr ; direct ; indirect ; data ]] → preinstruction A
120| SUBB: [[acc_a]] → [[ registr ; direct ; indirect ; data ]] → preinstruction A
121| INC: [[ acc_a ; registr ; direct ; indirect ; dptr ]] → preinstruction A
122| DEC: [[ acc_a ; registr ; direct ; indirect ]] → preinstruction A
123| MUL: [[acc_a]] → [[acc_b]] → preinstruction A
124| DIV: [[acc_a]] → [[acc_b]] → preinstruction A
125| DA: [[acc_a]] → preinstruction A
126
127(* conditional jumps *)
128| JC: A → preinstruction A
129| JNC: A → preinstruction A
130| JB: [[bit_addr]] → A → preinstruction A
131| JNB: [[bit_addr]] → A → preinstruction A
132| JBC: [[bit_addr]] → A → preinstruction A
133| JZ: A → preinstruction A
134| JNZ: A → preinstruction A
135| CJNE:
136   [[acc_a]] × [[direct; data]] ⊎ [[registr; indirect]] × [[data]] → A → preinstruction A
137| DJNZ: [[registr ; direct]] → A → preinstruction A
138 (* logical operations *)
139| ANL:
140   [[acc_a]] × [[ registr ; direct ; indirect ; data ]] ⊎
141   [[direct]] × [[ acc_a ; data ]] ⊎
142   [[carry]] × [[ bit_addr ; n_bit_addr]] → preinstruction A
143| ORL:
144   [[acc_a]] × [[ registr ; data ; direct ; indirect ]] ⊎
145   [[direct]] × [[ acc_a ; data ]] ⊎
146   [[carry]] × [[ bit_addr ; n_bit_addr]] → preinstruction A
147| XRL:
148   [[acc_a]] × [[ data ; registr ; direct ; indirect ]] ⊎
149   [[direct]] × [[ acc_a ; data ]] → preinstruction A
150| CLR: [[ acc_a ; carry ; bit_addr ]] → preinstruction A
151| CPL: [[ acc_a ; carry ; bit_addr ]] → preinstruction A
152| RL: [[acc_a]] → preinstruction A
153| RLC: [[acc_a]] → preinstruction A
154| RR: [[acc_a]] → preinstruction A
155| RRC: [[acc_a]] → preinstruction A
156| SWAP: [[acc_a]] → preinstruction A
157
158 (* data transfer *)
159| MOV:
160    [[acc_a]] × [[ registr ; direct ; indirect ; data ]] ⊎
161    [[ registr ; indirect ]] × [[ acc_a ; direct ; data ]] ⊎
162    [[direct]] × [[ acc_a ; registr ; direct ; indirect ; data ]] ⊎
163    [[dptr]] × [[data16]] ⊎
164    [[carry]] × [[bit_addr]] ⊎
165    [[bit_addr]] × [[carry]] → preinstruction A
166| MOVX:
167    [[acc_a]] × [[ ext_indirect ; ext_indirect_dptr ]] ⊎
168    [[ ext_indirect ; ext_indirect_dptr ]] × [[acc_a]] → preinstruction A
169| SETB: [[ carry ; bit_addr ]] → preinstruction A
170| PUSH: [[direct]] → preinstruction A
171| POP: [[direct]] → preinstruction A
172| XCH: [[acc_a]] → [[ registr ; direct ; indirect ]] → preinstruction A
173| XCHD: [[acc_a]] → [[indirect]] → preinstruction A
174
175 (* program branching *)
176| RET: preinstruction A
177| RETI: preinstruction A
178| NOP: preinstruction A.
179
180inductive instruction: Type[0] ≝
181  | ACALL: [[addr11]] → instruction
182  | LCALL: [[addr16]] → instruction
183  | AJMP: [[addr11]] → instruction
184  | LJMP: [[addr16]] → instruction
185  | SJMP: [[relative]] → instruction
186  | JMP: [[indirect_dptr]] → instruction
187  | MOVC: [[acc_a]] → [[ acc_dptr ; acc_pc ]] → instruction
188  | RealInstruction: preinstruction [[ relative ]] → instruction.
189 
190coercion RealInstruction: ∀p: preinstruction [[ relative ]]. instruction ≝
191  RealInstruction on _p: preinstruction ? to instruction.
192
193inductive pseudo_instruction: Type[0] ≝
194  | Instruction: preinstruction Identifier → pseudo_instruction
195  | Comment: String → pseudo_instruction
196  | Cost: Identifier → pseudo_instruction
197  | Jmp: Identifier → pseudo_instruction
198  | Call: Identifier → pseudo_instruction
199  | Mov: [[dptr]] → Identifier → pseudo_instruction.
200
201definition labelled_instruction ≝ option Identifier × pseudo_instruction.
202definition preamble ≝ list (Identifier × nat).
203definition assembly_program ≝ list instruction.
204definition pseudo_assembly_program ≝ preamble × (list labelled_instruction).
Note: See TracBrowser for help on using the repository browser.