[Libre-soc-bugs] [Bug 419] MUL pipeline formal proof needed

bugzilla-daemon at libre-soc.org bugzilla-daemon at libre-soc.org
Fri Sep 4 00:27:53 BST 2020


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

check for yourself:


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 ?


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.

More information about the libre-soc-bugs mailing list