Alternative solver for the fuzzing problem

[mkurc-ant]

This script solves bits through least-mean-square solution of an overdetermined linear equation system (see docstring in the file). It is an alternative to the segmatch.

For IDELAY fuzzer (#946) and ISERDES fuzzer (still not pushed WIP) it allows to solve more bits than the segmatch.

[mithro]

@litghost This is going to need your review to see if it makes sense.

[litghost]

Can you provide an example fuzzer that uses this solver?

[mkurc-ant]

@litghost I tested it for example with my IDELAY fuzzer. Using segmatch I always have 0 candidates for IDELAY_TYPE_FIXED and IDELAY_TYPE_VARIABLE, but when i use the lms_solver I get a reasonable solution for those features.

I split the fuzzer and the solver into separate PRs. But you can check the solution by first running make database in 035a-iob-iodelay folder for the PR #946. It will generate txt files with segdata. Then in the same folder run lms_solver.py `find build -name "*.txt"` and it will generate a solution.

I have also checked it in the same way for fuzzers 016 and 018. The results are consistent with the segmaker except for some negative correlation which segmaker does not look for.

[litghost]

@mkurc-ant: This tool is extremely useful! The output isn't right yet, but I think we can fix that.

First I need to clarify something about the .db format. In FASM enabling a feature mutates the "default" bitstream, but not enabling a feature does nothing to the "default" bitstream. So take the following correlation:

IOI3.IDELAY_Y1.IDELAY_VALUE[0]           ---------------------10---------------  222|  63 lo=-0.500 hi=+0.500 e=0.000

What your tool outputs is:

IOI3.IDELAY_Y1.IDELAY_VALUE[0] 35_05 !35_07

Which is valid, but incomplete. Let me explain. If the FASM file say:

IOI3.IDELAY_Y1.IDELAY_VALUE[0] = 1

that asserts that 35_05 is set and 35_07 is cleared. However:

IOI3.IDELAY_Y1.IDELAY_VALUE[0] = 0

does nothing! This does not ensure 35_05 is cleared and 35_07 is set! In order to do that, you need to have a new feature, like:

IOI3.IDELAY_Y1.ZIDELAY_VALUE[0] !35_05 35_07 

Make sense?

Second issue I see in the output has to do with enum groupings. Take for example the output from your tool:

IOI3.IDELAY_Y1.IDELAY_TYPE_FIXED !34_08                                           
IOI3.IDELAY_Y1.IDELAY_TYPE_VARIABLE 34_08                                         
IOI3.IDELAY_Y1.IDELAY_TYPE_VAR_LOAD 34_08 34_14

This is valid, but not exactly what was want. I would consider the "correct" output to be:

IOI3.IDELAY_Y1.IDELAY_TYPE_FIXED !34_08 !34_14                   
IOI3.IDELAY_Y1.IDELAY_TYPE_VARIABLE 34_08 !34_14                                   
IOI3.IDELAY_Y1.IDELAY_TYPE_VAR_LOAD 34_08 34_14

The way to express this using segmaker would be to use a zero-db group, like so:

34_08 34_14, IOI3.IDELAY_Y1.IDELAY_TYPE_FIXED 

However manually discovering these groups are time consuming, and you approach nearly does the right thing! See #347 . To be clear, I am not suggesting that we continue to use segmaker and the rdb files. Instead I'm suggestion that we add this kind of group detection to this tool.

Overall, this approach seems very solid, just need to address the above points. This tool is already super useful for guiding modifications to fuzzers. For example, here is the changes required to 035a to solve the relevant bits using segmaker, guided by this tool: #957

[litghost]

Looks really good. I think we may want to consider a hybrid approach, where we use this tool to guide writing of generate.py (and compute the bits.dbf), rather than using it wholesale. I've seen this tool generate spurious correlations, but as guidance it seems top notch!

[litghost]

whic -> which

[litghost]

A problem I've found with this is you need to handle counter-factual proofs. For example if there is ever:

seg X_004
tag Y 1
bit Z
seg X_008
tag Y 0
bit Z

Then bit Z should not be ever associated with tag Y. Segmatch does this, but this tool does not.

[mkurc-ant]

@litghost Thanks for your insights.

I've been thinking how to add automatic tag grouping but I don't have a clear idea how to do it. I think that for sure a list of tags belonging to a group must be specified manually.

As for the counter-factual proof: The problem is that there is no way to be 100% sure that when you tell Vivado to enable a feature it ends up being enabled in the bitstream. Or that is its enabled in the way that we want it to be. For example: For the IDELAY block you can set the IDELAY_VALUE and it is encoded directly in the bitstream. But when you set the IDELAY_TYPE to VAR_LOAD or VAR_LOAD_PIPE then despite that you are setting the delay to eg. 5, Vivado encodes it in the bitstream always as 0. In the generate.py you then set the IDELAY_VALUE to 5 which yields in a counter-factual proof. And the fact is that if such case happens rarely then it only lowers the overall correlation bit-feature. That is why I deliberately do not filter such cases.

[litghost]

As for the counter-factual proof: The problem is that there is no way to be 100% sure that when you tell Vivado to enable a feature it ends up being enabled in the bitstream. Or that is its enabled in the way that we want it to be. For example: For the IDELAY block you can set the IDELAY_VALUE and it is encoded directly in the bitstream. But when you set the IDELAY_TYPE to VAR_LOAD or VAR_LOAD_PIPE then despite that you are setting the delay to eg. 5, Vivado encodes it in the bitstream always as 0. In the generate.py you then set the IDELAY_VALUE to 5 which yields in a counter-factual proof. And the fact is that if such case happens rarely then it only lowers the overall correlation bit-feature. That is why I deliberately do not filter such cases.

The counter-factuals are very important, because they prevent incorrect bit associations. In general, if a counter-factual is causing a failure in segmatch, it is a generate.py bug.

What would be extremely valuable is a way to say "this bit is fairly correlated, except for this case". Many times bits are fairly coupled, but either due to low stimulus or edge cases, a bit toggles infrequently. Finding these edge cases by hand is fairly annoying, but this tool could make a correlate and counter factual report, e.g.:

• These features and bits seem really correlated, except in N cases this feature combination disproves it

Or something like that.

[mithro]

@litghost - Did you mean to merge this pull request? It looks like the tests were failing?