From: Cesar Strauss <cestrauss@gmail.com>
Date: Sat, 16 Jan 2021 19:00:28 +0000 (-0300)
Subject: Check PartitionedSignal.any().
X-Git-Tag: ls180-24jan2020~3
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0164106c06bcde84079330c5653af8c459264bdf;p=ieee754fpu.git

Check PartitionedSignal.any().
---

diff --git a/src/ieee754/part/formal/proof_partition.py b/src/ieee754/part/formal/proof_partition.py
index df1b6f87..a84a127b 100644
--- a/src/ieee754/part/formal/proof_partition.py
+++ b/src/ieee754/part/formal/proof_partition.py
@@ -555,6 +555,14 @@ class PartitionTestCase(FHDLTestCase):
         self.assertFormal(module, mode="bmc", depth=1)
         self.assertFormal(module, mode="cover", depth=1)
 
+    def test_partsig_any(self):
+
+        def op_any(obj):
+            return obj.any()
+
+        module = ComparisonOpDriver(op_any, nops=1)
+        self.assertFormal(module, mode="bmc", depth=1)
+
 
 if __name__ == '__main__':
     unittest.main()