國立虎尾科技大學 |

Enabling SoC Verification Through Instruction-Level Hardware Models.

Record Type:	Language materials, manuscript : Monograph/item
Title/Author:	Enabling SoC Verification Through Instruction-Level Hardware Models./
Author:	Xing, Yue.
Description:	1 online resource (150 pages)
Notes:	Source: Dissertations Abstracts International, Volume: 85-04, Section: A.
Contained By:	Dissertations Abstracts International85-04A.
Subject:	Computer engineering. -
Online resource:	click for full text (PQDT)
ISBN:	9798380413992

Enabling SoC Verification Through Instruction-Level Hardware Models.
Xing, Yue.

Enabling SoC Verification Through Instruction-Level Hardware Models. - 1 online resource (150 pages)

Source: Dissertations Abstracts International, Volume: 85-04, Section: A.

Thesis (Ph.D.)--Princeton University, 2023.

Includes bibliographical references

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.

Electronic reproduction.
Ann Arbor, Mich. :
ProQuest,
2024

Mode of access: World Wide Web

ISBN: 9798380413992Subjects--Topical Terms:

569006
Computer engineering.
Subjects--Index Terms:

Compositional verificationIndex Terms--Genre/Form:

554714
Electronic books.

Enabling SoC Verification Through Instruction-Level Hardware Models.
LDR:03987ntm a2200397K 4500 001 1141612
005 20240318062654.5
006 m o d
007 cr mn ---uuuuu
008 250605s2023 xx obm 000 0 eng d
020 $a 9798380413992
035 $a (MiAaPQ)AAI30632069
035 $a AAI30632069
040 $a MiAaPQ $b eng $c MiAaPQ $d NTU
100 1 $a Xing, Yue. $3 1465508
245 1 0 $a Enabling SoC Verification Through Instruction-Level Hardware Models.
264 0 $c 2023
300 $a 1 online resource (150 pages)
336 $a text $b txt $2 rdacontent
337 $a computer $b c $2 rdamedia
338 $a online resource $b cr $2 rdacarrier
500 $a Source: Dissertations Abstracts International, Volume: 85-04, Section: A.
500 $a Advisor: Malik, Sharad.
502 $a Thesis (Ph.D.)--Princeton University, 2023.
504 $a Includes bibliographical references
520 $a 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.
533 $a Electronic reproduction. $b Ann Arbor, Mich. : $c ProQuest, $d 2024
538 $a Mode of access: World Wide Web
650 4 $a Computer engineering. $3 569006
650 4 $a Electrical engineering. $3 596380
650 4 $a Design. $3 595500
653 $a Compositional verification
653 $a Formal verification
653 $a Instruction-Level Abstraction
653 $a Systems-on-a-Chip
653 $a Graphics Processing Units
655 7 $a Electronic books. $2 local $3 554714
690 $a 0464
690 $a 0544
690 $a 0389
710 2 $a ProQuest Information and Learning Co. $3 1178819
710 2 $a Princeton University. $b Electrical and Computer Engineering. $3 1413580
773 0 $t Dissertations Abstracts International $g 85-04A.
856 4 0 $u http://pqdd.sinica.edu.tw/twdaoapp/servlet/advanced?query=30632069 $z click for full text (PQDT)