From: Michael Nolan <mtnolan2640@gmail.com>
Date: Thu, 6 Feb 2020 02:06:49 +0000 (-0500)
Subject: Add 0 assertions to the proof for eq_gt_ge
X-Git-Tag: ls180-24jan2020~260
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=773bd0b8343b65483a0c3c31ab8ca9d2e7c5bad7;p=ieee754fpu.git

Add 0 assertions to the proof for eq_gt_ge
---

diff --git a/src/ieee754/part_cmp/formal/proof_eq_gt_ge.py b/src/ieee754/part_cmp/formal/proof_eq_gt_ge.py
index 1118bd44..8d223746 100644
--- a/src/ieee754/part_cmp/formal/proof_eq_gt_ge.py
+++ b/src/ieee754/part_cmp/formal/proof_eq_gt_ge.py
@@ -58,17 +58,21 @@ class EqualsDriver(Elaboratable):
             with m.Switch(gates):
                 with m.Case(0b00):
                     comb += Assert(out[0] == (a == b))
+                    comb += Assert(out[1] == 0)
+                    comb += Assert(out[2] == 0)
                 with m.Case(0b01):
+                    comb += Assert(out[0] == (a_intervals[0] == b_intervals[0]))
                     comb += Assert(out[1] == ((a_intervals[1] == \
                                     b_intervals[1]) &
                                               (a_intervals[2] == \
                                     b_intervals[2])))
-                    comb += Assert(out[0] == (a_intervals[0] == b_intervals[0]))
+                    comb += Assert(out[2] == 0)
                 with m.Case(0b10):
                     comb += Assert(out[0] == ((a_intervals[0] == \
                                     b_intervals[0]) &
                                               (a_intervals[1] == \
                                     b_intervals[1])))
+                    comb += Assert(out[1] == 0)
                     comb += Assert(out[2] == (a_intervals[2] == b_intervals[2]))
                 with m.Case(0b11):
                     for i in range(mwidth-1):
@@ -77,7 +81,7 @@ class EqualsDriver(Elaboratable):
         with m.If(opcode == 0b01):
             with m.Switch(gates):
                 with m.Case(0b00):
-                    comb += Assert(out[0] == (a > b))
+                    comb += Assert(out == (a > b))
                 with m.Case(0b01):
                     comb += Assert(out[0] == (a_intervals[0] > b_intervals[0]))
 
@@ -96,7 +100,7 @@ class EqualsDriver(Elaboratable):
         with m.If(opcode == 0b10):
             with m.Switch(gates):
                 with m.Case(0b00):
-                    comb += Assert(out[0] == (a >= b))
+                    comb += Assert(out == (a >= b))
                 with m.Case(0b01):
                     comb += Assert(out[0] == (a_intervals[0] >= b_intervals[0]))