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

The test case at src/ieee754/part/test/test_partsig.py was also testing for
(a-1). I fixed it by shifting down the input, negating it and shifting it back
again. This way, it becomes independent of my implementation.

Speaking of which, that test suite fails when checking the partitioned
carry-out from the adder. As it turns out, the carry-out is being registered,
which confuses the test. See:

https://git.libre-soc.org/?p=ieee754fpu.git;a=blob;f=src/ieee754/part_mul_add/adder.py;h=e1849b4d25fc5ec4fc4473cc02b32f49dd5912b2;hb=HEAD#l271

Should we replace sync by comb? Or was it intentional?

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

> shift: likewise, but these are expected to take a looong time, it may be
> better to add them as separate independent unit tests.

OK.

> oh.  one important code-path: RHS (operand 2) as:
> 
> * Const
> * Signal
> * PartitionedSignal
> 
> Shift in particular is commmpletely different when passed in a global Const
> or a global (nonpartitioned) Signal.

Sure.

Const and Signal apply globally, right? For instance, "pa + 1" should add one
independently to each partition, correct?

Const must be given an initial value when created, so we can't depend on the
solver to generate random values for us. We have to repeat running the proof
for random values of the Const.

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