Validating Families of Latency Insensitive Protocols
|
With increasing clock frequencies, the signal delay on some interconnects in a System on Chip (SoC) often exceeds the clock period, which necessitates latency insensitive protocols (LIPs). The correctness of a system composed of synchronous blocks communicating via LIPs is established by showing latency equivalence between a completely synchronous composition of the blocks, and the LIP-based composition. Every time a new LIP is conceived, it needs to be debugged and then proven correct. Mathematical theorems to establish correctness, though elegant, are error prone, and tedious to create for every new variant of LIPs. In this work, we present validation frameworks for families of LIPs, both for dynamic validation, useful for early debug cycles, and formal verification for formal proof of correctness. This can be a useful framework in the hands of designers trying to create new LIPs or to optimize existing ones for design convergence.
[1] 1391 M.T. Bohr, “Interconnect Scaling—The Real Limiter to High Performance Ulsi,” IEEE Int'l Electron Devices Meeting, pp. 241-244, 1995.
[2] L.P. Carloni and A.L. Sangiovanni-Vincentelli, “Coping with Latency in SoC Design,” IEEE Micro, special issue on Systems on Chip, vol. 22, no. 5, p. 12, Sept.-Oct. 2002.
[3] L. Carloni, K. McMillan, A. Saldanha, and A. Sangiovanni-Vincentelli, “A Methodology for Correct-by-Construction Latency Insensitive Design,” Proc. Int'l Conf. Computer Aided Verification, pp. 309-315, Nov. 1999.
[4] L.P. Carloni, K.L. McMillan, and A.L. Sangiovanni-Vincentelli, “Latency Insensitive Protocols,” Proc. 11th Int'l Conf. Computer-Aided Verification, pp. 123-133, 1999.
[5] L. Carloni, K. McMillan, and A. Sangiovanni-Vincentelli, “The Theory of Latency Insensitive Design,” IEEE Trans. Computer Aided Design of Integrated Circuits and System, vol. 20, no. 9, pp. 1059-1076, 2001.
[6] M. Casu and L. Macchiarulo, “A New Approach to Latency Insensitive Design,” Proc. Design Automation Conf., 2004.
[7] M. Singh and M. Theobald, “Generalized Latency-Insensitive Systems for Single-Clock and Multi-Clock Architectures,” Proc. Design, Automation and Test in Europe (DATE '04), 2004.
[8] S. Suhaib, D. Berner, D. Mathaikutty, J.-P. Talpin, and S. Shukla, Presentation and Formal Verification of a Family of Protocols for Latency Insensitive Design, Technical Report 2005-02, Virginia Tech, 2005.
[9] L. Benini and G. De Micheli, “Networks on Chip: A New Paradigm for Systems on Chip Design,” Proc. Design, Automation and Test in Europe, 2002.
[10] A. Jantsch, Modeling Embedded Systems and SoCs—Concurrency and Time in Models of Computation. Morgan Kaufmann, 2001.
[11] E. Clarke, O. Grumberg, and D. Peled, Model Checking. The MIT Press, 2000.
[12] G. Holzmann, The SPIN Model Checker. Addison Wesley, 2004.
[13] D.A. Mathaikutty, H.D. Patel, and S.K. Shukla, “A Functional Programming Framework of Heterogeneous Model of Computation for System Design,” Proc. Forum of Design Languages (FDL '04), 2004.
[14] R. Milner, M. Tofte, R. Harper, and D. MacQueen, The Definition of Standard ML—Revised. MIT Press, 1997.
[15] LIP FERMAT Website. http://fermat.ece.vt.eduLIP.html, 2005.
Index Terms:
Simulation, formal verification, long interconnects, latency insensitive protocols, relay station, splitter, merger, verification framework.
Citation:
Syed Suhaib, Deepak Mathaikutty, David Berner, Sandeep Shukla, "Validating Families of Latency Insensitive Protocols," IEEE Transactions on Computers, vol. 55, no. 11, pp. 1391-1401, Nov. 2006, doi:10.1109/TC.2006.188
PURCHASE ARTICLE: $19
IEEE Xplore Subscribers
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb