Skip navigation
Please use this identifier to cite or link to this item:
Title: The Hardware-Software Interface for Systems-on-Chip: Formal Modeling and Modular Verification
Authors: Zhang, Hongce
Advisors: Malik, Sharad
Contributors: Electrical Engineering Department
Keywords: domain-specific hardware accelerator
formal verification
hardware-software interface
instruction-level abstraction
Subjects: Electrical engineering
Computer engineering
Issue Date: 2021
Publisher: Princeton, NJ : Princeton University
Abstract: Modern computing platforms are getting increasingly heterogeneous with domain-specific hardware accelerators. The heterogeneity provides efficiency in computation, however, it also brings about new challenges in specification and verification. Previously, for general-purpose processors, the instruction set architecture (ISA) created a separation between the hardware and software in terms of design and verification. It decoupled the development of a software program from the hardware implementation of the processor. Verification of hardware and software could be conducted separately with ISA as a specification for the hardware, or an abstraction of the hardware for the software. However, for specialized hardware accelerators in emerging systems-on-chip (SoCs), there is no such ISA-like model for the interface. Existing abstract models built in languages like SystemC do not specifically target the hardware-software interface, and therefore, are hard to use to separate the design and verification concerns between hardware and software. This thesis considers the instruction-level abstraction (ILA) as a generalization of the ISA to include domain-specific accelerators in heterogeneous SoCs. It first provides a formal definition of ILA, which, like the ISA, models architectural state variables and their updates in terms of instructions. It then discusses an ILA-based hardware formal verification methodology where ILA is used as a specification, and it demonstrates how formal verification can benefit from the attributes of the ILA through verification case studies. The thesis then discusses the importance of invariants in such formal hardware verification and proposes two techniques, both based on syntax-guided synthesis, forenvironment-invariant synthesis and hardware model checking, respectively. As a hardware-software interface model, ILA is also used as a hardware abstraction in system-level hardware-software verification. Specifically, as SoC components typically use shared memory accesses for bulk data transfer, the verification must take memory consistency issues into account. This is addressed by the ILA-MCM verification framework in this thesis. In summary, this thesis presents the ILA as the hardware-software interface model for the specification and verification of modern heterogeneous SoCs. The ILA-based verification methodology allows modular verification which increases the scalability of formal SoC verification.
Alternate format: The Mudd Manuscript Library retains one bound copy of each dissertation. Search for these copies in the library's main catalog:
Type of Material: Academic dissertations (Ph.D.)
Language: en
Appears in Collections:Electrical Engineering

Files in This Item:
File Description SizeFormat 
Zhang_princeton_0181D_13767.pdf9.65 MBAdobe PDFView/Download

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