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

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

... that's the problem: we cannot assume that the testing of one partition will
not cause interactions (due to coding mistakes) that result in the corruption
of other partitions.

the way that the inference engines work is to exhaustively search for the
combinations of inputs (and outputs!) that cause a failure.

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.

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

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.

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