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
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.}, }