可扩展的硬件验证与符号仿真

This  book  presents  recent  advancements  in  symbolic  simulation-based  solutionswhich  radically  improve  scalability.  We  overview  current  verificationtechniques,  both  based  on  logic  simulation  and  on  formal  verification  methods,and  we  describe  in  detail  the  baseline  technique  of  symbolic  simulation.The  core  of  this  book  focuses  on  new  techniques  that  narrow  the  performancegap  between  the  complexity  of  digital  systems  and  the  limited  ability  to  verifythem.  In  particular  we  cover  a  range  of  solutions  that  exploit  approximationand  parametrization  methods  in  order  to  achieve  this  goal.  In  the  directionof  approximation  techniques,  we  comprehensively  cover  quasi-symbolic  simulation-  an  aggressive  technique  aiming  at  simulating  only  the  portion  of  thedesign  necessary  for  the  verification  goal  at  hand  -  and  cycle-based  symbolicsimulation  -  a  unique  combination  of  formal  methods  and  logic  simulation  thatcan  stimulate  a  circuit  with  a  very  large  number  of  input  combinations  and  sequences  in  parallel.  Cycle-based  symbolic  simulation  is  a  hybrid  solution  thatuses  both  approximation  and  parametrization  to  attain  its  scalability  goal.  Itskey  concept  is  the  use  of  a  parametric  form  to  represent  the  set  of  states  visitedduring  simulation.  This  approach  maintains  a  high  degree  of  scalability,  in  linewith  current  logic  simulation  techniques,  while  achieving  better  efficiency.In  the  realm  of  parametric  solutions,  we  discuss  a  range  of  approaches,  includingvarious  applications  of  parametric  symbolic  simulation  to  industrialmicroprocessor  designs.  An  in-depth  analysis  is  dedicated  to  another  solutionthat  we  recently  proposed,  disjoint-support  decomposition-based  symbolicsimulation,  where  the  parametrization  makes  use  of  the  disjoint-support  decomposition  properties  of  a  Boolean  function.  This  simulation  technique  isrooted  on  a  novel  algorithm  that  exposes  the  disjoint  decomposition  propertiesof  a  Boolean  function  by  restructuring  its  BDD  representation.  The  newalgorithm  is  very  efficient  in  the  sense  that  it  has  worst-case  complexity  thatis  only  quadratic  in  the  size  of  the  initial  BDD,  compared  to  that  of  previoussolutions  which  had  exponential  complexity  in  the  number  of  input  variablesof  the  function.  We  deploy  this  algorithm  to  decompose  of  the  state  functionsin  symbolic  simulation.  Then,  by  restructuring  the  next-state  functions  usingtheir  disjoint  components,  it  is  possible  to  transform  them  into  a  simpler  parametric  form  without  sacrificing  simulation  accuracy.  Results  show  that  thistechnique  is  effective  in  reducing  the  memory  requirements  of  symbolic  simulationwhile  maintaining  exact  state  exploration.  When  the  design  complexitybecomes  overwhelming,  it  can  trade-off  search  breadth  for  performance,  andproceed  to  simulate  very  large  trace  sets  in  parallel,  thus  maintaining  a  simulation  speed  and  memory  profile  that  are  close  to  logic  simulation.In  structuring  this  book,  the  hope  was  to  provide  an  interesting  reading  for  abroad  range  of  readers.  Chapters  1,2  and  3  constitute  a  panoramic  flight  overthe  world  of  digital  systems'  design  and,  in  particular,  verification.  Chapter3  reviews  some  of  the  mainstream  symbolic  techniques  in  formal  verification,dedicating  most  of  the  focus  to  symbolic  simulation.We  use  Chapter  4  to  cover  the  necessary  principles  of  parametric  formsand  disjoint-support  decompositions.  In  particular,  we  attempt  to  keep  thematerial  at  a  level  that  facilitates  understanding,  but  without  too  many  formaldetails.  While  there  is  a  range  of  resources  discussing  parametric  formsand  parametrizations  for  Boolean  functions,  we  felt  that  the  topic  of  disjointsupport  decompositions  was  not  as  readily  available.  For  that  reason  Appendix  A  complements  Chapter  4  in  providing  a  more  formal  presentation  of  the  topic  and  derivation  of  the  theoretical  results.Chapters  5  and  6  focus  on  a  range  of  recent  symbolic  simulation  techniques,which  we  grouped  in  approximate  solutions,  and  exact  parametrizations.  Finally,Chapter  7  wraps  up  the  presentation  and  outlines  possible  future  researchdirections.