aboutsummaryrefslogtreecommitdiff
path: root/test-suite/primitive/float/valid_binary_conv.v
diff options
context:
space:
mode:
authorGuillaume Bertholon2018-07-19 13:33:17 +0200
committerPierre Roux2019-11-01 10:20:23 +0100
commit55d32c9f3a91058f69f34c17c17701d0dc81874d (patch)
tree6f36a173531ae36655d291fb3242e047131fc8ad /test-suite/primitive/float/valid_binary_conv.v
parentcc7dfa82705b64d1cf43408244ef6c7dd930a6e9 (diff)
Add tests for primitive floats with 'vm_compute'
Tests are updated to include VM computations and check for double rounding.
Diffstat (limited to 'test-suite/primitive/float/valid_binary_conv.v')
-rw-r--r--test-suite/primitive/float/valid_binary_conv.v13
1 files changed, 13 insertions, 0 deletions
diff --git a/test-suite/primitive/float/valid_binary_conv.v b/test-suite/primitive/float/valid_binary_conv.v
index ad81e55667..53fad1a74c 100644
--- a/test-suite/primitive/float/valid_binary_conv.v
+++ b/test-suite/primitive/float/valid_binary_conv.v
@@ -18,3 +18,16 @@ Check (eq_refl : valid_binary (Prim2SF denorm) = true).
Check (eq_refl : valid_binary (Prim2SF nan) = true).
Check (eq_refl : valid_binary (Prim2SF two) = true).
Check (eq_refl : valid_binary (Prim2SF half) = true).
+
+Check (eq_refl true <: valid_binary (Prim2SF zero) = true).
+Check (eq_refl true <: valid_binary (Prim2SF neg_zero) = true).
+Check (eq_refl true <: valid_binary (Prim2SF one) = true).
+Check (eq_refl true <: valid_binary (Prim2SF (-one)) = true).
+Check (eq_refl true <: valid_binary (Prim2SF infinity) = true).
+Check (eq_refl true <: valid_binary (Prim2SF neg_infinity) = true).
+Check (eq_refl true <: valid_binary (Prim2SF huge) = true).
+Check (eq_refl true <: valid_binary (Prim2SF tiny) = true).
+Check (eq_refl true <: valid_binary (Prim2SF denorm) = true).
+Check (eq_refl true <: valid_binary (Prim2SF nan) = true).
+Check (eq_refl true <: valid_binary (Prim2SF two) = true).
+Check (eq_refl true <: valid_binary (Prim2SF half) = true).