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

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. 

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.

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

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