From 773bd0b8343b65483a0c3c31ab8ca9d2e7c5bad7 Mon Sep 17 00:00:00 2001 From: Michael Nolan Date: Wed, 5 Feb 2020 21:06:49 -0500 Subject: [PATCH] Add 0 assertions to the proof for eq_gt_ge --- src/ieee754/part_cmp/formal/proof_eq_gt_ge.py | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) 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])) -- 2.30.2