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

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

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

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

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