diff options
Diffstat (limited to 'lib/vector_dec.sail')
| -rw-r--r-- | lib/vector_dec.sail | 29 |
1 files changed, 23 insertions, 6 deletions
diff --git a/lib/vector_dec.sail b/lib/vector_dec.sail index 9ac4d1a5..0e97c237 100644 --- a/lib/vector_dec.sail +++ b/lib/vector_dec.sail @@ -5,8 +5,6 @@ $include <flow.sail> type bits ('n : Int) = vector('n, dec, bit) -val eq_bit = { lem : "eq", _ : "eq_bit" } : (bit, bit) -> bool - val eq_bits = { ocaml: "eq_list", interpreter: "eq_list", @@ -39,6 +37,9 @@ val sail_sign_extend = "sign_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom(' val sail_zero_extend = "zero_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m) +/*! +THIS`(v, n)` truncates `v`, keeping only the _least_ significant `n` bits. + */ val truncate = { ocaml: "vector_truncate", interpreter: "vector_truncate", @@ -47,6 +48,16 @@ val truncate = { c: "sail_truncate" } : forall 'm 'n, 'm >= 0 & 'm <= 'n. (vector('n, dec, bit), atom('m)) -> vector('m, dec, bit) +/*! +THIS`(v, n)` truncates `v`, keeping only the _most_ significant `n` bits. + */ +val truncateLSB = { + ocaml: "vector_truncateLSB", + lem: "vector_truncateLSB", + coq: "vector_truncateLSB", + c: "sail_truncateLSB" +} : forall 'm 'n, 'm >= 0 & 'm <= 'n. (vector('n, dec, bit), atom('m)) -> vector('m, dec, bit) + val sail_mask : forall 'len 'v, 'len >= 0 & 'v >= 0. (atom('len), vector('v, dec, bit)) -> vector('len, dec, bit) function sail_mask(len, v) = if len <= length(v) then truncate(v, len) else sail_zero_extend(v, len) @@ -67,7 +78,7 @@ val bitvector_access = { lem: "access_vec_dec", coq: "access_vec_dec", c: "vector_access" -} : forall ('n : Int), 'n >= 0. (bits('n), int) -> bit +} : forall ('n : Int) ('m : Int), 0 <= 'm < 'n . (bits('n), int('m)) -> bit val plain_vector_access = { ocaml: "access", @@ -85,7 +96,7 @@ val bitvector_update = { lem: "update_vec_dec", coq: "update_vec_dec", c: "vector_update" -} : forall 'n, 'n >= 0. (bits('n), int, bit) -> bits('n) +} : forall 'n 'm, 0 <= 'm < 'n. (bits('n), atom('m), bit) -> bits('n) val plain_vector_update = { ocaml: "update", @@ -93,7 +104,7 @@ val plain_vector_update = { lem: "update_list_dec", coq: "vec_update_dec", c: "vector_update" -} : forall 'n ('a : Type). (vector('n, dec, 'a), int, 'a) -> vector('n, dec, 'a) +} : forall 'n 'm ('a : Type), 0 <= 'm < 'n. (vector('n, dec, 'a), atom('m), 'a) -> vector('n, dec, 'a) overload vector_update = {bitvector_update, plain_vector_update} @@ -130,7 +141,7 @@ val vector_update_subrange = { lem: "update_subrange_vec_dec", c: "vector_update_subrange", coq: "update_subrange_vec_dec" -} : forall 'n 'm 'o. (bits('n), atom('m), atom('o), bits('m - ('o - 1))) -> bits('n) +} : forall 'n 'm 'o, 0 <= 'o <= 'm < 'n. (bits('n), atom('m), atom('o), bits('m - ('o - 1))) -> bits('n) // Some ARM specific builtins @@ -146,6 +157,9 @@ val slice = "slice" : forall 'n 'm 'o, 0 <= 'o < 'm & 'o + 'n <= 'm & 0 <= 'n. val replicate_bits = "replicate_bits" : forall 'n 'm. (bits('n), atom('m)) -> bits('n * 'm) +/*! +converts a bit vector of length $n$ to an integer in the range $0$ to $2^n - 1$. + */ val unsigned = { ocaml: "uint", lem: "uint", @@ -155,6 +169,9 @@ val unsigned = { } : forall 'n. bits('n) -> range(0, 2 ^ 'n - 1) /* We need a non-empty vector so that the range makes sense */ +/*! +converts a bit vector of length $n$ to an integer in the range $-2^{n-1}$ to $2^{n-1} - 1$ using twos-complement. + */ val signed = { c: "sail_signed", _: "sint" |