[Libre-soc-bugs] [Bug 565] Improve formal verification on PartitionedSignal

[bugzilla-daemon at libre-soc.org]

https://bugs.libre-soc.org/show_bug.cgi?id=565

Luke Kenneth Casson Leighton <lkcl at lkcl.net> changed:

           What    |Removed                     |Added
----------------------------------------------------------------------------
    NLnet milestone|---                         |NLNet.2019.10.Formal
           See Also|                            |https://bugs.libre-soc.org/
                   |                            |show_bug.cgi?id=132
    parent task for|                            |196
  budget allocation|                            |
                 CC|                            |lkcl at lkcl.net

--- Comment #1 from Luke Kenneth Casson Leighton <lkcl at lkcl.net> ---
(In reply to Cesar Strauss from comment #0)
> On 01/02/2021 15:42, Luke Kenneth Casson Leighton wrote:
> > we do need formal verification of PartitionedSignal, but in a way that it
> > obvious how it works, so that it is easy to read the proof code.
> 
> I took a look at ieee754fpu/src/ieee754/part* and its proofs. I see what you
> mean.

yes, the propagation across the partition points, when done optimally, is
challenging to understand.

> I think I have an idea.
> 
> The approach is to create nested for loops that will enumerate all possible
> partitions of varying widths and positions. 

this can be done as a python for-loop that adds AST for each case, rather than
an explicit hard-coded switch statement, just like in the Decoder.

> Then, check whether that
> partition is "complete" (delimited by ones on each side) and "unbroken" (all
> zeros inside). If so, compute the expected result, compare and assert.

an option there is to compute all 8-bit results @ offsets 0..N-1
all 16-bit results @ offsets 0..N-2
and so on.

then to "connect" those with the appropriate partition-derived test.

> It's horribly inefficient on resources (O(n^2) I think). Let's hope the
> proof is not too slow.

well, i would expect it to be dreadful for shift and multiply but tolerable for
add, compares, OR etc.  however if the initial tests are only 32-bit and 3
partition points it should complete in reasonable time.

another speed-up trick would be to run multiple tests in parallel, with subsets
of the permutations disallowed.  however... that would only be appropriate for
speeding up testing and development.

also if you can, Cesar, use a higher-order-function (or, plan to add one, as an
iterative incremental development) for the computation of the "thing" and the
"thing to compare against".

the partitioning itself is identically-coded in all cases and it will save
having to repeat the scheme you devised above.  this is important because we
will need to revise some of the eq/etc. code to "propagate" compare/tests
across all bits.  currently eq/gt/lt produce this:

     if a > b return 0b0001 # partition size of 32-bit

where what is actually needed is this:

     if a > b return 0b1111 # one bit set in each partition to indicate "True"

luckily there is a class which performs this job, it propagates the LSB in a
partition, repeated up to the end of a partition.

-- 
You are receiving this mail because:
You are on the CC list for the bug.