diff options
Diffstat (limited to 'risc-v/riscv_extras_embed_sequential.lem')
| -rw-r--r-- | risc-v/riscv_extras_embed_sequential.lem | 71 |
1 files changed, 0 insertions, 71 deletions
diff --git a/risc-v/riscv_extras_embed_sequential.lem b/risc-v/riscv_extras_embed_sequential.lem deleted file mode 100644 index 3c922268..00000000 --- a/risc-v/riscv_extras_embed_sequential.lem +++ /dev/null @@ -1,71 +0,0 @@ -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_acquire : (vector bitU * integer) -> M (vector bitU) -val MEMr_strong_acquire : (vector bitU * integer) -> M (vector bitU) -val MEMr_reserved : (vector bitU * integer) -> M (vector bitU) -val MEMr_reserved_acquire : (vector bitU * integer) -> M (vector bitU) -val MEMr_reserved_strong_acquire : (vector bitU * integer) -> M (vector bitU) - -let MEMr (addr,size) = read_mem false Read_plain addr size -let MEMr_acquire (addr,size) = read_mem false Read_RISCV_acquire addr size -let MEMr_strong_acquire (addr,size) = read_mem false Read_RISCV_strong_acquire addr size -let MEMr_reserved (addr,size) = read_mem false Read_RISCV_reserved addr size -let MEMr_reserved_acquire (addr,size) = read_mem false Read_RISCV_reserved_acquire addr size -let MEMr_reserved_strong_acquire (addr,size) - = read_mem false Read_RISCV_reserved_strong_acquire addr size - -val MEMea : (vector bitU * integer) -> M unit -val MEMea_release : (vector bitU * integer) -> M unit -val MEMea_strong_release : (vector bitU * integer) -> M unit -val MEMea_conditional : (vector bitU * integer) -> M unit -val MEMea_conditional_release : (vector bitU * integer) -> M unit -val MEMea_conditional_strong_release : (vector bitU * integer) -> M unit - -let MEMea (addr,size) = write_mem_ea Write_plain addr size -let MEMea_release (addr,size) = write_mem_ea Write_RISCV_release addr size -let MEMea_strong_release (addr,size) = write_mem_ea Write_RISCV_strong_release addr size -let MEMea_conditional (addr,size) = write_mem_ea Write_RISCV_conditional addr size -let MEMea_conditional_release (addr,size) = write_mem_ea Write_RISCV_conditional_release addr size -let MEMea_conditional_strong_release (addr,size) - = write_mem_ea Write_RISCV_conditional_strong_release addr size - -val MEMval : (vector bitU * integer * vector bitU) -> M unit -val MEMval_release : (vector bitU * integer * vector bitU) -> M unit -val MEMval_strong_release : (vector bitU * integer * vector bitU) -> M unit -val MEMval_conditional : (vector bitU * integer * vector bitU) -> M unit -val MEMval_conditional_release : (vector bitU * integer * vector bitU) -> M unit -val MEMval_conditional_strong_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_strong_release (_,_,v) = write_mem_val v >>= fun _ -> return () -let MEMval_conditional (_,_,v) = write_mem_val v >>= fun _ -> return () -let MEMval_conditional_release (_,_,v) = write_mem_val v >>= fun _ -> return () -let MEMval_conditional_strong_release (_,_,v) - = write_mem_val v >>= fun _ -> return () - -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 -val MEM_fence_r_r : unit -> M unit -val MEM_fence_rw_w : unit -> M unit -val MEM_fence_w_w : unit -> M unit -val MEM_fence_i : unit -> M unit - -let MEM_fence_rw_rw () = barrier Barrier_RISCV_rw_rw -let MEM_fence_r_rw () = barrier Barrier_RISCV_r_rw -let MEM_fence_r_r () = barrier Barrier_RISCV_r_r -let MEM_fence_rw_w () = barrier Barrier_RISCV_rw_w -let MEM_fence_w_w () = barrier Barrier_RISCV_w_w -let MEM_fence_i () = barrier Barrier_RISCV_i - -let duplicate (bit,len) = - let bits = repeat [bit] len in - let start = len - 1 in - Vector bits start false |