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.
Fix for div pipeline in https://git.libre-soc.org/?p=soc.git;a=commitdiff;h=837d9fbdd54265a63a07e475b6d85313cadf2927
(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.
(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?
(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.
(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 :)
(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.
(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?
(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).
(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?
(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.
(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 :)