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