Validation of efficiency of formal verification methodology for verification closure

Sammanfattning: Application Specific Integrated Circuits (ASIC) and Field Programmable Gate Arrays (FPGA) verification is quite a time consuming phase in design flow cycle and it can be done using methodologies such as Universal Verification Methodology (UVM) and formal verification.The UVM methodology is simulation based verification where in the verifier will have to trigger the Design Under Test (DUT) manually by writing sequences which target different features of the DUT and the verification environment can also have verification directives such as assertions to spot design bugs. Formal verification on the other hand is purely assertion based verification where we describe the expected DUT behaviour using System Verilog Assertion (SVA) and we check for design sanity by exercising the assertions by letting the formal tool drive the inputs to the design in a constrained way. This completely eliminates the need of having to define sequences to drive the inputs. This thesis will bring up formal verification using jasper gold to light and will help verifiers to decide on how much of formal verification methodology can be used in verification of an IP with respect to the complexity of the design and the design behaviour to be verified. The results from this thesis proves how efficient formal verification was with respect to simulation based verification, to stress the design to test for corner case behaviour. The reason why formal verification cannot be extended for Top-Level Verification (TLV) and end to end functional verification is because of design complexity and this was also explored with the help of a complex ethernet design. Finally, a guideline as to when to use simulation based verification and formal verification was formulated.