Bug 449 - FU unit tests checking output one cycle too late
Summary: FU unit tests checking output one cycle too late
Status: RESOLVED FIXED
Alias: None
Product: Libre-SOC's first SoC
Classification: Unclassified
Component: Source Code (show other bugs)
Version: unspecified
Hardware: PC Linux
: --- normal
Assignee: Luke Kenneth Casson Leighton
URL:
Depends on:
Blocks: 324
  Show dependency treegraph
 
Reported: 2020-08-05 04:48 BST by Jacob Lifshay
Modified: 2020-08-05 21:18 BST (History)
2 users (show)

See Also:
NLnet milestone: ---
total budget (EUR) for completion of task and all subtasks: 0
budget (EUR) for this task, excluding subtasks' budget: 0
parent task for budget allocation:
child tasks for budget allocation:
The table of payments (in EUR) for this task; TOML format:


Attachments

Note You need to log in before you can comment on or make changes to this bug.
Description Jacob Lifshay 2020-08-05 04:48:13 BST
I finally figured out why the div pipe was failing with the FSM:
the unit test was checking the output one cycle later than it should. Once I fixed that, the tests pass for all three div pipe implementations.

The unit tests for the other FUs are probably broken in the same way, so I'm creating this bug report to track fixing it.
Comment 2 Luke Kenneth Casson Leighton 2020-08-05 12:29:11 BST
(In reply to Jacob Lifshay from comment #0)
> I finally figured out why the div pipe was failing with the FSM:
> the unit test was checking the output one cycle later than it should. 

hmmm yeah i found timing issues with MUL as well, these unit tests
are cobbled together to do manual ready/valid signalling which is
normally handled by the CompUnit "Manager".

> Once I fixed that, the tests pass for all three div pipe implementations.

excellent.

> The unit tests for the other FUs are probably broken in the same way, so I'm
> creating this bug report to track fixing it.

i ran test_div_compunit.py and it worked perfectly: i expected that it would.

with each test_pipe_caller.py being hand-written ready/valid signalling,
it's kiinda "ok" that their ready/valid signalling is "borked" (or in
the case of the single-stage ones such as ALU and Logical, *completely* borked).

as long as the test_*_compunit.py functions correctly it's fine.

this is precisely why we have unit tests at every integration level.

i think we're good on this one.
Comment 3 Cole Poirier 2020-08-05 17:40:08 BST
(In reply to Luke Kenneth Casson Leighton from comment #2)
> i ran test_div_compunit.py and it worked perfectly: i expected that it would.
> 
> with each test_pipe_caller.py being hand-written ready/valid signalling,
> it's kiinda "ok" that their ready/valid signalling is "borked" (or in
> the case of the single-stage ones such as ALU and Logical, *completely*
> borked).

Do you think in the future Managers for ready/valid signalling should be added into the unit test? If so what is blocking this? Do the Managers need to be formally verified first so we don't introduce an unrelated point of failure into the DIV and MUL unit tests?

> as long as the test_*_compunit.py functions correctly it's fine.
> 
> this is precisely why we have unit tests at every integration level.
> 
> i think we're good on this one.

Or is it that these unit tests will be integrated into future higher-level unit tests?
Comment 4 Luke Kenneth Casson Leighton 2020-08-05 17:58:30 BST
(In reply to Cole Poirier from comment #3)

> Do you think in the future Managers for ready/valid signalling should be
> added into the unit test? 

they already are: they're called compunit tests, and they're in
soc/fu/compunit/test.

> If so what is blocking this? 

nothing because they already exist.

> Do the Managers need to be formally verified first

soc/fu/compunits/formal/proof_fu.py

it needs to be completed.

> so we don't introduce an unrelated point of
> failure into the DIV and MUL unit tests?

indeed.  however given that there are 8+ pipelines using MultiCompUnit, and after 4+ months of work by both myself, cesar and michael we are reeeeasonably confident it's stable.

the formal proof proof_fu.py - if written correctly - gives us 100% confidence rather than "empirical evidential" confidence.


> > as long as the test_*_compunit.py functions correctly it's fine.
> > 
> > this is precisely why we have unit tests at every integration level.
> > 
> > i think we're good on this one.
> 
> Or is it that these unit tests will be integrated into future higher-level
> unit tests?

absolutely not.  they are designed specifically to be absolutely 100%
separate and distinct.

i've said this before a number of times:

1) test_pipe_caller.py tests the functionality of the *pipeline*

2) test_*_compunit tests the *MANAGEMENT* of the pipeline

3) test_core.py tests the integration of pipelines with *register* files

