Exploration of formal verification in GPU hardware IP

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.The advent of transistors in 1947 revolutionized the field of electronics and paved the way for development of first IC in 1949 by the German engineer Werner Jacobi. In 1965, Gordon Moore predicted that number of transistor per IC will double every year while their cost will get halved, which famously later come to known as Moore's law. For later part of most of 20th century, there has been a tremendous growth in advancement of IC's in terms of speed, size and capacity. Almost following the Moore's law, the IC's of today are million times more faster and bigger in size then the ones in 1970's. Although IC's continue to grow in design and complexity, the engineers at the same time start to get haunted by the question of reliability of these designs. Today advancement in machine learning, big data analytic, Internet of Things (IoT), autonomous vehicles are further fueling the innovation in hardware, thus, further worsening the challenges of test and verification of these designs. Verification almost account for nearly 70% of the overall design cost. Dynamic simulation has been the most popular choice of verification methodology for testing and verification of hardware designs. It has evolved over years by consolidating various diverse sets of methodologies into one now known as UVM. Although overall framework looks promising but it still has some way to go. While almost in parallel a new verification methodology was evolving in background called formal verification. During this thesis work, application of formal verification on DUT will be explored mostly from the point of view that it can be applied as an alternative verification methodology on a complete module inside a system and also that it can help to try and hit the corner case bugs which might be missed by the simulation verification