[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

--- Comment #3 from Luke Kenneth Casson Leighton <lkcl at lkcl.net> ---
(In reply to Cesar Strauss from comment #2)
> New idea: take an arbitrary partition, by choosing its start point and size
> at random. Use "Assume" to ensure it is a whole unbroken partition (start
> and end points are one, with only zeros in between). 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.

unfortunately we have to be careful: ultimately a full permutation proof has to
be done.

perhaps a simpler task would be to first write a "length+offset" proof.  i.e.
to write a proof of a sub-class that turns partitions into "length of partition
plus the offset that it starts from".

this only needs one for-loop:

    for partitionbits in range(1<<partitionlength):
        # analyse partition bits, looking for runs of zeros

if this were expanded out from 32-bit with 3 partition bits, it would produce:

0 0 0 -> 8,0   8,8  8,16  8,24
0 0 1 -> 16,0       8,16  8,24
0 1 0 -> 8,0   16,8       8,24
0 1 1 -> 24,0             8,24
1 0 0 -> 8,0   8,8  16,16
1 0 1 -> 16,0       16,16
1 1 0 -> 8,0   24,8
1 1 1 -> 32,0

a *python* function can analyse the partitionbits and Assert those patterns


    with m.Switch(partitionsignal):
       for partitionbits in range(1<<partitionlength):
           # analyse partition bits, looking for runs of zeros
           l = create_patterns(partitionbits) # above table
           with m.Case(partitionbits):
               # check each pattern from the list

> I suspect it's still O(n^2), but it seems simpler (no nested for loop) in
> spite of some extra setup work.
> 
> To test the above, an idea is to create a partition pattern generator, that
> outputs an unique pattern, depending on partition size.

a for-loop can go through them all, the thing is it doesn't have to be
done manually and by rote like this:

  
https://git.libre-soc.org/?p=ieee754fpu.git;a=blob;f=src/ieee754/part_cmp/formal/proof_gt.py;hb=HEAD

but it *can* be done in a similar way, with the m.Case() being in a for-loop.

    with m.Switch(partitionsignal):
       for partitionbits in range(1<<partitionlength):
           with m.Case(partitionbits):
                Assert(....)

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