[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 #18 from Samuel A. Falvo II <kc5tja at arrl.net> ---
Thanks for cleaning up the code; it reads a lot better.  I do have some
questions though.

(In reply to Luke Kenneth Casson Leighton from comment #16)
> 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".

Can you help me understand why xer_ov.ok is reset only in the default case?  As
I understand the ISA specs, xer_ov.ok should only be set when OE=1.  I feel
like I'm missing something.

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

I looked in the fu/mul hierarchy for this correctness proof, but did not find
it.  Are you perhaps referring to alu/formal/proof_output_stage.py ?

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