[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 #16 from Cesar Strauss <cestrauss at gmail.com> ---
(In reply to Luke Kenneth Casson Leighton from comment #15)
> (In reply to Cesar Strauss from comment #14)
> 
> > > * Implement proofs of the remaining partitioned operations
> > 
> > This is next. I'll begin with PartitionedEq.

Done. It passes! See:

https://git.libre-soc.org/?p=ieee754fpu.git;a=blob;f=src/ieee754/part_cmp/experiments/formal/proof_partitioned_eq.py;h=ba222a86356b744906fe05516ffb7e257e938cdd;hb=HEAD

> remember that where PartitionedEq currently returns 0b00001 (LSB and zeros)
> in each partition, this needs to be modified to return 0b11111 to indicate
> "equal".
> that is done (easily) with nmutil.ripple.RippleLSB

Understood. I added post processing by RippleLSB in the latest commit.

> also, that PartitionedEq itself isn't actually in use: it was one of the
> early intermediate stages of development, the actual code in use is 
> PartitionedEqGtGe.  that also needs to be run through RippleLSB as its last
> stage, to modify the output.

Sure. I guess it was a stepping stone. Will do PartitionedEqGtGe next.

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