From 16d4cdd1f0e4057bc60fa70197a95f1dc3d0a418 Mon Sep 17 00:00:00 2001 From: Cesar Strauss Date: Mon, 4 Jan 2021 18:38:51 -0300 Subject: [PATCH] Work only with nibbles on the ascending cascade --- src/ieee754/part/formal/proof_partition.py | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/src/ieee754/part/formal/proof_partition.py b/src/ieee754/part/formal/proof_partition.py index 361ff56d..5388d322 100644 --- a/src/ieee754/part/formal/proof_partition.py +++ b/src/ieee754/part/formal/proof_partition.py @@ -69,20 +69,22 @@ class PartitionedPattern(Elaboratable): # Begin counting at one last_start = positions[0] last_end = positions[1] - comb += self.output[last_start:last_end].eq(1) + last_middle = (last_start+last_end)//2 + comb += self.output[last_start:last_middle].eq(1) # Build an incrementing cascade for i in range(1, self.mwidth): start = positions[i] end = positions[i+1] + middle = (start + end) // 2 # Propagate from the previous byte, adding one to it. with m.If(~gates[i]): - comb += self.output[start:end].eq( - self.output[last_start:last_end] + 1) + comb += self.output[start:middle].eq( + self.output[last_start:last_middle] + 1) with m.Else(): # ... unless it's a partition boundary. If so, start again. - comb += self.output[start:end].eq(1) + comb += self.output[start:middle].eq(1) last_start = start - last_end = end + last_middle = middle # Mirror the nibbles on the last byte last_start = positions[-2] last_end = positions[-1] @@ -102,7 +104,6 @@ class PartitionedPattern(Elaboratable): # If so, mirror the nibbles again. comb += self.output[middle:end].eq( self.output[start:middle]) - last_start = start last_middle = middle last_end = end -- 2.30.2