[Libre-soc-dev] SimdSignal library

[Cesar Strauss]

Em 01/10/2021 09:47, lkcl escreveu:
> 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?

Just a reminder that, for PartitionedSignal (without padding), there is 
already a somewhat generic operator-based Formal Prover:

https://git.libre-soc.org/?p=ieee754fpu.git;a=blob;f=src/ieee754/part/formal/proof_partition.py;h=f2ef30740d6566774aa6812936ce8a5bdd437727;hb=241b958d034f486c069acdcdd757ce61990c03e7#l324

This single driver function can already handle a comprehensive set of 
logical, bitwise and add/sub/neg operations (shifts and mul are still 
missing).

The approach is to take an arbitrary partition, by choosing its start 
point and size at random. Use "Assume" to ensure it is a whole unbroken 
partition, then shift inputs and outputs down to zero. Loop over all 
possible partition sizes and, if it's the right size, compute the 
expected value, compare with the result, and assert.

Regards,

Cesar