International Journal of Science and Research (IJSR)

International Journal of Science and Research (IJSR)
Call for Papers | Fully Refereed | Open Access | Double Blind Peer Reviewed

ISSN: 2319-7064


Downloads: 108 | Views: 183

Case Studies | Electronics & Communication Engineering | India | Volume 4 Issue 3, March 2015 | Rating: 6.6 / 10


Assertion-Based Formal Verification of CPU-Cache Crossbar of OpenSPARC T1 Processor

P. Vishnu Vardhan Reddy | Rajendra M. Patrikar


Abstract: Functional verification of complex designs, such as multi-core processors, is a challenging task in the entire verification cycle, because bugs which are not uncovered during this phase will carry on to the later design stages. The cost of fixing bugs is very high at later stages as compared to fixing them at the RTL implementation phase. Conventional verification methods like coverage-driven simulation techniques may not be able to uncover all the bugs due to their inability to exercise corner-case scenarios in a design. Formal methods like theorem proving, assertion-based verification are exhaustive and detect all corner-case bugs. This paper proposes an assertion-based formal approach for the verification of the CPU-Cache Crossbar module of the SPARC T1 processor, whose behavior is characterized by complex request patterns originating from the multiple cores to access shared resources such as the Level 2 cache memory banks, floating-point unit, and I/O Bridge ideal candidates for an assertion based formal verification approach.


Keywords: Arbiter, assertion-based verification, formal verification, multi-core processor


Edition: Volume 4 Issue 3, March 2015,


Pages: 1803 - 1806


How to Download this Article?

Type Your Valid Email Address below to Receive the Article PDF Link


Verification Code will appear in 2 Seconds ... Wait

Top