diff options
| author | Thomas Bauereiss | 2017-11-07 15:39:44 +0000 |
|---|---|---|
| committer | Thomas Bauereiss | 2017-11-07 15:39:44 +0000 |
| commit | a06fef246172dd97d68e4fef77132a375554db73 (patch) | |
| tree | 4f9574e9c9e46c9d7b6ecec349b84943b1ace2d6 /lib | |
| parent | 1dbf01cafae9aba80582754f17d831c8bc11cdba (diff) | |
Add builtin for reversing endianness
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/ocaml_rts/sail_lib.ml | 4 | ||||
| -rw-r--r-- | lib/prelude.sail | 3 |
2 files changed, 7 insertions, 0 deletions
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 (* MSB *) val forall Num 'n, Num 'm, Order 'ord. vector<'n, 'm, 'ord, bit> -> 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 |