[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 #12 from Samuel A. Falvo II <kc5tja at arrl.net> ---
(In reply to Luke Kenneth Casson Leighton from comment #11)
> 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?

Done.

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

Thanks for this; FOR NOW, I'd like to delay adding this until I fix the most
recent breakage.  I just committed my recent changes, which by all accounts
should work.  However, line 113 (asserting xer_ov_o == dut.i.ctx.xer_ov)
consistently fails **as long as** I assign the convenience variable xer_ov_o =
dut.o.xer_ov.data.  If I replace xer_ov_o with the referent dut.o.xer_ov.data,
it consistently works.

I cannot explain this behavior.  Why should this ever be the case?

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

Not sure what you mean here?  Can you clarify?

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