diff options
| author | Thomas Bauereiss <tb592@cl.cam.ac.uk> | 2019-10-07 16:00:56 +0100 |
|---|---|---|
| committer | Prashanth Mundkur <prashanth.mundkur@gmail.com> | 2019-10-09 22:04:15 -0700 |
| commit | 0e42c867fba498746405d2b878a12fd4d143c5d8 (patch) | |
| tree | 689e0ee412b6c91bcadb989148b72ad48b464a9b /handwritten_support | |
| parent | a13c0a435804a9a8250054c2e9af2eacfa883164 (diff) | |
| download | sail-riscv-0e42c867fba498746405d2b878a12fd4d143c5d8.zip sail-riscv-0e42c867fba498746405d2b878a12fd4d143c5d8.tar.gz sail-riscv-0e42c867fba498746405d2b878a12fd4d143c5d8.tar.bz2 | |
Add {read,write}_ram for Coq
Diffstat (limited to 'handwritten_support')
| -rw-r--r-- | handwritten_support/mem_metadata.v | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/handwritten_support/mem_metadata.v b/handwritten_support/mem_metadata.v new file mode 100644 index 0000000..ddb26e4 --- /dev/null +++ b/handwritten_support/mem_metadata.v @@ -0,0 +1,11 @@ +Require Import Sail2_instr_kinds. +Require Import Sail2_values. +Require Import Sail2_operators_mwords. +Require Import Sail2_prompt_monad. +Require Import Sail2_prompt. + +Definition write_ram {rv e} wk (addr : mword 64) size (v : mword (8 * size)) (meta : unit) : monad rv bool e := write_mem wk 64 addr size v. + +Definition read_ram {rv e} rk (addr : mword 64) size (read_tag : bool) `{ArithFact (size >= 0)} : monad rv (mword (8 * size) * unit) e := + read_mem rk 64 addr size >>= fun data => + returnm (data, tt).
\ No newline at end of file |