From: Cesar Strauss <cestrauss@gmail.com>
Date: Sun, 10 Jan 2021 21:33:10 +0000 (-0300)
Subject: Generate shifted down input and outputs
X-Git-Tag: ls180-24jan2020~11
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=705b03ab3ecd9fdb7379ffc32c6d3f1ba9ca0d57;p=ieee754fpu.git

Generate shifted down input and outputs
---

diff --git a/src/ieee754/part/formal/proof_partition.py b/src/ieee754/part/formal/proof_partition.py
index d1ba0f80..c2ff89ba 100644
--- a/src/ieee754/part/formal/proof_partition.py
+++ b/src/ieee754/part/formal/proof_partition.py
@@ -354,8 +354,18 @@ class ComparisonOpDriver(Elaboratable):
         comb += gates.eq(gen.gates)
         p_offset = gen.p_offset
         p_width = gen.p_width
+        # generate shifted down inputs and outputs
+        p_output = Signal(mwidth)
+        p_a = Signal(width)
+        p_b = Signal(width)
+        for pos in range(mwidth):
+            with m.If(p_offset == pos):
+                comb += p_output.eq(output[pos:])
+                comb += p_a.eq(a.sig[pos * step:])
+                comb += p_b.eq(b.sig[pos * step:])
         # output a test case
-        comb += Cover((p_offset != 0) & (p_width == 3) & (sum(output) > 1))
+        comb += Cover((p_offset != 0) & (p_width == 3) & (sum(output) > 1) &
+                      (p_a != 0) & (p_b != 0) & (p_output != 0))
         return m
 
 
@@ -440,7 +450,9 @@ class PartitionTestCase(FHDLTestCase):
             ('eq_1', {'submodule': 'eq_1'}, [
                 ('gates[6:0]', 'bin'),
                 'a[63:0]', 'b[63:0]',
-                ('output[7:0]', 'bin')])]
+                ('output[7:0]', 'bin')]),
+            'p_a[63:0]', 'p_b[63:0]',
+            ('p_output[7:0]', 'bin')]
         write_gtkw(
             'proof_partsig_eq_cover.gtkw',
             os.path.dirname(__file__) +