From: Michael Nolan <mtnolan2640@gmail.com>
Date: Sun, 2 Feb 2020 16:42:17 +0000 (-0500)
Subject: Handle NaNs for FPCMP
X-Git-Tag: ls180-24jan2020~297
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=82c8d40790f5ad9112fa4f1270fdc2e1616a5bdb;p=ieee754fpu.git

Handle NaNs for FPCMP
---

diff --git a/src/ieee754/fpcmp/formal/proof_fpcmp_mod.py b/src/ieee754/fpcmp/formal/proof_fpcmp_mod.py
index 38e97f0b..dd57a87c 100644
--- a/src/ieee754/fpcmp/formal/proof_fpcmp_mod.py
+++ b/src/ieee754/fpcmp/formal/proof_fpcmp_mod.py
@@ -48,9 +48,12 @@ class FPCMPDriver(Elaboratable):
 
         m.d.comb += Assert((z1.v == 0) | (z1.v == 1))
 
-        with m.Switch(opc):
-            with m.Case(0b10):
-                m.d.comb += Assert(z1.v == (a1.v == b1.v))
+        with m.If(a1.is_nan | b1.is_nan):
+            m.d.comb += Assert(z1.v == 0)
+        with m.Else():
+            with m.Switch(opc):
+                with m.Case(0b10):
+                    m.d.comb += Assert(z1.v == (a1.v == b1.v))
             
 
 
@@ -68,7 +71,7 @@ class FPCMPDriver(Elaboratable):
 
 
 class FPCMPTestCase(FHDLTestCase):
-    def test_max(self):
+    def test_fpcmp(self):
         for bits in [16, 32, 64]:
             module = FPCMPDriver(PipelineSpec(bits, 2, 2))
             self.assertFormal(module, mode="bmc", depth=4)
diff --git a/src/ieee754/fpcmp/fpcmp.py b/src/ieee754/fpcmp/fpcmp.py
index 8b22a862..7586d8be 100644
--- a/src/ieee754/fpcmp/fpcmp.py
+++ b/src/ieee754/fpcmp/fpcmp.py
@@ -48,10 +48,15 @@ class FPCMPPipeMod(PipeModBase):
 
         ab_equal = Signal()
         m.d.comb += ab_equal.eq(a1.v == b1.v)
+        contains_nan = Signal()
+        m.d.comb += contains_nan.eq(a1.is_nan | b1.is_nan)
 
-        with m.Switch(opcode):
-            with m.Case(0b10):
-                comb += z1.eq(ab_equal)
+        with m.If(contains_nan):
+            m.d.comb += z1.eq(0)
+        with m.Else():
+            with m.Switch(opcode):
+                with m.Case(0b10):
+                    comb += z1.eq(ab_equal)
 
         # copy the context (muxid, operator)
         comb += self.o.ctx.eq(self.i.ctx)