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 38e97f0b31bfa732adf5916e7631ec05e6ee9cce..dd57a87cba55fc92dc7b8ccda16aca68eae3645a 100644 (file)
--- 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 8b22a8620e0238968ef8feaad924854dd59cf31b..7586d8be1e9cf1d6258d88b6ff8881ed156394f3 100644 (file)
--- 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)