From: Cesar Strauss <cestrauss@gmail.com>
Date: Sun, 10 Jan 2021 22:02:01 +0000 (-0300)
Subject: Implement checks for all the rest of the comparison operarions
X-Git-Tag: ls180-24jan2020~9
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0bbad62934298fa33b05b655e9b34a4ab7d58bc0;p=ieee754fpu.git

Implement checks for all the rest of the comparison operarions
---

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()