[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 #32 from Luke Kenneth Casson Leighton <lkcl at lkcl.net> ---
(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).

odd.  sounds better.

> The test case at src/ieee754/part/test/test_partsig.py was also testing for
> (a-1).

bizzare

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

err yes :)

> Or was it intentional?

not at all!

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

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

yes. there will be cases where this needs to be done, such as immediate
operations, the immediate will need adding to all SIMD elements.

likewise for example if an algorithm needs a shift by X const then SIMD shift
by X applies to all elements 

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

hmm yuk, we can probably get away with just Signal then

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