diff options
| -rw-r--r-- | mips/run_embed.ml | 1 | ||||
| -rw-r--r-- | src/gen_lib/sail_values.ml | 12 |
2 files changed, 11 insertions, 2 deletions
diff --git a/mips/run_embed.ml b/mips/run_embed.ml index 0386c981..e967eb1c 100644 --- a/mips/run_embed.ml +++ b/mips/run_embed.ml @@ -74,6 +74,7 @@ let args = [ ("--max_instruction", Arg.Int (fun i -> max_cut_off := true; max_instr := i), "only run i instructions, then stop"); ("--trace", Arg.Set trace_writes, "trace all register writes"); (* trace_writes is in sail_values.ml *) ("--quiet", Arg.Clear interact_print, "suppress trace of PC"); + ("--undef", Arg.String (fun s -> undef_val := bit_of_string s), "value to use for undef (u,0,1)"); ] module type ISA_model = sig diff --git a/src/gen_lib/sail_values.ml b/src/gen_lib/sail_values.ml index 1516c503..7e6f0ae7 100644 --- a/src/gen_lib/sail_values.ml +++ b/src/gen_lib/sail_values.ml @@ -11,6 +11,8 @@ type _bool = vbit type _string = string type _nat = number +let undef_val = ref Vundef + type value = | Vvector of vbit array * int * bool | VvectorR of value array * int * bool @@ -25,6 +27,12 @@ let string_of_bit = function | Vzero -> "0" | Vundef -> "u" +let bit_of_string = function + | "1" -> Vone + | "0" -> Vzero + | "u" -> Vundef + | _ -> failwith "invalid bit value" + let string_of_bit_array a = Array.fold_left (^) "" (Array.map string_of_bit a) let string_of_value = function @@ -509,13 +517,13 @@ let to_vec_inc = to_vec_inc_big let to_vec_dec = to_vec_dec_big let to_vec_undef_int ord len = - let array = Array.make len Vundef in + let array = Array.make len !undef_val in let start = if ord then 0 else len-1 in Vvector(array, start, ord) let to_vec_undef_big ord len = let len = int_of_big_int len in - let array = Array.make len Vundef in + let array = Array.make len !undef_val in let start = if ord then 0 else len-1 in Vvector(array, start, ord) |