From a06fef246172dd97d68e4fef77132a375554db73 Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Tue, 7 Nov 2017 15:39:44 +0000 Subject: Add builtin for reversing endianness --- lib/ocaml_rts/sail_lib.ml | 4 ++++ lib/prelude.sail | 3 +++ 2 files changed, 7 insertions(+) (limited to 'lib') diff --git a/lib/ocaml_rts/sail_lib.ml b/lib/ocaml_rts/sail_lib.ml index c550b2ce..20d3e281 100644 --- a/lib/ocaml_rts/sail_lib.ml +++ b/lib/ocaml_rts/sail_lib.ml @@ -376,6 +376,10 @@ let read_ram (addr_size, data_size, hex_ram, addr) = in read_byte data_size +let rec reverse_endianness bits = + if List.length bits <= 8 then bits else + reverse_endianness (drop 8 bits) @ (take 8 bits) + (* FIXME: Casts can't be externed *) let zcast_unit_vec x = [x] diff --git a/lib/prelude.sail b/lib/prelude.sail index b7403057..8cc1b86d 100644 --- a/lib/prelude.sail +++ b/lib/prelude.sail @@ -126,6 +126,9 @@ val extern forall Num 'n, Num 'l, Order 'ord. vector<'n,'l,'ord,bit> -> list -> bit effect pure most_significant +(* Endianness *) +val extern forall Num 'n, Num 'm, Order 'ord. vector<'n, 8 * 'm, 'ord, bit> -> vector<'n, 8 * 'm, 'ord, bit> effect pure reverse_endianness + (* List functions *) val extern forall Type 'a. (int, list<'a>) -> list<'a> effect pure list_take -- cgit v1.2.3