From 07fad742df72ff6e7bfb948c1c353a2cf12f5e28 Mon Sep 17 00:00:00 2001
From: Shaked Flur
Date: Thu, 31 Aug 2017 15:08:10 +0100
Subject: added RISC-V AMOs

---
 risc-v/riscv_extras_embed.lem | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

(limited to 'risc-v/riscv_extras_embed.lem')

diff --git a/risc-v/riscv_extras_embed.lem b/risc-v/riscv_extras_embed.lem
index 6bfc2490..3f04f9a2 100644
--- a/risc-v/riscv_extras_embed.lem
+++ b/risc-v/riscv_extras_embed.lem
@@ -26,13 +26,15 @@ let MEMea_conditional_release (addr,size) = write_mem_ea Write_RISCV_conditional
 
 val MEMval                     : (vector bitU * integer * vector bitU) -> M unit
 val MEMval_release             : (vector bitU * integer * vector bitU) -> M unit
-val MEMval_conditional         : (vector bitU * integer * vector bitU) -> M bitU
-val MEMval_conditional_release : (vector bitU * integer * vector bitU) -> M bitU
+val MEMval_conditional         : (vector bitU * integer * vector bitU) -> M unit
+val MEMval_conditional_release : (vector bitU * integer * vector bitU) -> M unit
 
 let MEMval (_,_,v)                     = write_mem_val v >>= fun _ -> return ()
 let MEMval_release (_,_,v)             = write_mem_val v >>= fun _ -> return ()
-let MEMval_conditional (_,_,v)         = write_mem_val v >>= fun b -> return (if b then B1 else B0)
-let MEMval_conditional_release (_,_,v) = write_mem_val v >>= fun b -> return (if b then B1 else B0)
+let MEMval_conditional (_,_,v)         = write_mem_val v >>= fun _ -> return () (* (if b then B1 else B0) *)
+let MEMval_conditional_release (_,_,v) = write_mem_val v >>= fun _ -> return () (* (if b then B1 else B0) *)
+
+let speculate_conditional_success () = excl_result () >>= fun b -> return (if b then B1 else B0)
 
 val MEM_fence_rw_rw : unit -> M unit
 val MEM_fence_r_rw  : unit -> M unit
-- 
cgit v1.2.3