diff options
| author | Thomas Bauereiss | 2018-05-11 12:04:10 +0100 |
|---|---|---|
| committer | Thomas Bauereiss | 2018-05-11 12:04:10 +0100 |
| commit | ff18bac6654a73cedf32a45ee406fe3e74ae3efd (patch) | |
| tree | ed940ea575c93d741c84cd24cd3e029d0a590b81 /mips/prelude.sail | |
| parent | 823fe1d82e753add2d54ba010689a81af027ba6d (diff) | |
| parent | db3b6d21c18f4ac516c2554db6890274d2b8292c (diff) | |
Merge branch 'sail2' into cheri-mono
In order to use up-to-date sequential CHERI model for test suite
Diffstat (limited to 'mips/prelude.sail')
| -rw-r--r-- | mips/prelude.sail | 17 |
1 files changed, 13 insertions, 4 deletions
diff --git a/mips/prelude.sail b/mips/prelude.sail index 281ef5ea..5bb79f97 100644 --- a/mips/prelude.sail +++ b/mips/prelude.sail @@ -90,8 +90,14 @@ function or_vec (xs, ys) = builtin_or_vec(xs, ys) overload operator | = {or_bool, or_vec} +/*! +The \function{unsigned} function converts a bit vector to an integer assuming an unsigned representation: +*/ val unsigned = {ocaml: "uint", lem: "uint"} : forall 'n. bits('n) -> range(0, 2 ^ 'n - 1) +/*! +The \function{signed} function converts a bit vector to an integer assuming a signed twos-complement representation: +*/ val signed = {ocaml: "sint", lem: "sint"} : forall 'n. bits('n) -> range(- (2 ^ ('n - 1)), 2 ^ ('n - 1) - 1) val "get_slice_int" : forall 'w. (atom('w), int, int) -> bits('w) @@ -245,10 +251,10 @@ infix 4 >=_s infix 4 <_u infix 4 >=_u -val operator <_s = {lem: "slt_vec"} : forall 'n. (bits('n), bits('n)) -> bool -val operator >=_s = {lem: "sgteq_vec"} : forall 'n. (bits('n), bits('n)) -> bool -val operator <_u = {lem: "ult_vec"} : forall 'n. (bits('n), bits('n)) -> bool -val operator >=_u = {lem: "ugteq_vec"} : forall 'n. (bits('n), bits('n)) -> bool +val operator <_s : forall 'n. (bits('n), bits('n)) -> bool +val operator >=_s : forall 'n. (bits('n), bits('n)) -> bool +val operator <_u : forall 'n. (bits('n), bits('n)) -> bool +val operator >=_u : forall 'n. (bits('n), bits('n)) -> bool function operator <_s (x, y) = signed(x) < signed(y) function operator >=_s (x, y) = signed(x) >= signed(y) @@ -286,6 +292,9 @@ val operator *_s = "mults_vec" : forall 'n . (bits('n), bits('n)) -> bits(2 * 'n infix 7 *_u val operator *_u = "mult_vec" : forall 'n . (bits('n), bits('n)) -> bits(2 * 'n) +/*! +\function{to\_bits} converts an integer to a bit vector of given length. If the integer is negative a twos-complement representation is used. If the integer is too large (or too negative) to fit in the requested length then it is truncated to the least significant bits. +*/ val to_bits : forall 'l.(atom('l), int) -> bits('l) function to_bits (l, n) = get_slice_int(l, n, 0) |