[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 #7 from Luke Kenneth Casson Leighton <lkcl at lkcl.net> ---
(In reply to Cesar Strauss from comment #6)

> Only, since partition bits are inputs, we use Assume, not Assert.
> We do Assert the result.

got it.


> Well, only:
> 1) You have the polarity of the gates inverted. For instance, 32-bit is all
> zeros, see https://libre-soc.org/3d_gpu/architecture/dynamic_simd/eq/

yes, you probably noticed i get order/polarity wrong

> 2) I will also check that bit before the offset is 1. For instance, 16-bit
> is 101. Otherwise, you can be actually at the end of a bigger partition.
> 
> 3) I will add two guard bits (= 1) at each end, so 32-bit is not a special
> case.

good idea.  if you can also parameterise the length but keep to smaller lengths
initially, for testing, an O(N^2) algorithm on 64 bit could take some time, and
shift or mul may even run for several hours.

i like the plan, Cesar.

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