diff options
| author | Robert Norton | 2018-05-09 16:36:54 +0100 |
|---|---|---|
| committer | Robert Norton | 2018-05-09 16:58:19 +0100 |
| commit | cd33f38664c620f1eec5d97bde5b837770e7abbc (patch) | |
| tree | ee69f685f93ef237a59b1587b46c76ced78aa956 /mips/prelude.sail | |
| parent | 680acef72a84b1d3810ffd88c06639bafd1d4b3a (diff) | |
Use latex support for generating cheri documentation and remove sed based hack. Also some minor code cleanups and comments.
Diffstat (limited to 'mips/prelude.sail')
| -rw-r--r-- | mips/prelude.sail | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/mips/prelude.sail b/mips/prelude.sail index aa81175f..152996f1 100644 --- a/mips/prelude.sail +++ b/mips/prelude.sail @@ -87,8 +87,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) @@ -277,6 +283,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) |