*banner
 

Formal Verification and Synthesis for Quality-of-Service in On-Chip Networks
Dan Holcomb

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

Citation formats  
  • 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.

Notice: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright.

©2002-2018 Chess