Changeset 297


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

...

Location:
Deliverables/D4.1/Matita
Files:
2 edited

Legend:

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

    r293 r297  
    146146    [[carry]] × [[bit_addr]] ⊎
    147147    [[bit_addr]] × [[carry]] → preinstruction A
    148  | MOVC: [[acc_a]] × [[ acc_dptr ; acc_pc ]] → preinstruction A
     148 | MOVC: [[acc_a]] [[ acc_dptr ; acc_pc ]] → preinstruction A
    149149 | MOVX:
    150150    [[acc_a]] × [[ ext_indirect ; ext_indirect_dptr ]] ⊎
  • Deliverables/D4.1/Matita/Assembly.ma

    r296 r297  
    173173                 [ ([[true; false; true; true; false; true; true; i1]]); b2; b3 ] *)
    174174              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)*) ]]
    175   | _ ⇒ [ ]].
     175  | INC addr ⇒
     176     match addr return λx. bool_to_Prop (is_in ? [[acc_a;register;direct;indirect;dptr]] x) → ? with
     177      [ ACC_A ⇒ λ_.
     178         [ ([[false;false;false;false;false;true;false;false]]) ]         
     179      | REGISTER r1 r2 r3 ⇒ λ_.
     180         [ ([[false;false;false;false;true;r1;r2;r3]]) ]
     181      | DIRECT b1 ⇒ λ_.
     182         [ ([[false; false; false; false; false; true; false; true]]); b1 ]
     183      | INDIRECT i1 ⇒ λ_.
     184        [ ([[false; false; false; false; false; true; true; i1]]) ]
     185      | DPTR ⇒ λ_.
     186        [ ([[true;false;true;false;false;false;true;true]]) ]
     187      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
     188  | JMP addr ⇒
     189     [ ([[false;true;true;true;false;false;true;true]]) ]
     190  | LCALL addr ⇒
     191     match addr return λx. bool_to_Prop (is_in ? [[addr16]] x) → ? with
     192      [ ADDR16 w ⇒ λ_.
     193         let 〈b1,b2〉 ≝ split ? (S (S (S (S (S (S (S (S Z)))))))) (S (S (S (S (S (S (S (S Z)))))))) w in
     194          [ ([[false;false;false;true;false;false;true;false]]); b1; b2 ]         
     195      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
     196  | LJMP addr ⇒
     197     match addr return λx. bool_to_Prop (is_in ? [[addr16]] x) → ? with
     198      [ ADDR16 w ⇒ λ_.
     199         let 〈b1,b2〉 ≝ split ? (S (S (S (S (S (S (S (S Z)))))))) (S (S (S (S (S (S (S (S Z)))))))) w in
     200          [ ([[false;false;false;false;false;false;true;false]]); b1; b2 ]         
     201      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
    176202(*
    177   | `INC `A ->
    178     [mk_byte_from_bits ((false,false,false,false),(false,true,false,false))]
    179   | `INC (`REG(r1,r2,r3)) ->
    180     [mk_byte_from_bits ((false,false,false,false),(true,r1,r2,r3))]
    181   | `INC (`DIRECT b1) ->
    182     [mk_byte_from_bits ((false,false,false,false),(false,true,false,true)); b1]
    183   | `INC (`INDIRECT i1) ->
    184     [mk_byte_from_bits ((false,false,false,false),(false,true,true,i1))]
    185   | `INC `DPTR ->
    186     [mk_byte_from_bits ((true,false,true,false),(false,false,true,true))]
    187   | `JMP `IND_DPTR ->
    188     [mk_byte_from_bits ((false,true,true,true),(false,false,true,true))]
    189   | `LCALL (`ADDR16 w) ->
    190       let (b1,b2) = from_word w in
    191         [mk_byte_from_bits ((false,false,false,true),(false,false,true,false)); b1; b2]
    192   | `LJMP (`ADDR16 w) ->
    193       let (b1,b2) = from_word w in
    194         [mk_byte_from_bits ((false,false,false,false),(false,false,true,false)); b1; b2]
    195203  | `MOV (`U1 (`A, `REG(r1,r2,r3))) ->
    196204    [mk_byte_from_bits ((true,true,true,false),(true,r1,r2,r3))]
     
    230238    let (b1,b2) = from_word w in
    231239      [mk_byte_from_bits ((true,false,false,true),(false,false,false,false)); b1; b2]
    232   | `MOVC (`A, `A_DPTR) ->
    233     [mk_byte_from_bits ((true,false,false,true),(false,false,true,true))]
    234   | `MOVC (`A, `A_PC) ->
    235     [mk_byte_from_bits ((true,false,false,false),(false,false,true,true))]
     240*)
     241  | MOVC addr1 addr2 ⇒
     242     match addr2 return λx. bool_to_Prop (is_in ? [[acc_dptr;acc_pc]] x) → ? with
     243      [ ACC_DPTR ⇒ λ_.
     244         [ ([[true;false;false;true;false;false;true;true]]) ]
     245      | ACC_PC ⇒ λ_.
     246         [ ([[true;false;false;false;false;false;true;true]]) ]
     247      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
     248(*
    236249  | `MOVX (`U1 (`A, `EXT_INDIRECT i1)) ->
    237250    [mk_byte_from_bits ((true,true,true,false),(false,false,true,i1))]
     
    242255  | `MOVX (`U2 (`EXT_IND_DPTR, `A)) ->
    243256    [mk_byte_from_bits ((true,true,true,true),(false,false,false,false))]
     257*)
     258
     259
     260  | _ ⇒ [ ]].
     261
     262
     263
     264(*
    244265  | `MUL(`A, `B) ->
    245266    [mk_byte_from_bits ((true,false,true,false),(false,true,false,false))]
Note: See TracChangeset for help on using the changeset viewer.