summaryrefslogtreecommitdiff
path: root/src/gen_lib
diff options
context:
space:
mode:
Diffstat (limited to 'src/gen_lib')
-rw-r--r--src/gen_lib/sail_values.ml11
1 files changed, 11 insertions, 0 deletions
diff --git a/src/gen_lib/sail_values.ml b/src/gen_lib/sail_values.ml
index cc1979a1..945a7c22 100644
--- a/src/gen_lib/sail_values.ml
+++ b/src/gen_lib/sail_values.ml
@@ -333,6 +333,8 @@ let most_significant = function
| Vregister(array,_,_,_,_) -> !array.(0)
| _ -> assert false
+let _most_significant = most_significant
+
let bitwise_not_bit = function
| Vone -> Vzero
| Vzero -> Vone
@@ -1053,6 +1055,15 @@ let duplicate_big (bit,length) =
let duplicate = duplicate_big
+let duplicate_bits_big (bits, x) =
+ let len = (length_int bits) * (int_of_big_int x) in
+ let is_inc = get_ord bits in
+ let bits_arr = get_barray bits in
+ let arr = Array.concat (Array.to_list(Array.make (int_of_big_int x) bits_arr)) in
+ Vvector(arr, (if is_inc then 0 else (len - 1)), is_inc)
+
+let duplicate_bits = duplicate_bits_big
+
let compare_op op (l,r) =
if (op l r)
then Vone