Formal Verification of Cache System Using a Novel Cache Memory Model

Authors: Guowei Hou, Lixin Yu, Wei Zhuang, Hui Qin, Xue Yang

Abstract:

Formal verification is proposed to ensure the correctness of the design and make functional verification more efficient. As cache plays a vital role in the design of System on Chip (SoC), and cache with Memory Management Unit (MMU) and cache memory unit makes the state space too large for simulation to verify, then a formal verification is presented for such system design. In the paper, a formal model checking verification flow is suggested and a new cache memory model which is called “exhaustive search model” is proposed. Instead of using large size ram to denote the whole cache memory, exhaustive search model employs just two cache blocks. For cache system contains data cache (Dcache) and instruction cache (Icache), Dcache memory model and Icache memory model are established separately using the same mechanism. At last, the novel model is employed to the verification of a cache which is module of a custom-built SoC system that has been applied in practical, and the result shows that the cache system is verified correctly using the exhaustive search model, and it makes the verification much more manageable and flexible.

Keywords: Cache system, formal verification, novel model, System on Chip (SoC).

Digital Object Identifier (DOI): doi.org/10.5281/zenodo.1099784

References:

[1] R. Drechsler, Advanced Formal Verification (M), Kluwer Academic Publishers, 2004.
[2] S. Srinivasan, P. S. Chhabra, P. K. Jaini, A. Aziz and L. John, “Formal Verification of a Snoop-based Cache Coherence Protocol using Symbolic Model Checking,” International Conference on VLSI Design, pp. 288-293, Jan. 1999.
[3] P. Dhakad, A. Katariya and A. Arya, “Performance Verification for Cache Memory of Multicore Processor,” International Conference on Computational Intelligence and Communication Network, pp. 622-627, Nov. 2010.
[4] LEON2 Processor User’s Manual: Version 1. 0. 30, Jul. 2005.
[5] D. L. Dill, A. J. Drexler, A. J. Hu and C. H. Yang, “Protocol Verification as a Hardware Design Aid,” VLSI in Computers and Processors, pp. 522-525, Oct. 1992.
[6] E. T. Schubert, “Formal Verification of an MMU and MMU Cache,” 3rd NASA Symposium on VLSI Design, vol. 4, 1991.
[7] T. J. Li, J. M. Zhang and S. K. Li, “An FPGA-based Random Functional Verification Method for Cache,” IEEE Eighth International Conference on Networking, Architecture and Storage, pp. 277-281, Jul. 2013.
[8] M. Tomasevic and V. Milutinovic, “A Simulation Study of Snoop Cache Coherence Protocols,” Hawaii International Conference on System Sciences, pp. 427-436, Jan. 1992.
[9] W. Grumberg and D. E. Long, “Model Checking and Modular Verification,” ACM Transaction on Programming Languages and Systems, pp. 843-871, 1991.
[10] A. Miczo, Digital Logic Testing and Simulation, 2nd edition, published by John Wiley & Sons, Inc., Hoboken, New Jersey, 2003.
[11] O. Rashinkar, P. Paterson and L. Singh, System-on-a-chip Verification Methodology and Techniques, Kluwer Academic Publishers, 2002.
[12] B. H. Bao, J. Bormann, M. Wedler, D. Stoffel and W. Kunz, “Formal Plausibility Checks for Environment Constraints,” Forum on Specification and Design Languages, pp. 13-18, Sep. 2012.