Counterexample-Guided SMT-Driven Optimal Buffer Sizing

Bryan Brady, Daniel Holcomb, and Sanjit A. Seshia. Counterexample-Guided SMT-Driven Optimal Buffer Sizing. In Proceedings of the Conference on Design, Automation and Test in Europe (DATE), pp. 329–334, March 2011.

Download

[pdf] 

Abstract

The quality of network-on-chip (NoC) designs depends crucially on the size of buffers in NoC components. While buffers impose a significant area and power overhead, they are essential for ensuring high throughput and low latency. In this paper, we present a new approach for minimizing the cumulative buffer size in on-chip networks, so as to meet throughput and latency requirements, given high-level specifications on traffic behavior. Our approach uses model checking based on satisfiability modulo theories (SMT) solvers, within an overall counterexample-guided synthesis loop. We demonstrate the effectiveness of our technique on NoC designs involving arbitration, credit logic, and virtual channels.

BibTeX

@inproceedings{brady-date11,
  author    = {Bryan Brady and Daniel Holcomb and Sanjit A. Seshia},
  title     = {Counterexample-Guided SMT-Driven Optimal Buffer Sizing},
 booktitle = {Proceedings of the Conference on Design, Automation and Test in Europe (DATE)},
 pages = "329--334", 
 month = "March", 
 year = "2011",
  abstract = {The quality of network-on-chip (NoC) designs depends 
crucially on the size of buffers in NoC components. While buffers 
impose a significant area and power overhead, they are essential for 
ensuring high throughput and low latency. In this paper, we present 
a new approach for minimizing the cumulative buffer size in on-chip 
networks, so as to meet throughput and latency requirements, 
given high-level specifications on traffic behavior. Our approach 
uses model checking based on satisfiability modulo theories (SMT) 
solvers, within an overall counterexample-guided synthesis loop. 
We demonstrate the effectiveness of our technique on NoC designs 
involving arbitration, credit logic, and virtual channels.},
}

Generated by bib2html.pl (written by Patrick Riley ) on Mon Jul 11, 2011 22:14:40