15e71489a738b601646cdb6bc2683550e7e58f13
1 # SPDX-License-Identifier: LGPL-3-or-later
2 # Copyright 2021 Jacob Lifshay
4 # Funded by NLnet Assure Programme 2021-02-052, https://nlnet.nl/assure part
5 # of Horizon 2020 EU Programme 957073.
8 from nmigen
.hdl
.ast
import AnyConst
, Assert
9 from nmigen
.hdl
.dsl
import Module
10 from nmutil
.formaltest
import FHDLTestCase
11 from nmutil
.grev
import GRev
, grev
12 from nmigen
.sim
import Delay
13 from nmutil
.sim_util
import do_sim
, hash_256
16 class TestGrev(FHDLTestCase
):
19 width
= 2 ** log2_width
20 dut
= GRev(log2_width
)
21 self
.assertEqual(width
, dut
.width
)
23 def case(inval
, chunk_sizes
):
24 expected
= grev(inval
, chunk_sizes
, log2_width
)
25 with self
.subTest(inval
=hex(inval
), chunk_sizes
=bin(chunk_sizes
),
26 expected
=hex(expected
)):
27 yield dut
.input.eq(inval
)
28 yield dut
.chunk_sizes
.eq(chunk_sizes
)
30 output
= yield dut
.output
31 with self
.subTest(output
=hex(output
)):
32 self
.assertEqual(expected
, output
)
33 for i
, step
in enumerate(dut
._steps
):
34 cur_chunk_sizes
= chunk_sizes
& (2 ** i
- 1)
35 step_expected
= grev(inval
, cur_chunk_sizes
, log2_width
)
37 with self
.subTest(i
=i
, step
=hex(step
),
38 cur_chunk_sizes
=bin(cur_chunk_sizes
),
39 step_expected
=hex(step_expected
)):
40 self
.assertEqual(step
, step_expected
)
43 self
.assertEqual(len(dut
._steps
), log2_width
+ 1)
44 for count
in range(width
+ 1):
45 inval
= (1 << count
) - 1
46 for chunk_sizes
in range(2 ** log2_width
):
47 yield from case(inval
, chunk_sizes
)
49 inval
= hash_256(f
"grev input {i}")
50 inval
&= 2 ** width
- 1
51 chunk_sizes
= hash_256(f
"grev 2 {i}")
52 chunk_sizes
&= 2 ** log2_width
- 1
53 yield from case(inval
, chunk_sizes
)
54 with
do_sim(self
, dut
, [dut
.input, dut
.chunk_sizes
,
56 sim
.add_process(process
)
59 def test_formal(self
):
61 dut
= GRev(log2_width
)
63 m
.submodules
.dut
= dut
64 m
.d
.comb
+= dut
.input.eq(AnyConst(2 ** log2_width
))
65 m
.d
.comb
+= dut
.chunk_sizes
.eq(AnyConst(log2_width
))
66 # actual formal correctness proof is inside the module itself, now
70 if __name__
== "__main__":