Skip navigation
Please use this identifier to cite or link to this item:
Title: Enabling SoC Verification through Instruction-Level Hardware Models
Authors: Xing, Yue
Advisors: Malik, Sharad
Contributors: Electrical and Computer Engineering Department
Keywords: Compositional Verification
Electronic Design Automation (EDA)
Formal Verification
Instruction-Level Abstraction
Subjects: Computer engineering
Electrical engineering
Issue Date: 2023
Publisher: Princeton, NJ : Princeton University
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.
Type of Material: Academic dissertations (Ph.D.)
Language: en
Appears in Collections:Electrical Engineering

Files in This Item:
File Description SizeFormat 
Xing_princeton_0181D_14733.pdf1.46 MBAdobe PDFView/Download

Items in Dataspace are protected by copyright, with all rights reserved, unless otherwise indicated.