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

[bugzilla-daemon at libre-soc.org]

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

            Bug ID: 565
           Summary: Improve formal verification on PartitionedSignal
           Product: Libre-SOC's first SoC
           Version: unspecified
          Hardware: PC
               URL: https://lists.libre-soc.org/pipermail/libre-soc-dev/20
                    21-January/001811.html
                OS: Linux
            Status: IN_PROGRESS
          Severity: enhancement
          Priority: ---
         Component: Formal Verification
          Assignee: cestrauss at gmail.com
          Reporter: cestrauss at gmail.com
                CC: libre-soc-bugs at lists.libre-soc.org
   NLnet milestone: ---

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.

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

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

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