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.