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

oink.

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

no idea.

sounds like a bug that needs raising (on nmigen).  

> > need to check xer_ov as well (different method, there)
> 
> Not sure what you mean here?  Can you clarify?

xer_ov.ok and o.ok are crucial signals that tell the regfiles to actually write
the result.

if they are not checked then there is the possibility that whilst data is
produced it never actually hits the regfile.

therefore Assert(dut.o.o.ok == something) and Assert(dut.o.xer_ov.ok ==
something) are needed.

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