[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