[Libre-soc-bugs] [Bug 745] OP_TERNARY instruction

[bugzilla-daemon at libre-soc.org]

https://bugs.libre-soc.org/show_bug.cgi?id=745

--- Comment #5 from Luke Kenneth Casson Leighton <lkcl at lkcl.net> ---
(In reply to Jacob Lifshay from comment #4)
> Added formal test for BitwiseLut:
> https://git.libre-soc.org/?p=nmutil.git;a=commitdiff;
> h=878e4c6776203e12abb4cf4e78f6d251121418c1

excellent.  btw the convention for those is that they go
in a directory named "formal" rather than a directory named
"test".

(In reply to Jacob Lifshay from comment #2)
> updated the plan https://bugs.libre-soc.org/show_bug.cgi?id=745#c0
> also, ternary is not a very good name (too generic), imho a better name
> would be ternlog (like x86's instruction) or lut3

lut3's good.  using x86 names... hmmm.

(In reply to Jacob Lifshay from comment #3)
> Added BitwiseLut, which is a generic n-ary bitwise lut -- ternary is just
> BitwiseLut(input_count=3, width=64)
> 
> https://git.libre-soc.org/?p=nmutil.git;a=commitdiff;
> h=3e45917af6e91df910b6fc77d031ee3a656c4116

+                for i in range(self.input_count):
+                    if sel_values[i]:
+                        lut_index |= 2 ** i]

that could simply be done in one line as:

     lut_index.eq(Cat(*sel_values)

also... i'm not really sure this is a correct implementation.  there
are 256 unit tests required: one for each and every 4th input, because
the 4th input (lut) is 8-bit wide and therefore there are 256 possible
values.

also, i'm surprised it works without using Array()
(yes there are shorter ways to do this):

self._lut_underlying_signal = Signal(8)
lut_bits = []
for i in range(len(self._lut_underlying_signal)):
    lut_bits.append(self.lut_underlying_signal[i])
self.lut = Array(lut_bits)

without that dynamic indexing i would not expect it to work,
at all [Array creates a pmux at the back-end].

if it does work then i expect that what you've written is
a re-implementation of pmux (Array) using a lot more lines of
code than is necessary (30 instead of 2)

the whole module should be literally this - really not kidding,
only around 4 lines:

    lut = Array([lut_input[i] for i in range(lut_width)])
    for i in range(input_width):
        output[i].eq(lut[Cat(in1[i], in2[i], in3[i])])

that's it.  that's the entire implementation.


also, what is the Repl() for?  the idea is to take each bit
of the 3 inputs and put each of them through a lut Array
lookup.  the inputs should be of the exact length such that
no use of Repl() is required: that would be an additional
Module()'s job, or the user of this Module's responsibility.

Repl() - a secondary task - complicates both the unit test and the
Formal Correctness Proof because both the unit test and the Formal
Correctness Proof have two tasks to deal with, not one.

[unix philosophy: "do one job and do it well"]

-- 
You are receiving this mail because:
You are on the CC list for the bug.