[ca] El propòsit principal d'un computador és computar, encara que a vegades aquest simple fet no es tingui en compte o inclús s'arribi a pensar que aconseguir que els computadors calculin com ho fem les persones, és trivial. Els computadors són capaços de fer còmputs per diferents tipus de dades, sent un d'ells els nombres re- als. Els nombres reals són un conjunt de números que engloba tots els nombres positius i 0 (els naturals), els negatius (que junt amb els naturals formen els en- ters), els racionals (tots els números que es poden representar com a una fracció de dos nombres enters) i finalment els nombres irracionals (tots aquells números que no es poden representar com la fracció de dos enters). Per gestionar l'aritmètica dels nombres reals en representació binària, estàndards i especificacions, s'han de- senvolupat al llarg del temps per establir regles sobre com s'haurien de representar aquests números en un computador i com s'haurien de gestionar els possibles casos excepcionals. Aquest subconjunt de l'aritmètica de computadors va rebre el nom d'aritmètica de coma flotant (a causa de la coma o punt que separa la part entera de la part fraccionària en un nombre real), i per suportar-la, es van començar a desenvolupar Unitats de Coma Flotant (UCF). En aquest projecte, ens marquem l'objectiu de verificar, és a dir, avaluar la correctesa d'una implementació d'UCF utilitzant la popular tècnica de verificació funcional amb UVM i experimentant amb l'alternativa verificació formal. Esperem poder extreure conclusions valuoses sobre les dues alternatives, veient com rendeixen quan s'intenta verificar un dels compo- nents més complexos dins de l'arquitectura d'un computador.

[en] The primary purpose of a computer is to compute, even though this simple fact is usually ignored or even thought that getting computers to calculate like humans is trivial. Computers are able to make calculations for many different data types, one of them being real numbers. Real numbers are the number set that encompasses all positive numbers and 0 (the natural numbers), all negative numbers (which, to- gether with the natural numbers, form the integer set), all rational numbers (all numbers that can be represented as the fraction of two integer numbers) and finally the irrational numbers (all numbers that can not be expressed as the quotient of two integer numbers). To manage arithmetic for real numbers, standards and spec- ifications have been defined over the years to establish rules on how these numbers should be represented and how the possible exceptional cases should be handled. This subset of computer arithmetic was given the name of floating-point arithmetic (because of the point or comma that separates the whole and the frac- tional part of a real number), and to support it, Floating-Point Units (FPU) started being developed. In this project, we aim to verify, that is, to assess the correctness of an FPU implementation using the popular technique of functional verification with UVM and experimenting with the alternative formal verification. We expect to extract valuable conclusions about both alternatives, seeing how they perform when trying to verify one of the more complex components inside the arquitecture of a computer.