[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 #15 from Luke Kenneth Casson Leighton <lkcl at lkcl.net> ---
(In reply to Cesar Strauss from comment #14)

> > * Implement proofs of the remaining partitioned operations
> 
> This is next. I'll begin with PartitionedEq.

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

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.

ultimately PartitionedEqGtGe will need to be revised rather than
post-processed: given that it took 3 weeks to write this can be done during an
optimisation pass.

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