[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 #19 from Luke Kenneth Casson Leighton <lkcl at lkcl.net> ---
(In reply to Samuel A. Falvo II from comment #18)
> Thanks for cleaning up the code; it reads a lot better.  I do have some
> questions though.

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

OutputStage, which is *not included in the chain in this proof*, handles OE
checking.

check for yourself:

https://git.libre-soc.org/?p=soc.git;a=blob;f=src/soc/fu/mul/formal/proof_main_stage.py;h=0cf767f341668663a4f4c736af5aea5625c1c0d2;hb=HEAD#l88

is OutputStage in that chain? no it is not.

therefore trying to Assert things that *are not part of the test* is simply
never going to work, is it?

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

yes.  it's in the alu dir.

> Are you perhaps referring to alu/formal/proof_output_stage.py ?

yes.

if we were to include OutputStage in the chain at line 88, then the contents of
alu proof_output_stage.py would need to be duplicated in their entirety in mul
proof, wouldn't they?

which would be a waste of effort.  therefore we don't do that.

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