blob: 24bcecb86b6ab88aa8f0be9962c81e4a544ea216 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
|
open import Pervasives
open import Pervasives_extra
open import Sail2_instr_kinds
open import Sail2_values
open import Sail2_operators_mwords
open import Sail2_prompt_monad
open import Sail2_prompt
val write_ram : forall 'rv 'e 'n. Size 'n => write_kind -> mword ty64 -> integer -> mword 'n -> unit -> monad 'rv bool 'e
let write_ram wk addr width data meta =
write_mem wk () addr width data
val read_ram : forall 'rv 'e 'n. Size 'n => read_kind -> mword ty64 -> integer -> bool -> monad 'rv (mword 'n * unit) 'e
let read_ram rk addr width read_tag =
read_mem rk () addr width >>= (fun (data : mword 'n) ->
return (data, ()))
|
