[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 #6 from Cesar Strauss <cestrauss at gmail.com> ---
(In reply to Luke Kenneth Casson Leighton from comment #5)
> or, are you speaking of turning the for-loops around (on their head), such
> that you start from the *lengths* (and positions) and perform the Assert on
> the resultant partition bits?  that would be interesting.

That's the idea, yes.
Only, since partition bits are inputs, we use Assume, not Assert.
We do Assert the result.

> 
> in other words, you have patterns as follows:
> 
>   8-bit offsets 0,1,2,3
>   16-bit offsets 0,1,2
>   24-bit offsets 0,1
>   32-bit
> 
> * for 8-bit the partition bit between the two must be zero
> * for 16-bit the partition bit at the offset must be 1 and the partition bit
>   after it must be zero
> * for 24-bit the partition bits at the offset and at offset+1 must be 1 and
> at
>   offset+2 must be zero
> * for 32-bit the 3 bits must be 1 and you run out of partition bits to test
> for zero

Exactly.

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/

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.

> this would be efficient/effective in that things being tested (arith) would
> only be tested once.
> 
> interesting.  and it has the advantage that "it's not the same underlying
> algorithm as the code it's testing" which is always a good thing.

Indeed.

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