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 1118bd444b59f643f182ed960d445a11b0c121ca..8d22374615cd3d604c1eefc8c6a477e82ae2f9c6 100644 (file)
--- 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]))