work on integrating risc-v model with rmem (incomplete).

1 files changed, 34 insertions, 0 deletions

diff --git a/risc-v/riscv_extras_embed_sequential.lem b/risc-v/riscv_extras_embed_sequential.lem
new file mode 100644
index 00000000..7fb62161
--- /dev/null
+++ b/risc-v/riscv_extras_embed_sequential.lem
@@ -0,0 +1,34 @@
+open import Pervasives
+open import Pervasives_extra
+open import Sail_impl_base
+open import Sail_values
+open import State
+
+val MEMr             : (vector bitU * integer) -> M (vector bitU)
+val MEMr_reserve     : (vector bitU * integer) -> M (vector bitU)
+
+let MEMr (addr,size)             = read_mem false Read_plain addr size
+let MEMr_reserve (addr,size)     = read_mem false Read_reserve addr size
+
+val MEMea                 : (vector bitU * integer) -> M unit
+val MEMea_conditional     : (vector bitU * integer) -> M unit
+
+let MEMea (addr,size)                 = write_mem_ea Write_plain addr size
+let MEMea_conditional (addr,size)     = write_mem_ea Write_conditional addr size
+
+
+val MEMval                 : (vector bitU * integer * vector bitU) -> M unit
+val MEMval_conditional     : (vector bitU * integer * vector bitU) -> M bitU
+
+let MEMval (_,_,v)                   = write_mem_val v >>= fun _ -> return ()
+let MEMval_conditional (_,_,v)       = write_mem_val v >>= fun b -> return (if b then B1 else B0)
+
+val MEM_sync  : unit -> M unit
+
+let MEM_sync () = barrier Barrier_MIPS_SYNC
+
+
+let duplicate (bit,len) =
+  let bits = repeat [bit] len in
+  let start = len - 1 in
+  Vector bits start false