diff options
Diffstat (limited to 'verilog/Archi.v')
| -rw-r--r-- | verilog/Archi.v | 21 |
1 files changed, 15 insertions, 6 deletions
diff --git a/verilog/Archi.v b/verilog/Archi.v index 8f1ccdef..f801110a 100644 --- a/verilog/Archi.v +++ b/verilog/Archi.v @@ -7,10 +7,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) @@ -29,7 +30,9 @@ Definition align_float64 := 4%Z. Definition splitlong := false. Lemma splitlong_ptr32: splitlong = true -> ptr64 = false. -Proof. discriminate. Qed. +Proof. + unfold splitlong. destruct ptr64; simpl; congruence. +Qed. Definition default_nan_64 := (true, iter_nat 51 _ xO xH). Definition default_nan_32 := (true, iter_nat 22 _ xO xH). @@ -56,8 +59,14 @@ Definition fma_invalid_mul_is_nan := false. Definition float_of_single_preserves_sNaN := false. +Definition float_conversion_default_nan := false. + +(** Which ABI to use. *) +Parameter win64: bool. (* Always false in 32 bits *) + Global Opaque ptr64 big_endian splitlong default_nan_64 choose_nan_64 default_nan_32 choose_nan_32 fma_order fma_invalid_mul_is_nan - float_of_single_preserves_sNaN. + float_of_single_preserves_sNaN + float_conversion_default_nan. |