@article{(Open Science Index):https://publications.waset.org/pdf/10000775,
	  title     = {Formal Verification of Cache System Using a Novel Cache Memory Model},
	  author    = {Guowei Hou and  Lixin Yu and  Wei Zhuang and  Hui Qin and  Xue Yang},
	  country	= {},
	  institution	= {},
	  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.
},
	    journal   = {International Journal of Electronics and Communication Engineering},
	  volume    = {9},
	  number    = {3},
	  year      = {2015},
	  pages     = {721 - 724},
	  ee        = {https://publications.waset.org/pdf/10000775},
	  url   	= {https://publications.waset.org/vol/99},
	  bibsource = {https://publications.waset.org/},
	  issn  	= {eISSN: 1307-6892},
	  publisher = {World Academy of Science, Engineering and Technology},
	  index 	= {Open Science Index 99, 2015},
	}