I have noticed that the Denver cores always seem to be allocated as CPU 1 and 2 while the A57 cores are 0, 3, 4, and 5. Looking at /proc/cpuinfo only shows the A57 cores and dmesg shows that CPU1 and CPU2 are shutdown during boot around the 16.8 second mark.
It appears that the TX2 default boots with the 4 A57 cores running at the full 2GHz and Denver2 cores disabled, if I had to guess why I would say its because Linux can’t take advantage of these cores.
I guess the first thing is to actually enable the cores.