1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
|
open import Pervasives
open import State
open import Sail_values
let rMem_NORMAL (addr,l) = read_memory (unsigned addr) l
let rMem_STREAM (addr,l) = read_memory (unsigned addr) l
let rMem_ORDERED (addr,l) = read_memory (unsigned addr) l
let rMem_ATOMIC (addr,l) = read_memory (unsigned addr) l
let rMem_ATOMIC_ORDERED (addr,l) = read_memory (unsigned addr) l
let wMem_NORMAL (addr,l,v) = write_memory (unsigned addr) l v
let wMem_ORDERED (addr,l,v) = write_memory (unsigned addr) l v
let wMem_ATOMIC (addr,l,v) = write_memory (unsigned addr) l v
let wMem_ATOMIC_ORDERED (addr,l,v) = write_memory (unsigned addr) l v
let wMem_Addr_NORMAL (addr,l) = write_writeEA (unsigned addr) l
let wMem_Addr_ORDERED (addr,l) = write_writeEA (unsigned addr) l
let wMem_Addr_ATOMIC (addr,l) = write_writeEA (unsigned addr) l
let wMem_Addr_ATOMIC_ORDERED (addr,l) = write_writeEA (unsigned addr) l
let wMem_Val_NORMAL (l,v) = read_writeEA () >>= fun (addr,_) -> write_memory addr l v >> return ()
let wMem_Val_ATOMIC (l,v) = read_writeEA () >>= fun (addr,_) -> write_memory addr l v >> return Vector.O
let DataMemoryBarrier_Reads () = return ()
let DataMemoryBarrier_Writes () = return ()
let DataMemoryBarrier_All () = return ()
let DataSynchronizationBarrier_Reads () = return ()
let DataSynchronizationBarrier_Writes () = return ()
let DataSynchronizationBarrier_All () = return ()
let InstructionSynchronizationBarrier () = return ()
|
