MARC

 008250224s2024        us  ||||||||||||||c||eng  d
■001000017160613
■00520250211151049
■006m          o    d                
■007cr#unu||||||||
■020    ▼a9798382840215
■035    ▼a(MiAaPQ)AAI31141135
■040    ▼aMiAaPQ▼cMiAaPQ
■0820  ▼a621.3
■1001  ▼aPan,  Peitian.▼0(orcid)0000-0001-6147-9092
■24510▼aAddressing  the  Verification  Challenge  of  Agile  Hardware  Methodologies.
■260    ▼a[S.l.]▼bCornell  University.  ▼c2024
■260  1▼aAnn  Arbor▼bProQuest  Dissertations  &  Theses▼c2024
■300    ▼a145  p.
■500    ▼aSource:  Dissertations  Abstracts  International,  Volume:  85-12,  Section:  B.
■500    ▼aAdvisor:  Batten,  Christopher.
■5021  ▼aThesis  (Ph.D.)--Cornell  University,  2024.
■520    ▼aThe  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.
■590    ▼aSchool  code:  0058.
■650  4▼aComputer  engineering.
■650  4▼aComputer  science.
■650  4▼aInformation  technology.
■653    ▼aAgile  hardware  methodologies
■653    ▼aFormal  verification
■653    ▼aHardware  description  languages
■653    ▼aSMT  solving
■653    ▼aLatency-insensitive  interfaces  
■690    ▼a0464
■690    ▼a0489
■690    ▼a0984
■71020▼aCornell  University▼bElectrical  and  Computer  Engineering.
■7730  ▼tDissertations  Abstracts  International▼g85-12B.
■790    ▼a0058
■791    ▼aPh.D.
■792    ▼a2024
■793    ▼aEnglish
■85640▼uhttp://www.riss.kr/pdu/ddodLink.do?id=T17160613▼nKERIS▼z이  자료의  원문은  한국교육학술정보원에서  제공합니다.

미리보기

내보내기

chatGPT토론

Ai 추천 관련 도서