4) test_issuer.py tests the allocation of instructions *to* pipelines.
Comment 5 Cole Poirier 2020-08-05 18:16:26 BST
(In reply to Luke Kenneth Casson Leighton from comment #4)
> (In reply to Cole Poirier from comment #3)
> 
> > Do you think in the future Managers for ready/valid signalling should be
> > added into the unit test? 
> 
> they already are: they're called compunit tests, and they're in
> soc/fu/compunit/test.

Sorry I meant the test_pipe_caller tests because you said "with each test_pipe_caller.py being hand-written ready/valid signalling,
it's kiinda "ok" that their ready/valid signalling is "borked" (or in
the case of the single-stage ones such as ALU and Logical, *completely* borked)."

But clearly I missed this: "as long as the test_*_compunit.py functions correctly it's fine."

And your below comments further elucidate this.


> 
> > If so what is blocking this? 
> 
> nothing because they already exist.
> 
> > Do the Managers need to be formally verified first
> 
> soc/fu/compunits/formal/proof_fu.py
> 
> it needs to be completed.
> 
> > so we don't introduce an unrelated point of
> > failure into the DIV and MUL unit tests?
> 
> indeed.  however given that there are 8+ pipelines using MultiCompUnit, and
> after 4+ months of work by both myself, cesar and michael we are
> reeeeasonably confident it's stable.
> 
> the formal proof proof_fu.py - if written correctly - gives us 100%
> confidence rather than "empirical evidential" confidence.

Sorry, I'm not clear. Does "soc/fu/compunits/formal/proof_fu.py need to be completed."? Or are you saying that this has been done by you, michael, and cesar and you are reasonable confident it's stable?

> > > as long as the test_*_compunit.py functions correctly it's fine.
> > > 
> > > this is precisely why we have unit tests at every integration level.
> > > 
> > > i think we're good on this one.
> > 
> > Or is it that these unit tests will be integrated into future higher-level
> > unit tests?
> 
> absolutely not.  they are designed specifically to be absolutely 100%
> separate and distinct.
> 
> i've said this before a number of times:

You have, but this level of careful design it unfortunately unusual, so in order for my brain to grok this it needs repeats exposure.

> 1) test_pipe_caller.py tests the functionality of the *pipeline*
> 
> 2) test_*_compunit tests the *MANAGEMENT* of the pipeline
> 
> 3) test_core.py tests the integration of pipelines with *register* files
> 
> 4) test_issuer.py tests the allocation of instructions *to* pipelines.

So thank you for elucidating this very well-designed api and test architecture once again :)
Comment 6 Luke Kenneth Casson Leighton 2020-08-05 18:19:34 BST
(In reply to Cole Poirier from comment #5)

> Sorry, I'm not clear. Does "soc/fu/compunits/formal/proof_fu.py need to be
> completed."?

yes.
Comment 7 Cole Poirier 2020-08-05 18:23:45 BST
(In reply to Luke Kenneth Casson Leighton from comment #6)
> (In reply to Cole Poirier from comment #5)
> 
> > Sorry, I'm not clear. Does "soc/fu/compunits/formal/proof_fu.py need to be
> > completed."?
> 
> yes.

Ok, so what you were referring to here, "indeed. however given that there are 8+ pipelines using MultiCompUnit, and after 4+ months of work by both myself, cesar and michael we are reeeeasonably confident it's stable.", is the pipeline API?
Comment 8 Luke Kenneth Casson Leighton 2020-08-05 19:56:27 BST
(In reply to Cole Poirier from comment #7)

> Ok, so what you were referring to here, "indeed. however given that there
> are 8+ pipelines using MultiCompUnit, and after 4+ months of work by both
> myself, cesar and michael we are reeeeasonably confident it's stable.", is
> the pipeline API?

no, i was referring to MultiCompUnit, because the context was MultiCompUnit
and that formal proofs of MultiCompUnit had been mentioned.  no mention
of the pipeline API had been made.

(it so happens that MultiCompUnit *interacts* with pipelines *via* the
pipeline API).
Comment 9 Cole Poirier 2020-08-05 20:30:58 BST
(In reply to Luke Kenneth Casson Leighton from comment #8)
> (In reply to Cole Poirier from comment #7)
> 
> > Ok, so what you were referring to here, "indeed. however given that there
> > are 8+ pipelines using MultiCompUnit, and after 4+ months of work by both
> > myself, cesar and michael we are reeeeasonably confident it's stable.", is
> > the pipeline API?
> 
> no, i was referring to MultiCompUnit, because the context was MultiCompUnit
> and that formal proofs of MultiCompUnit had been mentioned.  no mention
> of the pipeline API had been made.
> 
> (it so happens that MultiCompUnit *interacts* with pipelines *via* the
> pipeline API).

That's true, I'm grasping at straws because I was having trouble understanding what you were saying, my fault not yours. Ok, so to be explicit, MultiCompUnit has a formal proof that you are confident in, soc/fu/compunits/formal/proof_fu.py still needs to be completed?
Comment 10 Luke Kenneth Casson Leighton 2020-08-05 21:15:26 BST
(In reply to Cole Poirier from comment #9)
).
> 
> That's true, I'm grasping at straws because I was having trouble
> understanding what you were saying, my fault not yours. Ok, so to be
> explicit, MultiCompUnit has a formal proof that you are confident in,
> soc/fu/compunits/formal/proof_fu.py still needs to be completed?

no: proof_fu.py is the MCU proof that has not been completed, which, like *all* formal correctness proofs, *if* completed, and completed correctly, gives 100 confidence.

there are not two separate proofs for MCU, one of which is completed and one of which has not.  that would be completely pointless.
Comment 11 Cole Poirier 2020-08-05 21:18:31 BST
(In reply to Luke Kenneth Casson Leighton from comment #10)
> (In reply to Cole Poirier from comment #9)
> ).
> > 
> > That's true, I'm grasping at straws because I was having trouble
> > understanding what you were saying, my fault not yours. Ok, so to be
> > explicit, MultiCompUnit has a formal proof that you are confident in,
> > soc/fu/compunits/formal/proof_fu.py still needs to be completed?
> 
> no: proof_fu.py is the MCU proof that has not been completed, which, like
> *all* formal correctness proofs, *if* completed, and completed correctly,
> gives 100 confidence.
> 
> there are not two separate proofs for MCU, one of which is completed and one
> of which has not.  that would be completely pointless.

Ok, thanks for taking to time to walk through this with me, I think I have finally *gotten* it :)