[Libre-soc-dev] SimdSignal library

[Jacob Lifshay]

On Fri, Oct 1, 2021, 02:41 lkcl <luke.leighton at gmail.com> wrote:

> On October 1, 2021 8:06:23 AM UTC, Jacob Lifshay <programmerjake at gmail.com>
> wrote:
> >I write out the list of operations and test time estimates:
> >Note, the following list includes both unit tests and formal proofs
> >(yay SimdValueTester class I just wrote that does both!)
> >SimdCat, SimdRepl: done.
> >SimdValue.bool(): 5min
>
> jacob, it took me about 3 days to do the gate-level analysis for bool xor
> and some, based on prior work on eq ge and lt that was itself around 3
> weeks.
>

I totally agree it will take longer than 5min to *implement* bool and most
other operations on this list, the times I gave are only for writing tests
and formal proofs (since that's what you asked for), nothing else.

><< >> shift_left shift_right rotate_left rotate_right: 10min total
>
> have you included time to analyse and understand the *existing* design?
>

if just writing unit tests and formal (particularly so for formal), you
don't necessarily need to fully understand the design, all you need is to
test it against a known-working implementation, which luckily we have:
nmigen's built-in operators.

>
> >& | ^ implies: 7min total
> >== != < <= > >=: 15min total
> >abs(): 5min
> >slicing: 30min
> >as_unsigned(), as_signed(): 5min
> >any(), all(), xor(): 5min
> >bit_select(), word_select(), SimdPart: 10min
> >matches(): 1hr
> >Mux(): 5min
> >Array(): not supported until we *really* need it...can we skip
> >implementing it?
>
> ohh yes.  it's extremely complex.  it's definitely off the list for a
> first design.
>

:)

>
> >SimdModule.If/Elif/Else: 2-3 days
> >SimdModule.Switch/Case/Default: 4-5 days
> >(not actually writing tests): fixing bugs that are revealed by the
> >tests: a week or two
> >
> >>
> >> > > * formal correctness proofs
> >
> >Included in above estimate, since all we need is to call
> >SimdValueTester.run_formal instead of SimdValueTester.run_sim
>
> Formal tests require a model against which to check.


yup, in this case we can use the known-working model provided by nmigen's
operators. we don't have to write our own.

from experience we know these take almost as long to write as the original
> code.
>

well, not with how I wrote the code -- nmigen does all the hard work of
having operators that function properly that I use as a reference.
Basic summary of formal proof approach I used in SimdValueTester.run_formal:
assign AnyConsts to all dut inputs and SimdPartMode.part_starts
assume SimdPartMode.is_valid
for each possible lane:
    input_bits = extract lane's bits from all dut inputs
    expected = native nmigen operator applied to input_bits
    if lane is active:
        assert lane's bits extracted from dut output == expected
        assert lane is padded correctly (see SimdPaddingKind for full list)

That's it!

Jacob