[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 #34 from Luke Kenneth Casson Leighton <lkcl at lkcl.net> ---
(In reply to Cesar Strauss from comment #33)
> (In reply to Luke Kenneth Casson Leighton from comment #32)
> > (In reply to Cesar Strauss from comment #31)
> > > (In reply to Luke Kenneth Casson Leighton from comment #30)
> > > > neg is the next obvious one,
> > > 
> > > For some reason, neg(a) was returning (a-1) instead of (-a). I
> > > re-implemented it as (0-a).
> 
> I have a theory. The test suite for PartitionedSignal has several instances
> of (-a) being calculated as ~(a-1), which is correct, even if
> unconventional. I think the intention was for neg(a) in PartitionedSignal
> itself to be calculated as ~(a-1), but the final inversion was forgotten,
> leaving only the (a-1) I found.
> 
> > > > and "or", "and", "not" and "implies" should be trivial but important to
> > > > add for completeness.
> > > 
> > > Sure. A partitioned check for those seems a bit overkill, tough. I guess
> > > it's worth it to be extra careful.
> > 
> > yehyeh, that's the idea.  they're bitlevel, it's "irrelevant" but still
> 
> Done.
> 
> implies() was calculated as "~premise | conclusion". I had to change it to
> "conclusion | ~premise", otherwise, the inversion would return a Signal, and
> the following OR would be Signal's OR, not PartitionedSignal's.

hmm there is a precedence system in python to deal with this, to get it to use
the reverse version.

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)

that's the root cause of the problem you are seeing.


> For some reason, the solver again took a long time with implies(). It
> doesn't make sense, since it's just like OR, which is fast, but with one
> input inverted. 

hmm.

> On a whim, I changed the solver from the default (yices2) to z3. Not only it
> didn't show a slowdown on implies(), but the earlier slow XOR became fast as
> well. On the other hand, NOT, ADD and SUB are slower with z3, while fast
> with yices2.

intriguing

> I'll add an optional "solver" parameter to FHDLTestCase.assertFormal().

nice idea.  do let whitequark know.

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