Implementation of Formal Verification on Scalable Arbiter
V. S. Jagannatha Rao1, Siva Yellampalli2
1V. S. Jagannatha Rao, Sr. Lecturer, Department of ECE, SJBIT, Bangalore Centre, Yeshwanthpur, Bangalore India.
2Dr. Siva Yellampalli, Professor, UTL Technologies Ltd, VTU Extension, Bangalore India.
Manuscript received on 12 November 2014 | Revised Manuscript received on 22 November 2014 | Manuscript Published on 30 November 2014 | PP: 70-76 | Volume-4 Issue-6, November 2014 | Retrieval Number: F1865114614/14©BEIESP
Open Access | Editorial and Publishing Policies | Cite | Mendeley | Indexing and Abstracting
© The Authors. Blue Eyes Intelligence Engineering and Sciences Publication (BEIESP). This is an open access article under the CC-BY-NC-ND license (http://creativecommons.org/licenses/by-nc-nd/4.0/)
Abstract: In this paper, the Formal Verification (FV) approach is implemented on a scalable arbiter. Arbiters are a critical component in systems containing shared resources. FV is an approach using mathematical proof of ensuring that a design’s implementation matches its specification, and utilizes formal analysis techniques targeted at assertions within the RTL, to find design errors. The FV requires, properties and coverage to be written and the same is required to be coded using system verilog assertions (SVA). The key advantage of FV is that it does not require test benches to run and can be used to verify RTL codes very early in the design process. The implementation requires checking RTL design of arbiter, clock initialization, implementation of assertions, proving properties, coverage and tabulating the results, to ensure successful implementation. The results are analyzed by running the incisive formal verifier, (ifv), tool and checking for the properties and coverage which are written in SVA, for pass or fail.
Keywords: Formal Verification FV,Time to Market, System Verilog Assertions –SVA, Bug Free Silicon, Resusbality.
Scope of the Article: Expert Systems