From f10a3973ec9e4f26fa78eb479fbeacc6caa0dcbf Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Tue, 13 Feb 2018 19:18:34 +0000
Subject: Support for large bitvector literals in C backend

---
 lib/vector_dec.sail | 25 +++++++++++++++++++++++++
 1 file changed, 25 insertions(+)
 create mode 100644 lib/vector_dec.sail

(limited to 'lib')

diff --git a/lib/vector_dec.sail b/lib/vector_dec.sail
new file mode 100644
index 00000000..84493f73
--- /dev/null
+++ b/lib/vector_dec.sail
@@ -0,0 +1,25 @@
+$ifndef _VECTOR_DEC
+$define _VECTOR_DEC
+
+type bits ('n : Int) = vector('n, dec, bit)
+
+val "zeros" : forall 'n. atom('n) -> bits('n)
+
+val "print_bits" : forall 'n. (string, bits('n)) -> unit
+
+val "sign_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m)
+val "zero_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m)
+
+val "append_64" : forall 'n. (bits('n), bits(64)) -> bits('n + 64)
+
+val add_bits = {
+  ocaml: "add_vec",
+  c: "add_bits"
+} : forall 'n. (bits('n), bits('n)) -> bits('n)
+
+val add_bits_int = {
+  ocaml: "add_vec_int",
+  c: "add_bits_int"
+} : forall 'n. (bits('n), int) -> bits('n)
+
+$endif
-- 
cgit v1.2.3