summaryrefslogtreecommitdiff
path: root/src/gen_lib/sail_operators.lem
diff options
context:
space:
mode:
Diffstat (limited to 'src/gen_lib/sail_operators.lem')
-rw-r--r--src/gen_lib/sail_operators.lem18
1 files changed, 18 insertions, 0 deletions
diff --git a/src/gen_lib/sail_operators.lem b/src/gen_lib/sail_operators.lem
index fbe096c9..a760fb42 100644
--- a/src/gen_lib/sail_operators.lem
+++ b/src/gen_lib/sail_operators.lem
@@ -205,6 +205,7 @@ let modulo (l,r) = hardware_mod l r
let quot = hardware_quot
let power (l,r) = integerPow l r
+let add_int = add
let sub_int = sub
let mult_int = mult
@@ -452,6 +453,9 @@ let rec repeat xs n =
let duplicate (bit, length) =
Vector (repeat [bit] length) (length - 1) false
+let replicate_bits (v, count) =
+ Vector (repeat (get_elems v) count) ((length v * count) - 1) false
+
let compare_op op (l,r) = (op l r)
let lt = compare_op (<)
@@ -531,3 +535,17 @@ let make_bitvector_undef length =
let mask' (start, n, Vector bits _ dir) =
let current_size = List.length bits in
Vector (drop (current_size - (natFromInteger n)) bits) start dir
+
+
+(* Register operations *)
+
+let update_reg_range i j reg_val new_val = update reg_val i j new_val
+let update_reg_bit i reg_val bit = update_pos reg_val i bit
+let update_reg_field_range regfield i j reg_val new_val =
+ let current_field_value = regfield.get_field reg_val in
+ let new_field_value = update current_field_value i j new_val in
+ regfield.set_field reg_val new_field_value
+let write_reg_field_bit regfield i reg_val bit =
+ let current_field_value = regfield.get_field reg_val in
+ let new_field_value = update_pos current_field_value i bit in
+ regfield.set_field reg_val new_field_value