Check PartitionedSignal.any().

[ieee754fpu.git] / src / ieee754 / part / formal / proof_partition.py

diff --git a/src/ieee754/part/formal/proof_partition.py b/src/ieee754/part/formal/proof_partition.py
index df1b6f871c15c1cf16e338bb918b3e976d919434..a84a127b8d3e5f37c5193667ef56387ccdaa3386 100644 (file)
--- 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()