With the computer hardware becoming more heterogeneous, it becomes challenging to verify the correctness of the software-hardware stack. Hardware abstractions are necessary to enable scalable verification of the software-hardware stack. But manually constructing hardware abstractions costs much engineering effort and is error-prone. In this thesis, a novel methodology is proposed to automatically generating architecture-level abstractions of hardware. Also, the automatically-generated abstraction is consistent with the underlining hardware by default. Experiments show that high-quality hardware abstraction can be generated for both CPUs and domain-specific accelerators.

Adviser: Sharad Malik