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

bugzilla-daemon at libre-soc.org bugzilla-daemon at libre-soc.org
Sun Jan 3 19:01:42 GMT 2021


--- Comment #4 from Cesar Strauss <cestrauss at gmail.com> ---
(In reply to Luke Kenneth Casson Leighton from comment #3)
> (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.

Maybe not: by letting the formal engine choose the size and offset, I think we
are indeed covering all possible cases. It's just that we test only one
partition at a time (the partition that the formal engine selected) instead of
all, and let the formal engine do the outer loop for us. Reminds me of SIMT.

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

More information about the libre-soc-bugs mailing list