[Libre-soc-dev] SimdSignal library

Jacob Lifshay programmerjake at gmail.com
Fri Oct 1 11:20:21 BST 2021

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!


More information about the Libre-soc-dev mailing list