From: Cesar Strauss <cestrauss@gmail.com>
Date: Mon, 4 Jan 2021 20:26:35 +0000 (-0300)
Subject: Restart the pattern at partition boundaries
X-Git-Tag: ls180-24jan2020~30
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b5fd7debb7245ce8ed052733721f7efe20b9899c;p=ieee754fpu.git

Restart the pattern at partition boundaries
---

diff --git a/src/ieee754/part/formal/proof_partition.py b/src/ieee754/part/formal/proof_partition.py
index 57abe4a3..25fc1ba4 100644
--- a/src/ieee754/part/formal/proof_partition.py
+++ b/src/ieee754/part/formal/proof_partition.py
@@ -75,8 +75,12 @@ class PartitionedPattern(Elaboratable):
             start = positions[i]
             end = positions[i+1]
             # Propagate from the previous byte, adding one to it
-            comb += self.output[start:end].eq(
-                self.output[last_start:last_end] + 1)
+            with m.If(~gates[i]):
+                comb += self.output[start:end].eq(
+                    self.output[last_start:last_end] + 1)
+            with m.Else():
+                # Unless it's a partition boundary, if so start again
+                comb += self.output[start:end].eq(1)
             last_start = start
             last_end = end
         return m
@@ -93,10 +97,8 @@ class Driver(Elaboratable):
     def elaborate(_):
         m = Module()
         comb = m.d.comb
-        sync = m.d.sync
         width = 64
         mwidth = 8
-        out = Signal(width)
         # Setup partition points and gates
         points = PartitionPoints()
         gates = Signal(mwidth-1)
@@ -106,8 +108,20 @@ class Driver(Elaboratable):
         # Instantiate the partitioned pattern producer
         m.submodules.dut = dut = PartitionedPattern(width, points)
         # Directly check some cases
-        comb += Assert(dut.output == 0x0807060504030201)
-        comb += Cover(1)
+        with m.If(gates == 0):
+            comb += Assert(dut.output == 0x0807060504030201)
+        with m.If(gates == 0b1100101):
+            comb += Assert(dut.output == 0x0101030201020101)
+        with m.If(gates == 0b0001000):
+            comb += Assert(dut.output == 0x0403020104030201)
+        with m.If(gates == 0b0100001):
+            comb += Assert(dut.output == 0x0201050403020101)
+        with m.If(gates == 0b1000001):
+            comb += Assert(dut.output == 0x0106050403020101)
+        with m.If(gates == 0b0000001):
+            comb += Assert(dut.output == 0x0706050403020101)
+        # Make it interesting, by having three partitions
+        comb += Cover(sum(gates) == 3)
         return m