서브메뉴
검색
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
- 전자적 위치 및 접속
- 로그인 후 원문을 볼 수 있습니다.
MARC
008240612s2023 us |||||||||||||||c||eng d■001000016934645
■00520240214101637
■006m o d
■007cr#unu||||||||
■020 ▼a9798380413992
■035 ▼a(MiAaPQ)AAI30632069
■040 ▼aMiAaPQ▼cMiAaPQ
■0820 ▼a621.3
■1001 ▼aXing, Yue.
■24510▼aEnabling SoC Verification Through Instruction-Level Hardware Models▼h[electronic resource]
■260 ▼a[S.l.]:▼bPrinceton University. ▼c2023
■260 1▼aAnn Arbor :▼bProQuest Dissertations & Theses, ▼c2023
■300 ▼a1 online resource(150 p.)
■500 ▼aSource: Dissertations Abstracts International, Volume: 85-04, Section: A.
■500 ▼aAdvisor: Malik, Sharad.
■5021 ▼aThesis (Ph.D.)--Princeton University, 2023.
■506 ▼aThis item must not be sold to any third party vendors.
■520 ▼aModern 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.
■590 ▼aSchool code: 0181.
■650 4▼aComputer engineering.
■650 4▼aElectrical engineering.
■650 4▼aDesign.
■653 ▼aCompositional verification
■653 ▼aFormal verification
■653 ▼aInstruction-Level Abstraction
■653 ▼aSystems-on-a-Chip
■653 ▼aGraphics Processing Units
■690 ▼a0464
■690 ▼a0544
■690 ▼a0389
■71020▼aPrinceton University▼bElectrical and Computer Engineering.
■7730 ▼tDissertations Abstracts International▼g85-04A.
■773 ▼tDissertation Abstract International
■790 ▼a0181
■791 ▼aPh.D.
■792 ▼a2023
■793 ▼aEnglish
■85640▼uhttp://www.riss.kr/pdu/ddodLink.do?id=T16934645▼nKERIS▼z이 자료의 원문은 한국교육학술정보원에서 제공합니다.
■980 ▼a202402▼f2024
