1 files changed, 32 insertions, 0 deletions
diff --git a/lib/reverse_endianness.sail b/lib/reverse_endianness.sail
new file mode 100644
index 00000000..ff75f6c3
--- /dev/null
+++ b/lib/reverse_endianness.sail
@@ -0,0 +1,32 @@
+$ifndef _REVERSE_ENDIANNESS
+$define _REVERSE_ENDIANNESS
+
+$ifdef _DEFAULT_DEC
+
+$include <vector_dec.sail>
+
+/* reverse_endianness function set up to ensure it generates good SMT
+definitions. The concat/extract pattern may be less efficient in other
+backends where these are not primitive operations. */
+
+val reverse_endianness : forall 'n, 'n in {8, 16, 32, 64, 128}. bits('n) -> bits('n)
+
+function reverse_endianness(xs) = {
+  let len = length(xs);
+  if len == 8 then {
+    xs
+  } else if len == 16 then {
+    xs[7 .. 0] @ xs[15 .. 8]
+  } else if len == 32 then {
+    xs[7 .. 0] @ xs[15 .. 8] @ xs[23 .. 16] @ xs[31 .. 24]
+  } else if len == 64 then {
+    xs[7 .. 0] @ xs[15 .. 8] @ xs[23 .. 16] @ xs[31 .. 24] @ xs[39 .. 32] @ xs[47 .. 40] @ xs[55 .. 48] @ xs[63 .. 56]
+  } else {
+    xs[7 .. 0] @ xs[15 .. 8] @ xs[23 .. 16] @ xs[31 .. 24] @ xs[39 .. 32] @ xs[47 .. 40] @ xs[55 .. 48] @ xs[63 .. 56]
+    @ xs[71 .. 64] @ xs[79 .. 72] @ xs[87 .. 80] @ xs[95 .. 88] @ xs[103 .. 96] @ xs[111 .. 104] @ xs[119 .. 112] @ xs[127 .. 120]
+  }
+}
+
+$endif
+
+$endif