Automatic Generation of Hardware Abstractions from Register-Transfer Level (RTL) Designs

Abstract

Hardware and software systems are getting more complex, which makes it harder to check if they are correct. The different parts of these systems interact in complex ways, so it takes significant time and effort to make sure they work correctly. This thesis explores a solution to make system verification easier by creating hardware abstractions automatically. It focuses on two types of abstractions: architecture-level models and timing models. Deriving these abstractions from the detailed hardware designs greatly reduces the burden of developing these abstractions and also avoids errors from manual construction of such abstractions. Architecture-level models are derived by simplifying the hardware design. These models represent the hardware behavior at the architecture level and abstract away all the implementation details. There are two main steps: determining Architecture-State Variables (ASVs), and extracting the state update functions for the ASVs for each instruction. The proposed algorithms are based on taint analysis, model checking, and compiler optimizations. Timing models are created to include cycle-accurate timing information, which allows for analysis of hardware performance. The timing models make it more efficient to optimize related hardware and software.