From: Michael Nolan <mtnolan2640@gmail.com>
Date: Sun, 2 Feb 2020 17:31:17 +0000 (-0500)
Subject: Add formal proof for FLT and FLE for FPCMP
X-Git-Tag: ls180-24jan2020~295
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f1d967353c0a6ebe1cf2dc2c379cf6a9430c7d82;p=ieee754fpu.git

Add formal proof for FLT and FLE for FPCMP
---

diff --git a/src/ieee754/fpcmp/formal/proof_fpcmp_mod.py b/src/ieee754/fpcmp/formal/proof_fpcmp_mod.py
index dd57a87c..45a978d1 100644
--- a/src/ieee754/fpcmp/formal/proof_fpcmp_mod.py
+++ b/src/ieee754/fpcmp/formal/proof_fpcmp_mod.py
@@ -48,12 +48,27 @@ class FPCMPDriver(Elaboratable):
 
         m.d.comb += Assert((z1.v == 0) | (z1.v == 1))
 
+        a_lt_b = Signal()
+
+        with m.If(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])
+        with m.Else():
+            m.d.comb += a_lt_b.eq(a1.v[0:31] > b1.v[0:31])
+
+
         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))
+                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)))
             
 
 
@@ -72,7 +87,7 @@ class FPCMPDriver(Elaboratable):
 
 class FPCMPTestCase(FHDLTestCase):
     def test_fpcmp(self):
-        for bits in [16, 32, 64]:
+        for bits in [32, 16, 64]:
             module = FPCMPDriver(PipelineSpec(bits, 2, 2))
             self.assertFormal(module, mode="bmc", depth=4)