[Libre-soc-dev] SimdSignal library
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>
> >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
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
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
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)
More information about the Libre-soc-dev