From: Luke Kenneth Casson Leighton 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)