Skip navigation
Please use this identifier to cite or link to this item: http://arks.princeton.edu/ark:/88435/dsp012r36v166m
Full metadata record
DC FieldValueLanguage
dc.contributor.advisorMalik, Sharad
dc.contributor.authorZhang, Hongce
dc.contributor.otherElectrical Engineering Department
dc.date.accessioned2021-10-04T13:47:33Z-
dc.date.available2021-10-04T13:47:33Z-
dc.date.created2021-01-01
dc.date.issued2021
dc.identifier.urihttp://arks.princeton.edu/ark:/88435/dsp012r36v166m-
dc.description.abstractModern 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.
dc.format.mimetypeapplication/pdf
dc.language.isoen
dc.publisherPrinceton, NJ : Princeton University
dc.relation.isformatofThe Mudd Manuscript Library retains one bound copy of each dissertation. Search for these copies in the library's main catalog: <a href=http://catalog.princeton.edu>catalog.princeton.edu</a>
dc.subjectdomain-specific hardware accelerator
dc.subjectformal verification
dc.subjecthardware-software interface
dc.subjectinstruction-level abstraction
dc.subjectsystems-on-chip
dc.subject.classificationElectrical engineering
dc.subject.classificationComputer engineering
dc.titleThe Hardware-Software Interface for Systems-on-Chip: Formal Modeling and Modular Verification
dc.typeAcademic dissertations (Ph.D.)
pu.date.classyear2021
pu.departmentElectrical Engineering
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.