Changeset 293
 Timestamp:
 Nov 25, 2010, 3:09:42 PM (9 years ago)
 Location:
 Deliverables/D4.1/Matita
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/ASM.ma
r283 r293 99 99 JC: A → jump A 100 100  JNC: A → jump A 101  JB: Bit→ A → jump A102  JNB: Bit→ A → jump A103  JBC: Bit→ A → jump A101  JB: [[bit_addr]] → A → jump A 102  JNB: [[bit_addr]] → A → jump A 103  JBC: [[bit_addr]] → A → jump A 104 104  JZ: A → jump A 105 105  JNZ: A → jump A 106 106  CJNE: 107 [[acc_a]] × [[direct; data]] ⊎ 108 [[register; indirect]] × [[data]] → A → jump A 107 [[acc_a]] × [[direct; data]] ⊎ [[register; indirect]] × [[data]] → A → jump A 109 108  DJNZ: [[register ; direct]] → A → jump A. 110 109 
Deliverables/D4.1/Matita/Assembly.ma
r284 r293 2 2 3 3 ndefinition assembly1 ≝ 4 λ A.λi: preinstruction A.match i with4 λi: instruction.match i with 5 5 [ ACALL addr ⇒ 6 6 match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with … … 54 54  N_BIT_ADDR b1 ⇒ λ_. [ ([[true;false;true;true;false;false;false;false]]) ; b1 ] 55 55  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)] 56 (*57  `CJNE (`U1 (`A, `DIRECT b1), `REL b2) >58 [mk_byte_from_bits ((true,false,true,true),(false,true,false,true)); b1; b2]59  `CJNE (`U1 (`A, `DATA b1), `REL b2) >60 [mk_byte_from_bits ((true,false,true,true),(false,true,false,false)); b1; b2]61  `CJNE (`U2 (`REG(r1,r2,r3), `DATA b1), `REL b2) >62 [mk_byte_from_bits ((true,false,true,true),(true,r1,r2,r3)); b1; b2]63  `CJNE (`U2 (`INDIRECT i1, `DATA b1), `REL b2) >64 [mk_byte_from_bits ((true,false,true,true),(false,true,true,i1)); b1; b2]65 *)66 56  CLR addr ⇒ 67 57 match addr return λx. bool_to_Prop (is_in ? [[acc_a;carry;bit_addr]] x) → ? with … … 97 87  DIV addr1 addr2 ⇒ 98 88 [ ([[true;false;false;false;false;true;false;false]]) ] 99 89  Jump j ⇒ 90 match j with 91 [ DJNZ addr1 addr2 ⇒ 92 let b2 ≝ 93 match addr2 return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with 94 [ RELATIVE b2 ⇒ λ_. b2 95  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in 96 match addr1 return λx. bool_to_Prop (is_in ? [[register;direct]] x) → ? with 97 [ REGISTER r1 r2 r3 ⇒ λ_. 98 [ ([[true; true; false; true; true; r1; r2; r3]]) ; b2 ] 99  DIRECT b1 ⇒ λ_. 100 [ ([[true; true; false; true; false; true; false; true]]); b1; b2 ] 101  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) 102  JC addr ⇒ 103 match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with 104 [ RELATIVE b1 ⇒ λ_. 105 [ ([[false; true; false; false; false; false; false; false]]); b1 ] 106  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) 107  JNC addr ⇒ 108 match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with 109 [ RELATIVE b1 ⇒ λ_. 110 [ ([[false; true; false; true; false; false; false; false]]); b1 ] 111  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) 112  JZ addr ⇒ 113 match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with 114 [ RELATIVE b1 ⇒ λ_. 115 [ ([[false; true; true; false; false; false; false; false]]); b1 ] 116  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) 117  JNZ addr ⇒ 118 match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with 119 [ RELATIVE b1 ⇒ λ_. 120 [ ([[false; true; true; true; false; false; false; false]]); b1 ] 121  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) 122  JB addr1 addr2 ⇒ 123 let b2 ≝ 124 match addr2 return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with 125 [ RELATIVE b2 ⇒ λ_. b2 126  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in 127 match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with 128 [ BIT_ADDR b1 ⇒ λ_. 129 [ ([[false; false; true; false; false; false; false; false]]); b1; b2 ] 130  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) 131  JNB addr1 addr2 ⇒ 132 let b2 ≝ 133 match addr2 return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with 134 [ RELATIVE b2 ⇒ λ_. b2 135  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in 136 match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with 137 [ BIT_ADDR b1 ⇒ λ_. 138 [ ([[false; false; true; true; false; false; false; false]]); b1; b2 ] 139  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) 140  JBC addr1 addr2 ⇒ 141 let b2 ≝ 142 match addr2 return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with 143 [ RELATIVE b2 ⇒ λ_. b2 144  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in 145 match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with 146 [ BIT_ADDR b1 ⇒ λ_. 147 [ ([[false; false; false; true; false; false; false; false]]); b1; b2 ] 148  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) 149  CJNE addrs addr3 ⇒ 150 let b3 ≝ 151 match addr3 return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with 152 [ RELATIVE b3 ⇒ λ_. b3 153  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr3) in 154 match addrs with 155 [ Left addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in 156 match addr2 return λx. bool_to_Prop (is_in ? [[direct;data]] x) → ? with 157 [ DIRECT b1 ⇒ λ_. 158 [ ([[true; false; true; true; false; true; false; true]]); b1; b3 ] 159 [ DATA b1 ⇒ λ_. 160 [ ([[true; false; true; true; false; true; false; false]]); b1; b3 ] 161  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) 162  Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in 163 let b2 ≝ 164 match addr2 return λx. bool_to_Prop (is_in ? [[data]] x) → ? with 165 [ DATA b2 ⇒ λ_. b2 166  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in 167 match addr2 return λx. bool_to_Prop (is_in ? [[direct;data]] x) → ? with 168 [ DIRECT b1 ⇒ λ_. 169 [ ([[true; false; true; true; false; true; false; true]]); b1; b3 ] 170 [ DATA b1 ⇒ λ_. 171 [ ([[true; false; true; true; false; true; false; false]]); b1; b3 ] 172  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) 173 174 ] 175  _ ⇒ [ ] 176 ] 100 177  _ ⇒ [ ]]. 101 178 102 179 (* 103  `DJNZ (`REG(r1,r2,r3), `REL b1) > 104 [mk_byte_from_bits ((true,true,false,true),(true,r1,r2,r3)); b1] 105  `DJNZ (`DIRECT b1, `REL b2) > 106 [mk_byte_from_bits ((true,true,false,true),(false,true,false,true)); b1; b2] 180  `CJNE (`U2 (`REG(r1,r2,r3), `DATA b1), `REL b2) > 181 [mk_byte_from_bits ((true,false,true,true),(true,r1,r2,r3)); b1; b2] 182  `CJNE (`U2 (`INDIRECT i1, `DATA b1), `REL b2) > 183 [mk_byte_from_bits ((true,false,true,true),(false,true,true,i1)); b1; b2] 184 185 107 186  `INC `A > 108 187 [mk_byte_from_bits ((false,false,false,false),(false,true,false,false))] … … 115 194  `INC `DPTR > 116 195 [mk_byte_from_bits ((true,false,true,false),(false,false,true,true))] 117  `JB (`BIT b1, `REL b2) >118 [mk_byte_from_bits ((false,false,true,false),(false,false,false,false)); b1; b2]119  `JBC (`BIT b1, `REL b2) >120 [mk_byte_from_bits ((false,false,false,true),(false,false,false,false)); b1; b2]121  `JC (`REL b1) >122 [mk_byte_from_bits ((false,true,false,false),(false,false,false,false)); b1]123 196  `JMP `IND_DPTR > 124 197 [mk_byte_from_bits ((false,true,true,true),(false,false,true,true))] 125  `JNB (`BIT b1, `REL b2) >126 [mk_byte_from_bits ((false,false,true,true),(false,false,false,false)); b1; b2]127  `JNC (`REL b1) >128 [mk_byte_from_bits ((false,true,false,true),(false,false,false,false)); b1]129  `JNZ (`REL b1) >130 [mk_byte_from_bits ((false,true,true,true),(false,false,false,false)); b1]131  `JZ (`REL b1) >132 [mk_byte_from_bits ((false,true,true,false),(false,false,false,false)); b1]133 198  `LCALL (`ADDR16 w) > 134 199 let (b1,b2) = from_word w in
Note: See TracChangeset
for help on using the changeset viewer.