Title
Counterexample-guided SMT-driven optimal buffer sizing
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.
Year
DOI
Venue
2011
10.1109/DATE.2011.5763058
Design, Automation & Test in Europe Conference & Exhibition
Keywords
DocType
ISSN
buffer storage,computability,network-on-chip,NoC components,counterexample-guided SMT-driven optimal buffer sizing,counterexample-guided synthesis loop,cumulative buffer size,network-on-chip designs,on-chip networks,satisfiability modulo theories
Conference
1530-1591
ISBN
Citations 
PageRank 
978-1-61284-208-0
3
0.38
References 
Authors
12
3
Name
Order
Citations
PageRank
Bryan A. Brady1312.16
Daniel E. Holcomb246231.63
Sanjit A. Seshia32226168.09