Changeset 298


Ignore:
Timestamp:
Nov 25, 2010, 10:44:45 PM (9 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Matita/Assembly.ma

    r297 r298  
    256256    [mk_byte_from_bits ((true,true,true,true),(false,false,false,false))]
    257257*)
    258 
    259 
    260   | _ ⇒ [ ]].
    261 
    262 
    263 
     258  | MUL addr1 addr2 ⇒
     259     [ ([[true;false;true;false;false;true;false;false]]) ]
     260  | NOP ⇒
     261     [ ([[false;false;false;false;false;false;false;false]]) ]
    264262(*
    265   | `MUL(`A, `B) ->
    266     [mk_byte_from_bits ((true,false,true,false),(false,true,false,false))]
    267   | `NOP ->
    268     [mk_byte_from_bits ((false,false,false,false),(false,false,false,false))]
    269263  | `ORL (`U1(`A, `REG(r1,r2,r3))) ->
    270264    [mk_byte_from_bits ((false,true,false,false),(true,r1,r2,r3))]
     
    283277  | `ORL (`U3 (`C, `NBIT b1)) ->
    284278    [mk_byte_from_bits ((true,false,true,false),(false,false,false,false)); b1]
    285   | `POP (`DIRECT b1) ->
    286     [mk_byte_from_bits ((true,true,false,true),(false,false,false,false)); b1]
    287   | `PUSH (`DIRECT b1) ->
    288     [mk_byte_from_bits ((true,true,false,false),(false,false,false,false)); b1]
    289   | `RET ->
    290     [mk_byte_from_bits ((false,false,true,false),(false,false,true,false))]
    291   | `RETI ->
    292     [mk_byte_from_bits ((false,false,true,true),(false,false,true,false))]
    293   | `RL `A ->
    294     [mk_byte_from_bits ((false,false,true,false),(false,false,true,true))]
    295   | `RLC `A ->
    296     [mk_byte_from_bits ((false,false,true,true),(false,false,true,true))]
    297   | `RR `A ->
    298     [mk_byte_from_bits ((false,false,false,false),(false,false,true,true))]
    299   | `RRC `A ->
    300     [mk_byte_from_bits ((false,false,false,true),(false,false,true,true))]
    301   | `SETB `C ->
    302     [mk_byte_from_bits ((true,true,false,true),(false,false,true,true))]
    303   | `SETB (`BIT b1) ->
    304     [mk_byte_from_bits ((true,true,false,true),(false,false,true,false)); b1]
     279*)
     280  | POP addr ⇒
     281     match addr return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
     282      [ DIRECT b1 ⇒ λ_.
     283         [ ([[true;true;false;true;false;false;false;false]]) ; b1 ]
     284      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
     285  | PUSH addr ⇒
     286     match addr return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
     287      [ DIRECT b1 ⇒ λ_.
     288         [ ([[true;true;false;false;false;false;false;false]]) ; b1 ]
     289      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
     290  | RET ⇒
     291     [ ([[false;false;true;false;false;false;true;false]]) ]
     292  | RETI ⇒
     293     [ ([[false;false;true;true;false;false;true;false]]) ]
     294  | RL addr ⇒
     295     [ ([[false;false;true;false;false;false;true;true]]) ]
     296  | RLC addr ⇒
     297     [ ([[false;false;true;true;false;false;true;true]]) ]
     298  | RR addr ⇒
     299     [ ([[false;false;false;false;false;false;true;true]]) ]
     300  | RRC addr ⇒
     301     [ ([[false;false;false;true;false;false;true;true]]) ]
     302  | SETB addr ⇒     
     303     match addr return λx. bool_to_Prop (is_in ? [[carry;bit_addr]] x) → ? with
     304      [ CARRY ⇒ λ_.
     305         [ ([[true;true;false;true;false;false;true;true]]) ]
     306      | BIT_ADDR b1 ⇒ λ_.
     307         [ ([[true;true;false;true;false;false;true;false]]); b1 ]
     308      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
     309
     310  | _ ⇒ [ ]].
     311(*
    305312  | `SJMP (`REL b1) ->
    306313    [mk_byte_from_bits ((true,false,false,false),(false,false,false,false)); b1]
     314
    307315  | `SUBB (`A, `REG(r1,r2,r3)) ->
    308316    [mk_byte_from_bits ((true,false,false,true),(true,r1,r2,r3))]
     
    313321  | `SUBB (`A, `DATA b1) ->
    314322    [mk_byte_from_bits ((true,false,false,true),(false,true,false,false)); b1]
     323
    315324  | `SWAP `A ->
    316325    [mk_byte_from_bits ((true,true,false,false),(false,true,false,false))]
     326
    317327  | `XCH (`A, `REG(r1,r2,r3)) ->
    318328    [mk_byte_from_bits ((true,true,false,false),(true,r1,r2,r3))]
     
    321331  | `XCH (`A, `INDIRECT i1) ->
    322332    [mk_byte_from_bits ((true,true,false,false),(false,true,true,i1))]
     333
    323334  | `XCHD(`A, `INDIRECT i1) ->
    324335    [mk_byte_from_bits ((true,true,false,true),(false,true,true,i1))]
     336
    325337  | `XRL(`U1(`A, `REG(r1,r2,r3))) ->
    326338    [mk_byte_from_bits ((false,true,true,false),(true,r1,r2,r3))]
Note: See TracChangeset for help on using the changeset viewer.