diff options
Diffstat (limited to 'verilog/Op.v')
| -rw-r--r-- | verilog/Op.v | 36 |
1 files changed, 36 insertions, 0 deletions
diff --git a/verilog/Op.v b/verilog/Op.v index 16d75426..fde078dc 100644 --- a/verilog/Op.v +++ b/verilog/Op.v @@ -149,6 +149,8 @@ Inductive operation : Type := | Osubf (**r [rd = r1 - r2] *) | Omulf (**r [rd = r1 * r2] *) | Odivf (**r [rd = r1 / r2] *) + | Omaxf (**r [rd = max(r1,r2)] *) + | Ominf (**r [rd = min(r1,r2)] *) | Onegfs (**r [rd = - r1] *) | Oabsfs (**r [rd = abs(r1)] *) | Oaddfs (**r [rd = r1 + r2] *) @@ -198,6 +200,32 @@ Defined. Global Opaque eq_condition eq_addressing eq_operation. +(** Helper function for floating point maximum and minimum operation *) + +Definition float_max f1 f2 := + match Float.compare f1 f2 with + | Some Gt => f1 + | Some Eq | Some Lt| None => f2 + end. + +Definition maxf (v1 v2: val) : val := + match v1, v2 with + | Vfloat f1, Vfloat f2 => Vfloat (float_max f1 f2) + | _, _ => Vundef + end. + +Definition float_min f1 f2 := + match Float.compare f1 f2 with + | Some Lt => f1 + | Some Eq | Some Gt| None => f2 + end. + +Definition minf (v1 v2: val) : val := + match v1, v2 with + | Vfloat f1, Vfloat f2 => Vfloat (float_min f1 f2) + | _, _ => Vundef + end. + (** In addressing modes, offsets are 32-bit signed integers, even in 64-bit mode. The following function checks that an addressing mode is valid, i.e. that the offsets are in range. @@ -392,6 +420,8 @@ Definition eval_operation | Osubf, v1::v2::nil => Some(Val.subf v1 v2) | Omulf, v1::v2::nil => Some(Val.mulf v1 v2) | Odivf, v1::v2::nil => Some(Val.divf v1 v2) + | Omaxf, v1::v2::nil => Some (maxf v1 v2) + | Ominf, v1::v2::nil => Some (minf v1 v2) | Onegfs, v1::nil => Some(Val.negfs v1) | Oabsfs, v1::nil => Some(Val.absfs v1) | Oaddfs, v1::v2::nil => Some(Val.addfs v1 v2) @@ -564,6 +594,8 @@ Definition type_of_operation (op: operation) : list typ * typ := | Osubf => (Tfloat :: Tfloat :: nil, Tfloat) | Omulf => (Tfloat :: Tfloat :: nil, Tfloat) | Odivf => (Tfloat :: Tfloat :: nil, Tfloat) + | Omaxf => (Tfloat :: Tfloat :: nil, Tfloat) + | Ominf => (Tfloat :: Tfloat :: nil, Tfloat) | Onegfs => (Tsingle :: nil, Tsingle) | Oabsfs => (Tsingle :: nil, Tsingle) | Oaddfs => (Tsingle :: Tsingle :: nil, Tsingle) @@ -722,6 +754,8 @@ Proof with (try exact I; try reflexivity). destruct v0; destruct v1... destruct v0; destruct v1... destruct v0; destruct v1... + destruct v0; destruct v1... + destruct v0; destruct v1... destruct v0... destruct v0... destruct v0; destruct v1... @@ -1290,6 +1324,8 @@ Proof. inv H4; inv H2; simpl; auto. inv H4; inv H2; simpl; auto. inv H4; inv H2; simpl; auto. + inv H4; inv H2; simpl; auto. + inv H4; inv H2; simpl; auto. inv H4; simpl; auto. inv H4; simpl; auto. inv H4; inv H2; simpl; auto. |