자료유형  

 학위논문

Control Number  

0017160613

International Standard Book Number  

9798382840215

Dewey Decimal Classification Number  

621.3

Main Entry-Personal Name  

Pan, Peitian.

Publication, Distribution, etc. (Imprint  

[S.l.] : Cornell University., 2024

Publication, Distribution, etc. (Imprint  

Ann Arbor : ProQuest Dissertations & Theses, 2024

Physical Description  

145 p.

General Note  

Source: Dissertations Abstracts International, Volume: 85-12, Section: B.

General Note  

Advisor: Batten, Christopher.

Dissertation Note  

Thesis (Ph.D.)--Cornell University, 2024.

Summary, Etc.  

요약The slowdown of Moore's Law and the breakdown of Dennard scaling have driven computer architects towards more specialized hardware designs to meet the growing performance and energy efficiency demands. Such specialized hardware designs tend to have high non-recurring engineering (NRE) costs that hinder the research and development of promising hardware systems. The recent rise of agile hardware design methodologies addresses the high NRE costs by promoting the reuse of hardware designs and applying state-of-the-art software design and testing practices to hardware design. Unfortunately, agile hardware methodologies also face unique verification challenges in the hardware development process.In this thesis, I identify and address key verification challenges in agile hardware methodologies. First, I address the verification challenges in dynamic HDLs. Modern HDLs embedded in dynamically typed programming languages facilitate the composition of statically typed hardware instances and dynamically typed test harnesses. However, existing dynamic HDLs suffer from the lack of early-in-design-cycle and complete safety guarantees for mixed-typed compositions and low simulation performance. I propose GT-HDL, an embedded HDL that leverage a combination of optional type checkers, guarded generator parameters, and type-based simulation optimizations to improve simulation performance of dynamic HDLs without compromising safety. Second, I address the verification challenges in generator creation. Recent HDLs heavily rely on parametrized and sophisticated hardware generators to achieve and maximize design reuse. However, it is challenging to verify the correctness of the hardware generators across the entire parameter space. To systematically and statically verify generator properties over a large parameter space, I propose symbolic elaboration, a static analysis technique based on satisfiability modulo theory (SMT) solving. Symbolic elaboration targets a synthesizable subset of HDL syntax and translates generator properties into integer constraints that can be solved by SMT solvers. Third, I overcome the verification challenges in instance composition. Latency-insensitive (LI) interfaces are critical to instance composition in agile hardware because they enable modular and composable hardware designs. However, it is challenging to verify the correctness of the LI interface handshake logic using dynamic verification techniques. I propose a formal verification solution to automatically verify hardware designs with LI interfaces that also generates counter example waveforms to debug LI handshake issues. Finally, I address the verification challenges in co-simulation. Modern HDLs used in agile hardware are typically embedded in a general-purpose host programming language. To maximize verification productivity, designers ideally should iterate on the target design using native simulations before generating RTL in a prototyping language such as Verilog. However, it is challenging to co-simulate the generated Verilog RTL and the test bench in the host language due to semantic gap between the host and the prototyping languages. To overcome this limitation, I propose seamless co-simulation based on a translation-import mechanism. I implement the translation-import mechanism in the PyMTL3 framework and demonstrate how it can improve verification productivity by reusing one test bench for both native simulation and co-simulation. In addition to the proposed solutions to verification challenges, I also present a coarse-grain reconfigurable array (CGRA) chip tape-out case study in GlobalFoundries 14nm technology. This case study demonstrates how the proposed solutions in this thesis can be integrated into an ASIC prototyping workflow and contribute to productive design and testing of the target hardware.

Subject Added Entry-Topical Term  

Computer engineering.

Subject Added Entry-Topical Term  

Computer science.

Subject Added Entry-Topical Term  

Information technology.

Index Term-Uncontrolled  

Agile hardware methodologies

Index Term-Uncontrolled  

Formal verification

Index Term-Uncontrolled  

Hardware description languages

Index Term-Uncontrolled  

SMT solving

Index Term-Uncontrolled  

Latency-insensitive interfaces

Added Entry-Corporate Name  

Cornell University Electrical and Computer Engineering

Host Item Entry  

Dissertations Abstracts International. 85-12B.

Electronic Location and Access  

로그인을 한후 보실 수 있는 자료입니다.

Control Number  

joongbu:656931