[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 #2 from Cesar Strauss <cestrauss at gmail.com> ---
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.

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. For instance, on a size
3 partition, it could be: 0x31, 0x32, 0x33. 

(In reply to Luke Kenneth Casson Leighton from comment #1)
> 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".

Sure.

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