Changeset 278 for Deliverables/D4.1/Matita/ASM.ma
 Timestamp:
 Nov 24, 2010, 5:18:11 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/ASM.ma
r271 r278 110 110 111 111 ninductive preinstruction (A: Type[0]) : Type[0] ≝ 112 ADD: [[acc_a]] > [[ register ; direct ; indirect ; data ]] >preinstruction A113  ADDC: [[acc_a]] × [[ register ; direct ; indirect ; data ]] >preinstruction A114  SUBB: [[acc_a]] × [[ register ; direct ; indirect ; data ]] >preinstruction A115  INC: [[ acc_a ; register ; direct ; indirect ; dptr ]] >preinstruction A116  DEC: [[ acc_a ; register ; direct ; indirect ]] >preinstruction A117  MUL: [[acc_a]] × [[acc_b]] >preinstruction A118  DIV: [[acc_a]] × [[acc_b]] >preinstruction A119  DA: [[acc_a]] >preinstruction A112 ADD: [[acc_a]] → [[ register ; direct ; indirect ; data ]] → preinstruction A 113  ADDC: [[acc_a]] → [[ register ; direct ; indirect ; data ]] → preinstruction A 114  SUBB: [[acc_a]] → [[ register ; direct ; indirect ; data ]] → preinstruction A 115  INC: [[ acc_a ; register ; direct ; indirect ; dptr ]] → preinstruction A 116  DEC: [[ acc_a ; register ; direct ; indirect ]] → preinstruction A 117  MUL: [[acc_a]] → [[acc_b]] → preinstruction A 118  DIV: [[acc_a]] → [[acc_b]] → preinstruction A 119  DA: [[acc_a]] → preinstruction A 120 120 121 121 (* logical operations *) … … 123 123 [[acc_a]] × [[ register ; direct ; indirect ; data ]] ⊎ 124 124 [[direct]] × [[ acc_a ; data ]] ⊎ 125 [[carry]] × [[ bit_addr ; n_bit_addr]] >preinstruction A125 [[carry]] × [[ bit_addr ; n_bit_addr]] → preinstruction A 126 126  ORL: 127 127 [[acc_a]] × [[ register ; data ; direct ; indirect ]] ⊎ 128 128 [[direct]] × [[ acc_a ; data ]] ⊎ 129 [[carry]] × [[ bit_addr ; n_bit_addr]] >preinstruction A129 [[carry]] × [[ bit_addr ; n_bit_addr]] → preinstruction A 130 130  XRL: 131 131 [[acc_a]] × [[ data ; register ; direct ; indirect ]] ⊎ 132 [[direct]] × [[ acc_a ; data ]] >preinstruction A133  CLR: [[ acc_a ; carry ; bit_addr ]] >preinstruction A134  CPL: [[ acc_a ; carry ; bit_addr ]] >preinstruction A135  RL: [[acc_a]] >preinstruction A136  RLC: [[acc_a]] >preinstruction A137  RR: [[acc_a]] >preinstruction A138  RRC: [[acc_a]] >preinstruction A139  SWAP: [[acc_a]] >preinstruction A132 [[direct]] × [[ acc_a ; data ]] → preinstruction A 133  CLR: [[ acc_a ; carry ; bit_addr ]] → preinstruction A 134  CPL: [[ acc_a ; carry ; bit_addr ]] → preinstruction A 135  RL: [[acc_a]] → preinstruction A 136  RLC: [[acc_a]] → preinstruction A 137  RR: [[acc_a]] → preinstruction A 138  RRC: [[acc_a]] → preinstruction A 139  SWAP: [[acc_a]] → preinstruction A 140 140 141 141 (* data transfer *) … … 146 146 [[dptr]] × [[data16]] ⊎ 147 147 [[carry]] × [[bit_addr]] ⊎ 148 [[bit_addr]] × [[carry]] >preinstruction A149  MOVC: [[acc_a]] × [[ acc_dptr ; acc_pc ]] >preinstruction A148 [[bit_addr]] × [[carry]] → preinstruction A 149  MOVC: [[acc_a]] × [[ acc_dptr ; acc_pc ]] → preinstruction A 150 150  MOVX: 151 151 [[acc_a]] × [[ ext_indirect ; ext_indirect_dptr ]] ⊎ 152 [[ ext_indirect ; ext_indirect_dptr ]] × [[acc_a]] >preinstruction A153  SETB: [[ carry ; bit_addr ]] >preinstruction A154  PUSH: [[direct]] >preinstruction A155  POP: [[direct]] >preinstruction A156  XCH: [[acc_a]] × [[ register ; direct ; indirect ]] >preinstruction A157  XCHD: [[acc_a]] × [[indirect]] >preinstruction A152 [[ ext_indirect ; ext_indirect_dptr ]] × [[acc_a]] → preinstruction A 153  SETB: [[ carry ; bit_addr ]] → preinstruction A 154  PUSH: [[direct]] → preinstruction A 155  POP: [[direct]] → preinstruction A 156  XCH: [[acc_a]] → [[ register ; direct ; indirect ]] → preinstruction A 157  XCHD: [[acc_a]] → [[indirect]] → preinstruction A 158 158 159 159 (* program branching *) 160 160  Jump: jump A → preinstruction A 161  ACALL: [[addr11]] >preinstruction A162  LCALL: [[addr16]] >preinstruction A161  ACALL: [[addr11]] → preinstruction A 162  LCALL: [[addr16]] → preinstruction A 163 163  RET: preinstruction A 164 164  RETI: preinstruction A 165  AJMP: [[addr11]] >preinstruction A166  LJMP: [[addr16]] >preinstruction A167  SJMP: [[relative]] >preinstruction A168  JMP: [[indirect_dptr]] >preinstruction A165  AJMP: [[addr11]] → preinstruction A 166  LJMP: [[addr16]] → preinstruction A 167  SJMP: [[relative]] → preinstruction A 168  JMP: [[indirect_dptr]] → preinstruction A 169 169  NOP: preinstruction A. 170 170 … … 176 176  Jmp: String → labelled_instruction 177 177  Call: String → labelled_instruction 178  Mov: [[dptr]] ×String → labelled_instruction178  Mov: [[dptr]] → String → labelled_instruction 179 179  WithLabel: preinstruction String → labelled_instruction. 180 180
Note: See TracChangeset
for help on using the changeset viewer.