Factor-out the code to make equally spaced partition points

diff --git a/src/ieee754/part/formal/proof_partition.py b/src/ieee754/part/formal/proof_partition.py
index 1357e516d66197a7408051ff636b25af08e09fa0..54c9f98f90c8c3b794a4ec1267a565d51e3fdc62 100644 (file)
--- a/src/ieee754/part/formal/proof_partition.py
+++ b/src/ieee754/part/formal/proof_partition.py
@@ -113,6 +113,19 @@ class PartitionedPattern(Elaboratable):
         return m
 
 
+def make_partitions(step, mwidth):
+    """Make equally spaced partition points
+
+    :param step: smallest partition width
+    :param mwidth: maximum number of partitions
+    :returns: partition points, and corresponding gates"""
+    gates = Signal(mwidth - 1)
+    points = PartitionPoints()
+    for i in range(mwidth-1):
+        points[(i + 1) * step] = gates[i]
+    return points, gates
+
+
 # This defines a module to drive the device under test and assert
 # properties about its outputs
 class Driver(Elaboratable):
@@ -127,11 +140,8 @@ class Driver(Elaboratable):
         width = 64
         mwidth = 8
         # Setup partition points and gates
-        points = PartitionPoints()
-        gates = Signal(mwidth-1)
         step = int(width/mwidth)
-        for i in range(mwidth-1):
-            points[(i+1)*step] = gates[i]
+        points, gates = make_partitions(step, mwidth)
         # Instantiate the partitioned pattern producer
         m.submodules.dut = dut = PartitionedPattern(width, points)
         # Directly check some cases
@@ -278,11 +288,8 @@ class GeneratorDriver(Elaboratable):
         width = 64
         mwidth = 8
         # Setup partition points and gates
-        points = PartitionPoints()
-        gates = Signal(mwidth-1)
         step = int(width/mwidth)
-        for i in range(mwidth-1):
-            points[(i+1)*step] = gates[i]
+        points, gates = make_partitions(step, mwidth)
         # Instantiate the partitioned pattern producer and the DUT
         m.submodules.dut = dut = PartitionedPattern(width, points)
         m.submodules.gen = gen = GateGenerator(mwidth)
@@ -314,14 +321,6 @@ class GeneratorDriver(Elaboratable):
         return m
 
 
-def make_partitions(step, mwidth):
-    gates = Signal(mwidth - 1)
-    points = PartitionPoints()
-    for i in range(mwidth-1):
-        points[(i + 1) * step] = gates[i]
-    return points, gates
-
-
 class ComparisonOpDriver(Elaboratable):
     """Checks comparison operations on partitioned signals"""
     def __init__(self, op, width, mwidth):

diff --git a/src/ieee754/part_cmp/experiments/formal/proof_partitioned_eq.py b/src/ieee754/part_cmp/experiments/formal/proof_partitioned_eq.py
index ba222a86356b744906fe05516ffb7e257e938cdd..bc464d8ab0fc08df3a51b8bdbb27a250a4a68787 100644 (file)
--- a/src/ieee754/part_cmp/experiments/formal/proof_partitioned_eq.py
+++ b/src/ieee754/part_cmp/experiments/formal/proof_partitioned_eq.py
@@ -8,8 +8,7 @@ from nmutil.formaltest import FHDLTestCase
 from nmutil.gtkw import write_gtkw
 from nmutil.ripple import RippleLSB
 
-from ieee754.part_mul_add.partpoints import PartitionPoints
-from ieee754.part.formal.proof_partition import GateGenerator
+from ieee754.part.formal.proof_partition import GateGenerator, make_partitions
 from ieee754.part_cmp.experiments.equal_ortree import PartitionedEq
 
 
@@ -25,11 +24,8 @@ class Driver(Elaboratable):
         width = 64
         mwidth = 8
         # Setup partition points and gates
-        points = PartitionPoints()
-        gates = Signal(mwidth-1)
         step = int(width/mwidth)
-        for i in range(mwidth-1):
-            points[(i+1)*step] = gates[i]
+        points, gates = make_partitions(step, mwidth)
         # instantiate the DUT
         m.submodules.dut = dut = PartitionedEq(width, points)
         # post-process the output to ripple the LSB

diff --git a/src/ieee754/part_cmp/formal/proof_partitioned_eq_gt_ge.py b/src/ieee754/part_cmp/formal/proof_partitioned_eq_gt_ge.py
index ed000b42049ce48264b1d74440b6208900fe2b6c..c8d527f9d37f0e2011394b0718bbbde44a0d3393 100644 (file)
--- a/src/ieee754/part_cmp/formal/proof_partitioned_eq_gt_ge.py
+++ b/src/ieee754/part_cmp/formal/proof_partitioned_eq_gt_ge.py
@@ -8,8 +8,7 @@ from nmutil.formaltest import FHDLTestCase
 from nmutil.gtkw import write_gtkw
 from nmutil.ripple import RippleLSB
 
-from ieee754.part_mul_add.partpoints import PartitionPoints
-from ieee754.part.formal.proof_partition import GateGenerator
+from ieee754.part.formal.proof_partition import GateGenerator, make_partitions
 from ieee754.part_cmp.eq_gt_ge import PartitionedEqGtGe
 
 
@@ -25,11 +24,8 @@ class Driver(Elaboratable):
         width = 64
         mwidth = 8
         # Setup partition points and gates
-        points = PartitionPoints()
-        gates = Signal(mwidth-1)
         step = int(width/mwidth)
-        for i in range(mwidth-1):
-            points[(i+1)*step] = gates[i]
+        points, gates = make_partitions(step, mwidth)
         # instantiate the DUT
         m.submodules.dut = dut = PartitionedEqGtGe(width, points)
         # post-process the output to ripple the LSB