diff options
Diffstat (limited to 'riscv')
| -rw-r--r-- | riscv/prelude.sail | 8 | ||||
| -rw-r--r-- | riscv/riscv_extras_embed_sequential.lem | 22 |
2 files changed, 24 insertions, 6 deletions
diff --git a/riscv/prelude.sail b/riscv/prelude.sail index 370f9370..754a5cec 100644 --- a/riscv/prelude.sail +++ b/riscv/prelude.sail @@ -90,9 +90,9 @@ overload operator != = {neq_atom, neq_int, neq_vec, neq_anything} val and_bool = "and_bool" : (bool, bool) -> bool -val builtin_and_vec = {ocaml: "and_vec", lem: "Sail_operators.and_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n) +val builtin_and_vec = {ocaml: "and_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n) -val and_vec : forall 'n. (bits('n), bits('n)) -> bits('n) +val and_vec = {lem: "and_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n) function and_vec (xs, ys) = builtin_and_vec(xs, ys) @@ -100,9 +100,9 @@ overload operator & = {and_bool, and_vec} val or_bool = "or_bool" : (bool, bool) -> bool -val builtin_or_vec = {ocaml: "or_vec", lem: "Sail_operators.or_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n) +val builtin_or_vec = {ocaml: "or_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n) -val or_vec : forall 'n. (bits('n), bits('n)) -> bits('n) +val or_vec = {lem: "or_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n) function or_vec (xs, ys) = builtin_or_vec(xs, ys) diff --git a/riscv/riscv_extras_embed_sequential.lem b/riscv/riscv_extras_embed_sequential.lem index 2d28f3c2..4ef3ed36 100644 --- a/riscv/riscv_extras_embed_sequential.lem +++ b/riscv/riscv_extras_embed_sequential.lem @@ -2,10 +2,12 @@ open import Pervasives open import Pervasives_extra open import Sail_impl_base open import Sail_values -open import Sail_operators +open import Sail_operators_mwords open import State open import State_monad +type bitvector 'a = mword 'a + 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 @@ -13,6 +15,13 @@ 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 +val MEMea : forall 'r 'a 'e. Size 'a => bitvector 'a -> integer -> M 'r unit 'e +val MEMea_release : forall 'r 'a 'e. Size 'a => bitvector 'a -> integer -> M 'r unit 'e +val MEMea_strong_release : forall 'r 'a 'e. Size 'a => bitvector 'a -> integer -> M 'r unit 'e +val MEMea_conditional : forall 'r 'a 'e. Size 'a => bitvector 'a -> integer -> M 'r unit 'e +val MEMea_conditional_release : forall 'r 'a 'e. Size 'a => bitvector 'a -> integer -> M 'r unit 'e +val MEMea_conditional_strong_release : forall 'r 'a 'e. Size 'a => bitvector 'a -> integer -> M 'r unit 'e + 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 @@ -21,26 +30,35 @@ let MEMea_conditional_release addr size = write_mem_ea Write_RISCV_conditional_ let MEMea_conditional_strong_release addr size = write_mem_ea Write_RISCV_conditional_strong_release addr size +val write_ram : forall 'a 'b 'r 'e. Size 'a, Size 'b => + integer -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b -> M 'r unit 'e let write_ram addrsize size hexRAM address value = write_mem_ea Write_plain address size >> write_mem_val value >>= fun _ -> return () +val read_ram : forall 'a 'b 'r 'e. Size 'a, Size 'b => + integer -> integer -> bitvector 'a -> bitvector 'a -> M 'r (bitvector 'b) 'e let read_ram addrsize size hexRAM address = read_mem Read_plain address size let speculate_conditional_success () = excl_result () +val get_slice_int : forall 'a. Size 'a => integer -> integer -> integer -> bitvector 'a let get_slice_int len n lo = (* TODO: Is this the intended behaviour? *) let hi = lo + len - 1 in let bits = bits_of_int (hi + 1) n in of_bits (get_bits false bits hi lo) +val sign_extend : forall 'a 'b. Size 'a, Size 'b => bitvector 'a -> integer -> bitvector 'b let sign_extend v len = exts_vec len v +val zero_extend : forall 'a 'b. Size 'a, Size 'b => bitvector 'a -> integer -> bitvector 'b let zero_extend v len = extz_vec len v +val shift_bits_right : forall 'a 'b. Size 'a, Size 'b => bitvector 'a -> bitvector 'b -> bitvector 'a let shift_bits_right v m = shiftr v (unsigned m) +val shift_bits_left : forall 'a 'b. Size 'a, Size 'b => bitvector 'a -> bitvector 'b -> bitvector 'a let shift_bits_left v m = shiftl v (unsigned m) val prerr_endline : string -> unit @@ -50,7 +68,7 @@ declare ocaml target_rep function prerr_endline = `prerr_endline` val print_int : string -> integer -> unit let print_int msg i = prerr_endline (msg ^ (stringFromInteger i)) -val print_bits : forall 'a. Bitvector 'a => string -> 'a -> unit +val print_bits : forall 'a. Size 'a => string -> bitvector 'a -> unit let print_bits msg bs = prerr_endline (msg ^ (show_bitlist (bits_of bs))) val putchar : integer -> unit |