From 25a26dd9a82267e94f6af3a84964f7e4f5eaa03f Mon Sep 17 00:00:00 2001 From: Luke Kenneth Casson Leighton Date: Sat, 16 Jan 2021 19:07:41 +0000 Subject: [PATCH] add first cut at formal proof for PartitionedXOR --- src/ieee754/part/formal/proof_partition.py | 8 ++++++++ src/ieee754/part/partsig.py | 5 +++-- 2 files changed, 11 insertions(+), 2 deletions(-) diff --git a/src/ieee754/part/formal/proof_partition.py b/src/ieee754/part/formal/proof_partition.py index a84a127b..5867cdb9 100644 --- a/src/ieee754/part/formal/proof_partition.py +++ b/src/ieee754/part/formal/proof_partition.py @@ -563,6 +563,14 @@ class PartitionTestCase(FHDLTestCase): module = ComparisonOpDriver(op_any, nops=1) self.assertFormal(module, mode="bmc", depth=1) + def test_partsig_xor(self): + + def op_xor(obj): + return obj.xor() + + module = ComparisonOpDriver(op_xor, nops=1) + self.assertFormal(module, mode="bmc", depth=1) + if __name__ == '__main__': unittest.main() diff --git a/src/ieee754/part/partsig.py b/src/ieee754/part/partsig.py index 168a0e0b..d710b7ff 100644 --- a/src/ieee754/part/partsig.py +++ b/src/ieee754/part/partsig.py @@ -47,7 +47,7 @@ class PartitionedSignal: else: self.partpoints = make_partition(mask, width) self.modnames = {} - for name in ['add', 'eq', 'gt', 'ge', 'ls']: + for name in ['add', 'eq', 'gt', 'ge', 'ls', 'xor']: self.modnames[name] = 0 def set_module(self, m): @@ -304,9 +304,10 @@ class PartitionedSignal: ``1`` if an odd number of bits are set, ``0`` if an even number of bits are set. """ + width = len(self.sig) pa = PartitionedXOR(width, self.partpoints) setattr(self.m.submodules, self.get_modname("xor"), pa) - self.m.d.comb += pa.a.eq(self) + self.m.d.comb += pa.a.eq(self.sig) return pa.output def implies(premise, conclusion): -- 2.30.2