Detection of bugs in the complex address translation mechanisms (ATMs) of modern microprocessors is much harder than in other microprocessor structures because their output (the physical address) is not directly observable to program or architecture visible locations during post-silicon validation. Errata reports, by major microprocessor vendors about ATM-related bugs found after chips massive production, plea for more efficient validation solutions. In this paper, we formulate the problem of post-silicon validation of microprocessors' address translation hardware, by defining a comprehensive set of bug models. We then propose an ISA-independent post-silicon validation methodology for the ATMs of high-end microprocessors. The method detects ATM bugs right after their manifestation, reveals mismatches due to them and facilitates diagnosis and debug. Our experiment evaluation on an enhanced version of the Gem5 simulator (including MMU caches) demonstrates the effectiveness of the method in detecting known ATM bugs, five orders of magnitude faster than traditional approaches.