From 0bbad62934298fa33b05b655e9b34a4ab7d58bc0 Mon Sep 17 00:00:00 2001 From: Cesar Strauss Date: Sun, 10 Jan 2021 19:02:01 -0300 Subject: [PATCH] Implement checks for all the rest of the comparison operarions --- src/ieee754/part/formal/proof_partition.py | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/src/ieee754/part/formal/proof_partition.py b/src/ieee754/part/formal/proof_partition.py index 4df92e7f..f257d024 100644 --- a/src/ieee754/part/formal/proof_partition.py +++ b/src/ieee754/part/formal/proof_partition.py @@ -491,6 +491,26 @@ class PartitionTestCase(FHDLTestCase): self.assertFormal(module, mode="bmc", depth=1) self.assertFormal(module, mode="cover", depth=1) + def test_partsig_ne(self): + module = ComparisonOpDriver(operator.ne, 64, 8) + self.assertFormal(module, mode="bmc", depth=1) + + def test_partsig_gt(self): + module = ComparisonOpDriver(operator.gt, 64, 8) + self.assertFormal(module, mode="bmc", depth=1) + + def test_partsig_ge(self): + module = ComparisonOpDriver(operator.ge, 64, 8) + self.assertFormal(module, mode="bmc", depth=1) + + def test_partsig_lt(self): + module = ComparisonOpDriver(operator.lt, 64, 8) + self.assertFormal(module, mode="bmc", depth=1) + + def test_partsig_le(self): + module = ComparisonOpDriver(operator.le, 64, 8) + self.assertFormal(module, mode="bmc", depth=1) + if __name__ == '__main__': unittest.main() -- 2.30.2