Formal Verification of Cache System Using a Novel Cache Memory Model

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.

• Guowei Hou
• Lixin Yu
• Wei Zhuang
• Hui Qin
• Xue Yang

• Cache system
• formal verification
• novel model
• System on Chip (SoC).

[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.