[Libre-soc-dev] SimdSignal library
Jacob Lifshay
programmerjake at gmail.com
Fri Oct 1 19:56:39 BST 2021
On Fri, Oct 1, 2021, 05:48 lkcl <luke.leighton at gmail.com> wrote:
> On Fri, Oct 1, 2021 at 11:20 AM Jacob Lifshay <programmerjake at gmail.com>
> wrote:
>
> > 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)
>
> if that approach works 100% for all of the operators that's absolutely
> brilliant,
> and puts a rather large chunk of the available EUR 10,350 into your bank
> account, for very little actual work.
>
well, assuming this works, I think we should set the allocated amount much
lower and use the remaining funds for something that actually takes more
work...how about SimdValue and switch/if? I don't feel comfortable taking a
huge amount of money for just a few days work, just because we
mis-estimated how much work was needed -- i think that would be
irresponsible allocation of funds on our part.
>
> (we're paid for results, not by the hour).
>
> https://bugs.libre-soc.org/show_bug.cgi?id=196
> https://bugs.libre-soc.org/show_bug.cgi?id=565
>
> however it has to be for *PartitionedSignal*... not a new design.
>
> can you do that?
>
sure! adapting the testing code I just wrote to work with PartitionedSignal
should be relatively easy -- mostly accounting for the fact
PartitionedSignal can be partitioned more ways since misaligned and
non-power-of-two-sized lanes are not excluded (even though those lanes
probably aren't very useful for an actual cpu), as well as changing the
padding check to always use the no-padding case.
Jacob
More information about the Libre-soc-dev
mailing list