[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
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).


however it has to be for *PartitionedSignal*... not a new design.

can you do that?


More information about the Libre-soc-dev mailing list