[Libre-soc-dev] SimdSignal library

lkcl luke.leighton at gmail.com
Fri Oct 1 13:47:58 BST 2021


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.

(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?

l.



More information about the Libre-soc-dev mailing list