Enabling SoC Verification through Instruction-Level Hardware Models

Abstract

Modern Systems-on-a-Chip (SoC) contain a diverse set of hardware design components for efficient computing -- not only Central Processing Units (CPUs) or Graphics Processing Units (GPUs), but also domain-specific accelerators and general hardware modules. These hardware components interact with software programs to deliver application-level functionality. The heterogeneity of hardware and software components leads to a range of verification challenges that relate to specification, scalability and automation. Verification is performed by checking the implementation against a specification. Model checking is widely used for this purpose. In this setting, the specification is a set of formal properties that can be verified by model checking algorithms. However, these properties are typically provided by design/verification engineers. Further, it is hard to evaluate their completeness. Alternatively, a high-level functional model such as the instruction set architecture (ISA) has been used to specify processors, and more recently, this has been extended to the Instruction-Level Abstraction (ILA) for accelerators. However, a similar specification is lacking for other hardware components. A common alternative to formal verification is simulation-based testing, in which a test stimulus is applied to an implementation and the result is compared with the expected value given the specification. For an ISA/ILA specification, this is provided by the executable model of the ISA/ILA. In this setting, manual effort is needed to establish the connection between the execution model of the specification and implementation. This dissertation addresses the challenges arising in the above tasks by leveraging the ILA modeling methodology. It makes the following contributions:- It generalizes the ILA modeling methodology to specify general design modules in an SoC and leverages the ILA verification techniques for their verification. - To address the scalability challenge in the verification of a design composed of several components, it provides a compositional verification methodology that decomposes the verification of a large composed design into a set of smaller verification problems using individual component specifications and an interface specification. - It introduces an instruction-level GPU model to address the scalability challenges of GPU program verification. - Further, it automates the simulation-based testing by leveraging ILA models and a refinement map used in ILA-based formal verification.