Towards Tractable Hardware Model Validation Against Real Hardware
This work presents a methodology that lets us validate an abstract formal model against real hardware by generating test cases, executing them on real hardware to capture traces of observable behavior, and employing a synthesis approach to identify the internal microarchitectural steps that explain the observable behav...