Exploration of formal verification in GPU hardware IP

Abstract: Today, digital circuits are part of every ones daily life in form of mobile phones, computers, television, smart cards etc. The advent of new technologies such as internet of things, 5G etc. are continuously making the digital circuits more and more complex in design. With this increase in complexity comes the possibility of more bugs in the system. Finding and fixing these bugs is of paramount importance as it can lead to huge financial losses or can even be fatal especially in safety critical applications. Over the last few decades, traditional simulation based verification has been used as the default methodology to verify digital hardware designs. Although it has certain drawbacks such as: • It is not exhaustive in nature meaning that it is very tough to cover all the possible input test vector as part of input stimulus being applied to the test bench. • And due to its non-exhaustive nature, there will always be a possibility of missing bugs in the design especially the corner cases that can lower the design quality. Recently formal verification has been evolved as an attractive and more comprehensive alternative to simulation based verification. In this master thesis work, model checking (alternatively property based verification) has been applied as a preferred formal verification technique on a module inside the Arm Mali GPU hardware IP in order to try and hit the corner case design bugs, if any. The module or DUT chosen for investigation in this thesis work is FSDC. This is a new module and mainly consists of control path logic which suits formal verification. The DUT has already been extensively verified by simulation based verification. The result shown later for this thesis work highlights that: • Formal verification can be applied to a complete module as an alternative verification methodology. • After the application of formal verification on DUT, 3 design bugs were discovered which were missed by the simulation verification. Finally, based on above results and various challenges faced during this thesis work such as state space exploration problem or applying formal verification on complex parts of the design, it can be concluded that formal verification complements and at least provides a partial solution to the limitations of simulation based verification.