From: Luke Kenneth Casson Leighton <lkcl@lkcl.net>
Date: Fri, 17 Dec 2021 21:52:14 +0000 (+0000)
Subject: * moved the grev formal correctness assertions into the module
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5a3eb42f1d6541498d62715b892114e08a9fdfcf;p=nmutil.git

* moved the grev formal correctness assertions into the module
  (under the protection of "if platform == formal")
* moved grev assert on internal variable (dut._steps) inside the
  unit test process() function so that it is after the elaborate()
  which is where ._steps gets created
  (this keeps Grev._steps a private variable for unit tests only)
* added TODO comment about the copyright notice at the top of test_grev.py
---

diff --git a/src/nmutil/grev.py b/src/nmutil/grev.py
index 5ffdfbc..21881c3 100644
--- a/src/nmutil/grev.py
+++ b/src/nmutil/grev.py
@@ -14,6 +14,7 @@ module docstring here, to describe the Grev concept.
 """
 
 from nmigen.hdl.ast import Signal, Mux, Cat
+from nmigen.hdl.ast import Assert
 from nmigen.hdl.dsl import Module
 from nmigen.hdl.ir import Elaboratable
 from nmigen.cli import rtlil
@@ -119,6 +120,18 @@ class GRev(Elaboratable):
         # last layer is also the output
         comb += self.output.eq(step_o)
 
+        if platform != 'formal':
+            return m
+
+        # formal test comparing directly against the (simpler) version
+        m.d.comb += Assert(self.output == grev(self.input,
+                                              self.chunk_sizes,
+                                              self.log2_width))
+        for i, step in enumerate(self._steps):
+            cur_chunk_sizes = self.chunk_sizes & (2 ** i - 1)
+            step_expected = grev(self.input, cur_chunk_sizes, self.log2_width)
+            m.d.comb += Assert(step == step_expected)
+
         return m
 
     def ports(self):
diff --git a/src/nmutil/test/test_grev.py b/src/nmutil/test/test_grev.py
index 18e1917..c13f3cb 100644
--- a/src/nmutil/test/test_grev.py
+++ b/src/nmutil/test/test_grev.py
@@ -1,5 +1,6 @@
 # SPDX-License-Identifier: LGPL-3-or-later
-# See Notices.txt for copyright information
+# XXX - this is insufficient See Notices.txt for copyright information - XXX
+# XXX TODO: add individual copyright
 
 import unittest
 from nmigen.hdl.ast import AnyConst, Assert
@@ -16,7 +17,6 @@ class TestGrev(FHDLTestCase):
         width = 2 ** log2_width
         dut = GRev(log2_width)
         self.assertEqual(width, dut.width)
-        self.assertEqual(len(dut._steps), log2_width + 1)
 
         def case(input, chunk_sizes):
             expected = grev(input, chunk_sizes, log2_width)
@@ -38,6 +38,7 @@ class TestGrev(FHDLTestCase):
                         self.assertEqual(step, step_expected)
 
         def process():
+            self.assertEqual(len(dut._steps), log2_width + 1)
             for count in range(width + 1):
                 input = (1 << count) - 1
                 for chunk_sizes in range(2 ** log2_width):
@@ -49,7 +50,7 @@ class TestGrev(FHDLTestCase):
                 chunk_sizes &= 2 ** log2_width - 1
                 yield from case(input, chunk_sizes)
         with do_sim(self, dut, [dut.input, dut.chunk_sizes,
-                                *dut._steps, dut.output]) as sim:
+                                dut.output]) as sim:
             sim.add_process(process)
             sim.run()
 
@@ -60,12 +61,7 @@ class TestGrev(FHDLTestCase):
         m.submodules.dut = dut
         m.d.comb += dut.input.eq(AnyConst(2 ** log2_width))
         m.d.comb += dut.chunk_sizes.eq(AnyConst(log2_width))
-        m.d.comb += Assert(dut.output == grev(dut.input,
-                                              dut.chunk_sizes, log2_width))
-        for i, step in enumerate(dut._steps):
-            cur_chunk_sizes = dut.chunk_sizes & (2 ** i - 1)
-            step_expected = grev(dut.input, cur_chunk_sizes, log2_width)
-            m.d.comb += Assert(step == step_expected)
+        # actual formal correctness proof is inside the module itself, now
         self.assertFormal(m)