From: Cesar Strauss <cestrauss@gmail.com>
Date: Thu, 7 Jan 2021 22:34:20 +0000 (-0300)
Subject: Compare the expected output for all partition sizes
X-Git-Tag: ls180-24jan2020~25
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a080b31887c93fedc6e4879e620e320b81e3c46d;p=ieee754fpu.git

Compare the expected output for all partition sizes

Optimize for the case where the partition points are equally spaced,
so the possible partition sizes are just multiple of the smaller one.
Otherwise, all combinations of start and end points would have to be
considered.
---

diff --git a/src/ieee754/part/formal/proof_partition.py b/src/ieee754/part/formal/proof_partition.py
index bed9e2bc..c8d15a2a 100644
--- a/src/ieee754/part/formal/proof_partition.py
+++ b/src/ieee754/part/formal/proof_partition.py
@@ -194,21 +194,35 @@ class Driver(Elaboratable):
         # Output an example.
         # Make it interesting, by having four partitions.
         # Make the selected partition not start at the very beginning.
-        comb += Cover((sum(gates) == 3) & (p_offset != 0))
+        comb += Cover((sum(gates) == 3) & (p_offset != 0) & (p_width == 3))
+        # Generate and check expected values for all possible partition sizes.
+        # Here, we assume partition sizes are multiple of the smaller size.
+        for w in range(1, mwidth+1):
+            with m.If(p_width == w):
+                # calculate the expected output, for the given bit width
+                bit_width = w * step
+                expected = Signal(bit_width, name=f"expected_{w}")
+                for b in range(w):
+                    # lower nibble is the position
+                    comb += expected[b*8:b*8+4].eq(b+1)
+                    # upper nibble is the partition width
+                    comb += expected[b*8+4:b*8+8].eq(w)
+                # truncate the output, compare and assert
+                comb += Assert(p_output[:bit_width] == expected)
         return m
 
 
 class PartitionTestCase(FHDLTestCase):
     def test_formal(self):
         traces = [
-            ('dut', {'submodule': 'dut'}, [
-                'output[63:0]',
-                ('gates[6:0]', {'base': 'bin'})]),
             ('p_offset[2:0]', {'base': 'dec'}),
             ('p_width[3:0]', {'base': 'dec'}),
             ('p_finish[3:0]', {'base': 'dec'}),
             ('p_gates[8:0]', {'base': 'bin'}),
-            'p_output[63:0]']
+            ('dut', {'submodule': 'dut'}, [
+                ('gates[6:0]', {'base': 'bin'}),
+                'output[63:0]']),
+            'p_output[63:0]', 'expected_3[21:0]']
         write_gtkw(
             'proof_partition_cover.gtkw',
             os.path.dirname(__file__) +