projects
/
ieee754fpu.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
| inline |
side by side
(parent:
8a652f6
)
Check PartitionedSignal.any().
author
Cesar Strauss
<cestrauss@gmail.com>
Sat, 16 Jan 2021 19:00:28 +0000
(16:00 -0300)
committer
Cesar Strauss
<cestrauss@gmail.com>
Sat, 16 Jan 2021 19:00:28 +0000
(16:00 -0300)
src/ieee754/part/formal/proof_partition.py
patch
|
blob
|
history
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()