diff options
Diffstat (limited to 'riscV/ExtValues.v')
-rw-r--r-- | riscV/ExtValues.v | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/riscV/ExtValues.v b/riscV/ExtValues.v index 5e6ebf02..4edd2e3d 100644 --- a/riscV/ExtValues.v +++ b/riscV/ExtValues.v @@ -3,6 +3,18 @@ Require Import Integers. Require Import Values. Require Import Floats. +Definition bits_of_float x := + match x with + | Vfloat f => Vlong (Float.to_bits f) + | _ => Vundef + end. + +Definition bits_of_single x := + match x with + | Vsingle f => Vint (Float32.to_bits f) + | _ => Vundef + end. + Definition bitwise_select_int b vtrue vfalse := Val.or (Val.and (Val.neg b) vtrue) (Val.and (Val.sub b Vone) vfalse). @@ -76,3 +88,8 @@ Proof. rewrite Int64.or_commut. apply Int64.or_zero. Qed. + +(* +Compute (Int.unsigned (Float32.to_bits (Float32.of_int (Int.repr 4200)))). +Compute (Int64.unsigned (Float.to_bits (Float.of_int (Int.repr 4233)))). +*) |