Flesh out the formal proof for fmax

diff --git a/src/ieee754/fpmax/formal/proof_fmax_mod.py b/src/ieee754/fpmax/formal/proof_fmax_mod.py
index 386cd0fdd27c8d5fc5c72b9f9c6a52236262b278..5471eee664f21fcef37d22fd02e728d998609e93 100644 (file)
--- a/src/ieee754/fpmax/formal/proof_fmax_mod.py
+++ b/src/ieee754/fpmax/formal/proof_fmax_mod.py
@@ -1,7 +1,7 @@
 # Proof of correctness for FPMAX module
 # Copyright (C) 2020 Michael Nolan <mtnolan2640@gmail.com>
 
-from nmigen import Module, Signal, Elaboratable
+from nmigen import Module, Signal, Elaboratable, Cat, Mux
 from nmigen.asserts import Assert, Assume
 from nmigen.cli import rtlil
 
@@ -26,6 +26,7 @@ class FPMAXDriver(Elaboratable):
     def elaborate(self, platform):
         m = Module()
 
+        width = self.pspec.width
         m.submodules.dut = dut = FPMAXPipeMod(self.pspec)
 
         a1 = FPNumBaseRecord(self.pspec.width, False)
@@ -41,6 +42,28 @@ class FPMAXDriver(Elaboratable):
 
         m.d.comb += Assert((z1.v == a1.v) | (z1.v == b1.v) | (z1.v == a1.fp.nan2(0)))
 
+        with m.If(a1.is_nan & b1.is_nan):
+            m.d.comb += Assert(z1.is_nan)
+        with m.Elif(a1.is_nan & ~b1.is_nan):
+            m.d.comb += Assert(z1.v == b1.v)
+        with m.Elif(b1.is_nan & ~a1.is_nan):
+            m.d.comb += Assert(z1.v == a1.v)
+        with m.Else():
+            isrhs = Signal()
+            # if a1 is negative and b1 isn't, then we should return b1
+            with m.If(a1.s != b1.s):
+                m.d.comb += isrhs.eq(a1.s > b1.s)
+            with m.Else():
+                # if they both have the same sign
+                gt = Signal()
+                m.d.comb += gt.eq(self.a[0:width-1] < self.b[0:width-1])
+                m.d.comb += isrhs.eq(gt ^ a1.s)
+
+            with m.If(self.opc == 0):
+                m.d.comb += Assert(z1.v ==
+                                   Mux(self.opc[0] ^ isrhs,
+                                       b1.v, a1.v))
+
         # connect up the inputs and outputs. I think these could
         # theoretically be $anyconst/$anysync but I'm not sure nmigen
         # has support for that