Citation
Dan Holcomb. "Formal Verification and Synthesis for Quality-of-Service in On-Chip Networks". Talk or presentation, 27, August, 2013.

Abstract
Quality-of-Service (QoS) in on-chip communication networks has a tremendous impact on overall system performance in today's era of ever-increasing core counts. Yet, Networks-on-Chip (NoCs) are still designed and analyzed using RTL simulation or highly abstracted analytical models. Formal methods, used successfully for many other verification tasks, have traditionally not found use in QoS verification due to the scale of the problems of interest, such as verifying latency bounds of hundreds of cycles for large on-chip networks. In this dissertation talk, I will present recent work toward leveraging formal methods for NoC synthesis and QoS verification. In particular, we address the problems of (1) optimal buffer sizing using a counterexample-guided approach, (2) using abstraction to verify end-to-end latency bounds in a mesh network, and (3) scalable latency verification using compositional inductive proofs.

Electronic downloads

• holcomb_dissertation_talk_oct_27_2013.pdf · application/pdf · 11514 kbytes

• HTML

  Dan Holcomb. <a
  href="http://chess.eecs.berkeley.edu/pubs/1013.html"
  ><i>Formal Verification and Synthesis for
  Quality-of-Service in On-Chip Networks</i></a>,
  Talk or presentation,  27, August, 2013.

• Plain text

  Dan Holcomb. "Formal Verification and Synthesis for
  Quality-of-Service in On-Chip Networks". Talk or
  presentation,  27, August, 2013.

• BibTeX

  @presentation{Holcomb13_FormalVerificationSynthesisForQualityofServiceInOnChip,
      author = {Dan Holcomb},
      title = {Formal Verification and Synthesis for
                Quality-of-Service in On-Chip Networks},
      day = {27},
      month = {August},
      year = {2013},
      abstract = {Quality-of-Service (QoS) in on-chip communication
                networks has a tremendous impact on overall system
                performance in today's era of ever-increasing core
                counts. Yet, Networks-on-Chip (NoCs) are still
                designed and analyzed using RTL simulation or
                highly abstracted analytical models. Formal
                methods, used successfully for many other
                verification tasks, have traditionally not found
                use in QoS verification due to the scale of the
                problems of interest, such as verifying latency
                bounds of hundreds of cycles for large on-chip
                networks. In this dissertation talk, I will
                present recent work toward leveraging formal
                methods for NoC synthesis and QoS verification. In
                particular, we address the problems of (1) optimal
                buffer sizing using a counterexample-guided
                approach, (2) using abstraction to verify
                end-to-end latency bounds in a mesh network, and
                (3) scalable latency verification using
                compositional inductive proofs.},
      URL = {http://chess.eecs.berkeley.edu/pubs/1013.html}
  }
  

Posted by Armin Wasicek on 5 Sep 2013.
Groups: chessworkshop
For additional information, see the Publications FAQ or contact webmaster at chess eecs berkeley edu.