Handle -0 and +0 equals and <

diff --git a/src/ieee754/fpcmp/formal/proof_fpcmp_mod.py b/src/ieee754/fpcmp/formal/proof_fpcmp_mod.py
index 45a978d192e4f1018a2a78a7cf5a7c64d5b650bd..4f3d273ebbff4ea2c5133134383600d14e8c2683 100644 (file)
--- a/src/ieee754/fpcmp/formal/proof_fpcmp_mod.py
+++ b/src/ieee754/fpcmp/formal/proof_fpcmp_mod.py
@@ -50,12 +50,17 @@ class FPCMPDriver(Elaboratable):
 
         a_lt_b = Signal()
 
-        with m.If(a1.s != b1.s):
+        with m.If(a1.is_zero & b1.is_zero):
+            m.d.comb += a_lt_b.eq(0)
+        with m.Elif(a1.s != b1.s):
             m.d.comb += a_lt_b.eq(a1.s > b1.s)
         with m.Elif(a1.s == 0):
-            m.d.comb += a_lt_b.eq(a1.v[0:31] < b1.v[0:31])
+            m.d.comb += a_lt_b.eq(a1.v[0:width-1] < b1.v[0:width-1])
         with m.Else():
-            m.d.comb += a_lt_b.eq(a1.v[0:31] > b1.v[0:31])
+            m.d.comb += a_lt_b.eq(a1.v[0:width-1] > b1.v[0:width-1])
+
+        a_eq_b = Signal()
+        m.d.comb += a_eq_b.eq((a1.v == b1.v) | (a1.is_zero & b1.is_zero))
 
 
         with m.If(a1.is_nan | b1.is_nan):
@@ -63,12 +68,12 @@ class FPCMPDriver(Elaboratable):
         with m.Else():
             with m.Switch(opc):
                 with m.Case(0b10):
-                    m.d.comb += Assert(z1.v == (a1.v == b1.v))
+                    m.d.comb += Assert((z1.v == a_eq_b))
                 with m.Case(0b00):
                     m.d.comb += Assert(z1.v == (a_lt_b))
                 with m.Case(0b01):
-                    m.d.comb += Assert(z1.v == (a_lt_b |
-                                                (a1.v == b1.v)))
+                    m.d.comb += Assert(z1.v == (a_lt_b | a_eq_b))
+        
             
 
 

diff --git a/src/ieee754/fpcmp/fpcmp.py b/src/ieee754/fpcmp/fpcmp.py
index 16405b557d38a603aa2fb98e6cadb788670e6d3d..067642d3723dac8ab5881374703da2e45615dfb9 100644 (file)
--- a/src/ieee754/fpcmp/fpcmp.py
+++ b/src/ieee754/fpcmp/fpcmp.py
@@ -46,13 +46,20 @@ class FPCMPPipeMod(PipeModBase):
         m.d.comb += [a1.v.eq(self.i.a),
                      b1.v.eq(self.i.b)]
 
+        both_zero = Signal()
+        comb += both_zero.eq((a1.v[0:width-1] == 0) &
+                             (b1.v[0:width-1] == 0))
+
         ab_equal = Signal()
-        m.d.comb += ab_equal.eq(a1.v == b1.v)
+        m.d.comb += ab_equal.eq((a1.v == b1.v) | both_zero)
+
         contains_nan = Signal()
         m.d.comb += contains_nan.eq(a1.is_nan | b1.is_nan)
         a_lt_b = Signal()
 
-        # if(a1.s != b1.s):
+        # if(a1.is_zero && b1.is_zero):
+        #    a_lt_b = 0
+        # elif(a1.s != b1.s):
         #    a_lt_b = a1.s > b1.s (a is more negative than b)
         signs_same = Signal()
         comb += signs_same.eq(a1.s > b1.s)
@@ -64,12 +71,13 @@ class FPCMPPipeMod(PipeModBase):
         #         a_lt_b = a[0:31] > b[0:31]
         signs_different = Signal()
         comb += signs_different.eq(Mux(a1.s,
-                                       (a1.v[0:31] > b1.v[0:31]),
-                                       (a1.v[0:31] < b1.v[0:31])))
+                                       (a1.v[0:width-1] > b1.v[0:width-1]),
+                                       (a1.v[0:width-1] < b1.v[0:width-1])))
 
-        comb += a_lt_b.eq(Mux(a1.s == b1.s,
+        comb += a_lt_b.eq(Mux(both_zero, 0,
+                              Mux(a1.s == b1.s,
                               signs_different,
-                              signs_same))    
+                              signs_same)))
 
         no_nan = Signal()
         # switch(opcode):

diff --git a/src/ieee754/fpcmp/test/test_fpcmp_pipe.py b/src/ieee754/fpcmp/test/test_fpcmp_pipe.py
index af0ce9534d8bdbeb0fb12329acb23825c3563f37..cff066efb8edd4a45d9196121bdf2c209f591b2a 100644 (file)
--- a/src/ieee754/fpcmp/test/test_fpcmp_pipe.py
+++ b/src/ieee754/fpcmp/test/test_fpcmp_pipe.py
@@ -3,6 +3,8 @@
 
 from ieee754.fpcmp.pipeline import (FPCMPMuxInOut)
 from ieee754.fpcommon.test.fpmux import runfp
+from ieee754.fpcommon.test.case_gen import run_pipe_fp
+from ieee754.fpcommon.test import unit_test_single
 
 from sfpy import Float16, Float32, Float64
 import math
@@ -32,9 +34,30 @@ def test_fpcmp_le():
     runfp(dut, 32, "test_fpcmp_le", Float32, fpcmp_le,
           n_vals=100, opcode=0b01)
 
+def cornercases():
+    nan = Float32(float('nan')).bits
+    yield nan, Float32(1.0).bits
+    yield Float32(1.0).bits, nan
+    yield nan, nan
+    yield Float32(0.0).bits, Float32(-0.0).bits
+    yield Float32(-0.0).bits, Float32(0.0).bits
+
+def test_fpcmp_cornercases():
+    dut = FPCMPMuxInOut(32, 4)
+    run_pipe_fp(dut, 32, "test_fpcmp_f32_corner_eq", unit_test_single,
+                Float32, cornercases, fpcmp_eq, 5,
+                opcode=0b10)
+    run_pipe_fp(dut, 32, "test_fpcmp_f32_corner_le", unit_test_single,
+                Float32, cornercases, fpcmp_le, 5,
+                opcode=0b01)
+    run_pipe_fp(dut, 32, "test_fpcmp_f32_corner_lt", unit_test_single,
+                Float32, cornercases, fpcmp_lt, 5,
+                opcode=0b00)
+
 
 if __name__ == '__main__':
-    for i in range(50):
-        test_fpcmp_lt()
-        test_fpcmp_eq()
-        test_fpcmp_le()
+    test_fpcmp_cornercases()
+    # for i in range(50):
+    #     test_fpcmp_lt()
+    #     test_fpcmp_eq()
+    #     test_fpcmp_le()