[Libre-soc-bugs] [Bug 419] MUL pipeline formal proof needed

[bugzilla-daemon at libre-soc.org]

https://bugs.libre-soc.org/show_bug.cgi?id=419

--- Comment #11 from Luke Kenneth Casson Leighton <lkcl at lkcl.net> ---
(In reply to Samuel A. Falvo II from comment #10)
> I *think* I've completed this pipeline proof.

excellent, looks reasonable: i threw some comments in, could you put some
comments in (brief ones) as to why m63.bool() & ~m63.all() works, what it's
doing?  and why the abs values are used and why check on sign-comparison?

also i believe you missed dut.o.o.ok, there are some other proofs that
create a signal named "ok", set it to 1 at the top, then in the
"default" of the switch set it to zero.  works a treat.

need to check xer_ov as well (different method, there)

then i think we're good here?

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