1 # Proof of correctness for partitioned equal signal combiner
2 # Copyright (C) 2020 Michael Nolan <mtnolan2640@gmail.com>
4 from nmigen import Module, Signal, Elaboratable, Mux
5 from nmigen.asserts import Assert, AnyConst, Assume
6 from nmutil.formaltest import FHDLTestCase
7 from nmigen.cli import rtlil
9 from ieee754.part_cmp.gt_combiner import GTCombiner
10 import unittest
13 # This defines a module to drive the device under test and assert
14 # properties about its outputs
15 class CombinerDriver(Elaboratable):
16 def __init__(self):
17 # inputs and outputs
18 pass
20 def elaborate(self, platform):
21 m = Module()
22 comb = m.d.comb
23 width = 3
25 # setup the inputs and outputs of the DUT as anyconst
26 eqs = Signal(width)
27 gts = Signal(width)
28 gates = Signal(width-1)
29 out = Signal(width)
30 aux_input = Signal()
31 gt_en = Signal()
32 comb += [eqs.eq(AnyConst(width)),
33 gates.eq(AnyConst(width)),
34 gts.eq(AnyConst(width)),
35 aux_input.eq(AnyConst(1)),
36 gt_en.eq(AnyConst(1))]
39 m.submodules.dut = dut = GTCombiner(width)
42 # If the aux_input is 0, then this should work exactly as
43 # described in
44 # https://libre-riscv.org/3d_gpu/architecture/dynamic_simd/gt/
45 # except for 2 gate bits, not 3
46 with m.If((aux_input == 0) & (gt_en == 1)):
47 with m.Switch(gates):
48 with m.Case(0b11):
49 for i in range(out.width):
50 comb += Assert(out[i] == gts[i])
51 with m.Case(0b10):
52 comb += Assert(out[2] == gts[2])
53 comb += Assert(out[1] == (gts[1] | (eqs[1] & gts[0])))
54 with m.Case(0b01):
55 comb += Assert(out[2] == (gts[2] | (eqs[2] & gts[1])))
56 comb += Assert(out[0] == gts[0])
57 with m.Case(0b00):
58 comb += Assert(out[2] == (gts[2] | (eqs[2] & (gts[1] | (eqs[1] & gts[0])))))
59 # With the aux_input set to 1, this should work similarly to
60 # eq_combiner. It appears this is the case, however the
61 # ungated inputs are not set to 0 like they are in eq
62 with m.Elif((aux_input == 1) & (gt_en == 0)):
63 with m.Switch(gates):
64 with m.Case(0b11):
65 for i in range(out.width):
66 comb += Assert(out[i] == eqs[i])
67 with m.Case(0b00):
68 comb += Assert(out[2] == (eqs[0] & eqs[1] & eqs[2]))
69 with m.Case(0b10):
70 comb += Assert(out[1] == (eqs[0] & eqs[1]))
71 comb += Assert(out[2] == eqs[2])
72 with m.Case(0b01):
73 comb += Assert(out[0] == eqs[0])
74 comb += Assert(out[2] == (eqs[1] & eqs[2]))
78 # connect up the inputs and outputs.
79 comb += dut.eqs.eq(eqs)
80 comb += dut.gts.eq(gts)
81 comb += dut.gates.eq(gates)
82 comb += dut.aux_input.eq(aux_input)
83 comb += dut.gt_en.eq(gt_en)
84 comb += out.eq(dut.outputs)
86 return m
88 class GTCombinerTestCase(FHDLTestCase):
89 def test_gt_combiner(self):
90 module = CombinerDriver()
91 self.assertFormal(module, mode="bmc", depth=4)
92 def test_ilang(self):
93 dut = GTCombiner(3)
94 vl = rtlil.convert(dut, ports=dut.ports())
95 with open("gt_combiner.il", "w") as f:
96 f.write(vl)
99 if __name__ == '__main__':
100 unittest.main()