From: Cesar Strauss <cestrauss@gmail.com>
Date: Sun, 10 Jan 2021 20:28:23 +0000 (-0300)
Subject: Factor-out the code to make equally spaced partition points
X-Git-Tag: ls180-24jan2020~14
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=feadebe6551a27c63899563d430135775982be5b;p=ieee754fpu.git

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 1357e516..54c9f98f 100644
--- 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 ba222a86..bc464d8a 100644
--- 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 ed000b42..c8d527f9 100644
--- 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