Implementation of Formal Verification on Scalable Arbiter

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