Changeset 876 for src/ASM/Fetch.ma


Ignore:
Timestamp:
Jun 3, 2011, 4:03:00 PM (9 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Fetch.ma

    r856 r876  
    66 λpmem: BitVectorTrie Byte 16.
    77 λpc: Word.
    8  let 〈x,res〉 ≝ half_add … pc (bitvector_of_nat 16 (S O)) in
    9    〈res, lookup … pc pmem (zero 8)〉.
     8  〈\snd (half_add … pc (bitvector_of_nat 16 (S O))), lookup … pc pmem (zero 8)〉.
    109
    1110(* timings taken from SIEMENS *)
    1211
    13 definition fetch: BitVectorTrie Byte 16 → Word → instruction × Word × nat ≝
     12definition fetch0: BitVectorTrie Byte 16 → Word × Byte → instruction × Word × nat ≝
    1413 λpmem: BitVectorTrie Byte 16.
    15  λpc: Word.
    16   let 〈pc,v〉 ≝ next pmem pc in
     14 λpc_v.
     15  let 〈pc,v〉 ≝ pc_v in
    1716   let 〈b,v〉 ≝ head … v in if b then
    1817    let 〈b,v〉 ≝ head … v in if b then
     
    390389  %.
    391390qed.
     391
     392definition fetch: BitVectorTrie Byte 16 → Word → instruction × Word × nat ≝
     393 λpmem: BitVectorTrie Byte 16.
     394 λpc: Word.
     395  fetch0 pmem (next pmem pc).
Note: See TracChangeset for help on using the changeset viewer.