[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 #16 from Luke Kenneth Casson Leighton <lkcl at lkcl.net> ---
(In reply to Samuel A. Falvo II from comment #15)
> (In reply to Luke Kenneth Casson Leighton from comment #13)
> > oink.
> 
> Fixed!
> 
> > xer_ov.ok and o.ok are crucial signals that tell the regfiles to actually
> > write the result.
> 
> Right.  That's what I thought, but wasn't 100% sure.

ok you implemented something slightly differently, checking the OE flag
(this is output_stage.py's job, which is not part of the chain).  we
chained these together:

        pipe1 = MulMainStage1(pspec)
        pipe2 = MulMainStage2(pspec)
        pipe3 = MulMainStage3(pspec)

where in fu/mul/pipeline.py you can see that OE checking is handled here:

        out = DivMulOutputStage(self.pspec)  # do CR, XER and out-invert etc.

so any Assertions involving OE would be erroneous.

the xer_ov.ok flag (and o.ok flag) are quite simple, they just tell the
Register Files, "results are available if you want them".

there does exist a Formal Correctness Proof for OutputStage, it does need
updating.

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