Test vector patterns in LEC

[Fati_hv]

Hello!

As I mentioned in another thread, I'm learning about LEC and i read that you can diagnose causing issues of non equivalence by identifying patterns of test vectors.
I saw that there are mapping issues and the pattern they give in the document is this one:

d: Golden value is 0 and Revised value is 1
D: Golden value is 1 and Revised value is 0

The following illustrates the test vector ordering for a non-equivalence caused by a
mapping issue. Specifically, the supports a, b in Golden are incorrectly mapped to the
supports b', a'.
0: 1001100001 dddDd
1: 0101100001 DDDdD
2: 1001010001 ddddD
3: 0101010001 DDDDd
....
^^ (a is the first column, and b is the second column)
Test vectors contain only patterns of a, b non- equivalence. The output values are also
inverted when a, b change from 01 to 10.

I really am not able to understand what they are saying and explaining.
First of all, they give a test vector with 10 bits yet the output is only 5 characters. Shouldn't it be 10 as well? And let's assume they didn't give the rest of the output, the two first columns of the output don't make sense to me. I'm very confused.
I hope someone knows more about this and can help.
There is also another pattern that they give and I can't understand:

■ Sequential constant

The following illustrates the test vector ordering for a non-equivalence caused by a
sequential constant issue. Specifically, the Golden key points have non-corresponding
DFF supports, and some pattern of these non-corresponding supports is missing in all
test vectors.
0: 11101110 01 Dddd0
1: 11011110 01 Ddd0d
2: 11101110 11 Dddd0
3: 11011110 11 Ddd0d
4: 11101110 10 0ddd0
5: 11011110 10 0dd0d
6: 11001110 01 Ddd00
7: 11001110 11 Ddd00
8: 11001110 10 0dd00
^^ (non corresponding supports that can be sequential
constant 00) (it's referring to the two digits in between the two sequences)
For the above example, pattern 00 is missing, which is the value that these DFFs become
after sequential constant propagation.

As well as this one:

■ Sequential merge

The following illustrates the test vector ordering for a non-equivalence caused by a
sequential merge issue. Specifically, both Golden and Revised key points have noncorresponding DFF supports. The all 0 or all 1 patterns of the non-corresponding DFF
supports are missing from the test vectors.
0: 10000000000000000000000000000000 1 dddddddddddd1ddddddddddddddddddd
1: 01000000000000000000000000000000 1 dddddddddddddddddddddddddddd1ddd
2: 11000000000000000000000000000000 1 dddddddddddd1ddddddddddddddd1ddd
3: 11100000000000000000000000000000 0 0000000000D0D000000000000000D000
4: 11010000000000000000000000000000 0 000000000000D0000000D0000000D000
5: 11001000000000000000000000000000 0 000000000000D000000000000000D0D0
......
In the above example, Golden has 32 DFFs that should be merged, which are shown as
the first 32 supports. These DFFs directly feed to POs, which are proven non-equivalent.
The last support shown is the Revised non-corresponding support. The error happens
when Golden DFFs are taken at different values from the Revised support.

So the last one I understand better. The only thing confusing me is the 1 or 0 in between the two sequences (test vector and output). I don't get its role.

I know I'm asking a lot of questions, but I'm stuck on this and It would help if someone had an answer.

 

[Fati_hv]

Is there anyone who can help?