Enabling SoC Verification Through Instruction-Level Hardware Models- [electronic resource]
Enabling SoC Verification Through Instruction-Level Hardware Models- [electronic resource]
- 자료유형
- 학위논문파일 국외
- 최종처리일시
- 20240214101637
- ISBN
- 9798380413992
- DDC
- 621.3
- 저자명
- Xing, Yue.
- 서명/저자
- Enabling SoC Verification Through Instruction-Level Hardware Models - [electronic resource]
- 발행사항
- [S.l.]: : Princeton University., 2023
- 발행사항
- Ann Arbor : : ProQuest Dissertations & Theses,, 2023
- 형태사항
- 1 online resource(150 p.)
- 주기사항
- Source: Dissertations Abstracts International, Volume: 85-04, Section: A.
- 주기사항
- Advisor: Malik, Sharad.
- 학위논문주기
- Thesis (Ph.D.)--Princeton University, 2023.
- 사용제한주기
- This item must not be sold to any third party vendors.
- 초록/해제
- 요약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 typically need to be 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) as a specification 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 in modern SoC verification 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 each 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.
- 일반주제명
- Computer engineering.
- 일반주제명
- Electrical engineering.
- 일반주제명
- Design.
- 기타저자
- Princeton University Electrical and Computer Engineering
- 기본자료저록
- Dissertations Abstracts International. 85-04A.
- 기본자료저록
- Dissertation Abstract International
- 전자적 위치 및 접속
- 로그인 후 원문을 볼 수 있습니다.
ค้นหาข้อมูลรายละเอียด
- จองห้องพัก
- ไม่อยู่
- โฟลเดอร์ของฉัน
- ขอดูแรก
- 비도서대출신청
- 야간 도서대출신청
로그인 후 이용 가능합니다.