[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 #36 from Luke Kenneth Casson Leighton <lkcl at lkcl.net> ---
(In reply to Cesar Strauss from comment #35)
> (In reply to Luke Kenneth Casson Leighton from comment #34)
> > (In reply to Cesar Strauss from comment #33)
> > > (In reply to Luke Kenneth Casson Leighton from comment #32)
> > but, really, this is a bug in PartitionedSignal if the inverse fn is not
> > returning a PartitionedSignal.  let me check...
> > 
> > https://git.libre-soc.org/?p=ieee754fpu.git;a=blob;f=src/ieee754/part/
> > partsig.py;h=728764e77f972d75ba0229f4d5e2e821a059ea78;
> > hb=54ebe54bb3dceacfddf376a73088896daf900bc6#l65
> > 
> > yep that is a bug, it should be return PartitionedSignal(~self.sig,
> > self.partpoints)
> 
> Well, you may notice that every arithmetic/logical/shift operation is
> returning Signal instead of PartitionedSignal, not just inverse. Should we
> fix them all?

arg!  yes :)


> On the other hand, partition-like outputs (results from comparisons, any,
> all, xor) should be kept as Signals, right?

actually at some point it may be necessary to create a "PartitionSignal"
class for them, or a "PartitionedBool" class might be more accurate.

in effect, partition-like outputs are also a PartitionedSignal, it's just
that the bitwidth of each partition is only one bit wide.


> For instance: (pa >= pmin) & (pa <= pmax)
> In the above, "&" is Signal's "and".

this *should* - for now - be ok.  this was why i insisted on the full
bits to be set on boolean tests (RippleMSBDown / RippleLSB).
actually it is related to PMux (parallel mux).

if all the bits are set then anything treated as boolean (pa >= pmin)
is a simple & or | to do these tests and it *should* all "work"

PMux (the parallel version of Mux) is then *DEAD* simple: every single
individual 8-bit group can just be a for-loop:
    for i in range(8):
         output[i] = Mux(test[i], a[i], b[i])

and that's it: no knowledge of the partitions is needed, at all.  if however
they were single-bit then PMux becomes much more complicated: it needs a
RippleLSB before doing the for-loop on the Muxes.


regarding PartitionedBool, this *may* be needed, we will have to see how
things interact when it comes to bool() overrides.


> > > I'll add an optional "solver" parameter to FHDLTestCase.assertFormal().
> 
> Done. As a result, all proofs up to now use the full 64-bit, 8 x 8-bit
> partitions.

star.

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