COMPLEMENTING THE UVM VERIFICATION FRAMEWORK WITH FORMAL TECHNIQUES

The goal of any production is to reduce the cost of manufacturing and deliver high-quality products that take a long time to produce. At present, the verification phase carries an important role in the design. The verification represents the biggest amount of the cost of the design, which is about 70% of the total cost. This thesis aims to verify the Arithmetic Logic Unit (ALU) of the RISC-V processor, using the PULP platform [1], benefiting Formal Verification to assist and complete a UVM based simulation environment, explaining the design specifications and constraints. Finally showing how the Universal Verification Methodologies (UVM) and Formal Verification (FV) adopted and analyzing the comparison between these two methods of verification on a same module. Introduction The implemented Arithmetic Logic Unit is based on the RISC-V, which is a set of specifications defining the Instructions Set Architecture (ISA). Increasing the design complexity leads to having several methods for verification in terms of quality and reliability. In this thesis, several approaches were presented to verify the ALU unit in RISC-V, which include: •??UVM Simulation •??Formal Verification •??Bug Hunting FV •??Mutation The design under test (DUT) includes both combinational and sequential logic, each of which can be verified with these methods or with the help of each other. However, the purpose of this study is to achieve completeness and 100% proof for each of these areas in order to cover all the design space states and comparison between the verification methods. Proposed Approaches In the PULP design, ALU consists of 67 instructions which I verified as following: 1.UVM Simulation 2.Formal Verification 3.Bug Hunting FV 4.Mutation The result of these method's analyses and the number of failures instructions are compared in these methods, and it shows how important it is to use formal tools in order to save time and reach completeness in terms of checking all the design state space when the design is considerably large and complex. In particular, using the scoreboard in UVM simulation becomes very useful, when the design state space is small and doesn't have complexity. Also, by using Bug Hunting, it was concluded that the classic formal verification method needs more time and more resources to verify all the state space in the complex units, which contradicts the time required to bring it to the market. Finally, the mutation method could be extremely helpful for checking the quality of the testbench. Regarding the importance of time consuming and resources for the verification, still, some aspects need to be developed for this project. For the next step in this project, it is better to have a design parameterized so, that it can be easily abstracted in formal method. In addition to this, adding a formal tool's license, which means having more resources and using multiple engines at the same time for proofing the assertions, could speed up the verification process. Also trying to increase the assumptions and assertions and adding more cover points can be very constructive. Also, the Equivalence Checker tools can also be used in the Mutation part to validate the mutations to checks if both the main design and the mutated design are functionally equivalenced or not. Because if the functionality is equal in both designs, the mutation is not valid because the mutation must change the functionality.