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