Model Checking Formal Verification Methodology for Virtual Channel NoCs


Article Preview

The increasing complexity of System on a Chip (SOC) using Network on a Chip (NoC) results in significant increases in traditional verification times. Formal methods fully prove design properties, without deadline vs. coverage compromises, hence tremendously reducing time to market. In this work we use the CONNECT NOC to illustrate our new white box formal verification methodology. We develop constraints and assertions for properties verification. Our methodology is faster than the current methods; it also uncovered key gaps in current practices. In addition, our assertion checkers can be reused both in simulation and as monitors on silicon.



Edited by:

Mahir Dursun




S. Agamy et al., "Model Checking Formal Verification Methodology for Virtual Channel NoCs", Applied Mechanics and Materials, Vol. 850, pp. 30-37, 2016

Online since:

August 2016




* - Corresponding Author

[1] P. P. Pande, C. Grecu, M. Jones, A. Ivanov, and R. Saleh Performance evaluation and design trade-offs for Network-on-Chip interconnect architectures, in IEEE TRANSACTIONS ON COMPUTERS, VOL. 54, NO. 8, (AUGUST 2005).


[2] R. Marculescu, U. Y. Ogras, L. Peh, N. E. Jerger, and Y. Hoskote, Outstanding Research Problems in NoC Design: System, Microarchitecture, and Circuit Perspectives, in IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, VOL. 28, NO. 1, (JANUARY 2009).


[3] G. Tsiligiannis, L. Pierre: A Mixed Verification Strategy Tailored for Networks on Chip,. Proc. ACM/IEEE International Symposium on Networks-on-Chip, Lyngby Denmark, (May 2012).


[4] D. Borrione, A. Helmy, L. Pierre, and J. Schmaltz, A formal approach to the verification of networks on chip., EURASIP J. Emb. Sys., (2009).

[5] Y. Oddos, K. Morin-Allory, and D. Borrione, Assertion-Based Design with Horus, " in MEMOCODE, 08, (June 2008).


[6] C. Yean-Ru, S. Wan-Ting, H. Pao-Ann, L. Ying-Cherng, H. Yu-Hen, and C. Sao-Jie, Formal modeling and verification for Network-on-chip, " in Proc. Conf. "Green Circuits and Systems, (ICGCS), June (2010).


[7] F. G. Moraes, N. Calazans, A. Mello, L. Mller, and L. Ost, Hermes: an infrastructure for low area overhead packet-switching networks onchip, The VLSI Journal, vol. 8, no. 1, (2004).


[8] GAPH – Hermes – PUCRS, Hermes routing fabric designs and manuals http: /www. inf. pucrs. br/~calazans/research/Projects/Hermes/Hermes. html.

[9] Michael K. Papamichael and James C. Hoe. CONNECT: Re-Examining Conventional Wisdom for Designing NoCs in the Context of FPGAs, To appear in 20th ACM/SIGDA International Symposium on Field- Programmable Gate Arrays (FPGA 2012), Monterey, CA, (February 22-24, 2012).


[10] CONNECT- CONfigurable Network Creation Tool, Network design and manuals for CONNECT routing fabric and networks. http: /users. ece. cmu. edu/~mpapamic/connect/?id=gen.

[11] W. J. Dally and B. Towles. Principles and Practices of Interconnection Networks. Morgan Kaufmann Publishers, San Francisco, CA, (2004).

[12] P. Aggarwal, D. Chu, V. Kadamby, and V. Singhal, Planning for end-to-end formal with simulation-based coverage, Proc. Formal Methods in Computer-Aided Design FMCAD 2011, Austin, TX, USA, (2011), pp.9-16.

[13] H. Foster, Applied Assertion-Based Verification: An Industry Perspective, Foundations and Trends in Electronic Design Automation, vol. 3, (Jan 2009).