[Libre-soc-bugs] [Bug 565] Improve formal verification on PartitionedSignal

bugzilla-daemon at libre-soc.org bugzilla-daemon at libre-soc.org
Sat Jan 9 16:19:28 GMT 2021


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


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

More information about the libre-soc-bugs mailing list