Formal verification of a theory of ieee rounding

Abstract. We report on the formal verification of a theory of IEEE rounding in the theorem prover PVS. The theory consists of a formalization of the IEEE standard, and notations and theorems facilitating the verification of floating point hardware. In part

Formal Veri?cation of a Theory of IEEE Rounding

Christian Jacobi

Saarland University,Computer Science Department

66123Saarbr¨u cken,Germany

cj@cs.uni-sb.de

Tel+49-681-302-4129,Fax-4290

October12,2001

Abstract.We report on the formal veri?cation of a theory of IEEE rounding

in the theorem prover PVS.The theory consists of a formalization of the IEEE

standard,and notations and theorems facilitating the veri?cation of?oating point

hardware.In particular,the concepts of-equivalence and round decomposition

are formalized,allowing for a subdivision of?oating point units into smaller

building blocks,which then can be veri?ed separately.The theory has been suc-

cessfully applied to the veri?cation of a fully IEEE compliant?oating point unit.

1Introduction

In[6,15],a theory of IEEE rounding was presented.This theory is used in[15]to prove the correctness of a?oating point unit(FPU).This paper describes the formal veri?cation of this theory of rounding in the theorem prover PVS[17].The veri?ed theory has been successfully used to formally verify the complete FPU[3].

The theory consists of a formalization of the IEEE standard754[11],and notations and theorems facilitating the veri?cation of?oating point hardware.Since the design of?oating point units is an error prone process and the correctness of the?oating point hardware strongly depends on the correctness of the rounding theory,we have formally veri?ed this rounding theory.

The major concepts of the theory are factorings,-equivalence,and round decom-position.Factorings are an abstraction of IEEE?oating point numbers,which allows talking about numbers instead of their bitvector encodings.This enables concise state-ments without having to deal with the actual IEEE formats and special cases(e.g., and NaN).

The concept of-equivalence partitions the real numbers into equivalence classes such that equivalent numbers are rounded to the same?oating point number.This en-ables the decomposition of the FPU into computational units(e.g.,adder and multi-plier),and a rounding unit.The computational unit delivers a result to the rounder that needs not to be the exact result of the operation but an equivalent result.The rounder therefrom computes the rounded?oating point number and the exceptions.The excep-tion computation is a central part of the rounding unit.

The process of rounding a real number to the appropriate representable?oating point number is split into three simple steps by means of round decomposition.This enables a similar decomposition of the rounding hardware into three smaller modules.

Abstract. We report on the formal verification of a theory of IEEE rounding in the theorem prover PVS. The theory consists of a formalization of the IEEE standard, and notations and theorems facilitating the verification of floating point hardware. In part

2 C.Jacobi

Furthermore,round decomposition is a useful tool for proving properties of the round-ing function.

The veri?cation of complex hardware systems such as FPUs depends on a sub-division of the system into smaller parts,which then are veri?ed separately.In this sense,-equivalence and round decomposition ease the problem of?oating point hard-ware veri?cation.This has been successfully applied in a project at Saarland University, where we formally veri?ed a fully IEEE compliant?oating point unit[3].

Project Status.The veri?cation of the theory of rounding is part of a larger project aiming to formally verify the V AMP microprocessor.The V AMP microprocessor is a variant of the DLX[9,15],a RISC processor based on the MIPS instruction set.The V AMP features an out-of-order Tomasulo scheduler,delayed branch,precise and nested interrupts,cache memory,and a fully IEEE compliant FPU.

We have veri?ed a library of basic circuits,upon which more complex circuits are built[4].The veri?cation of the Tomasulo CPU core is?nished[12].The veri?cation of the cache has just begun.The veri?cation of the?oating point theory and hardware is complete.The?oating point unit supports both single and double precision.Denormal numbers are handled in hardware.Exceptions are computed as mandated by the stan-dard.The supported operations are addition,subtraction,multiplication,division(by Newton-Raphson iteration),comparisons,and conversion between the?oating point formats and between?oating point numbers and integers[3].

The complete hardware of the V AMP processor is described on the gate level in PVS.We have developed a translation tool to automatically convert the PVS hardware description to Verilog HDL.The veri?ed V AMP processor will be implemented on a Xilinx FPGA.We have already converted the complete multiplication/division-FPU to Verilog and have implemented it on the FPGA.

Related Work.As mentioned above,the central concepts in this paper are taken from[6,15].The paper-and-pencil proofs in[6,15]served as guidelines in our for-mal veri?cation.The signi?cance of the proofs in this paper is that they are formally veri?ed;they are excerpts of the actual PVS proofs.1Some proofs in[6,15]had bugs, and most proofs had gaps which had to be?lled for the formal veri?cation.

Miner has previously formalized the IEEE standard in PVS[13].Our de?nition of the rounding function is based on this work,since the de?nition in[6,15]is informal. Miner’s formalization does not comprise theorems related to our-equivalence and round decomposition theorems.

Another formalization of the IEEE standard was given by Harrison[8]in the theo-rem prover HOL Light.Harrison does not discuss exponent wrapping,which introduces some ambiguities in the de?nition of the inexact exception(cf.Sect.4).Harrison’s for-malization has no counterpart to round decomposition.He has theorems related to the computation of exceptions of-equivalent numbers[8,Sect.5.3],but does not relate them to sticky-bit computations.However,this is essential to subdivide the FPU into computational units and a rounder unit in our veri?cation project.

Abstract. We report on the formal verification of a theory of IEEE rounding in the theorem prover PVS. The theory consists of a formalization of the IEEE standard, and notations and theorems facilitating the verification of floating point hardware. In part

Formal Veri?cation of a Theory of IEEE Rounding3 Barrett has speci?ed parts of the IEEE standard in Z[2].In[14],Moore et al.verify the AMD K5?oating point division algorithm.They have a de?nition of sticky bit computations,which is similar to our-equivalence.They do not describe exceptions and round decomposition.In[18–20],Russinoff proves the correctness of the AMD K5 square root,and the AMD Athlon square root,division,and addition algorithms.His formalization of the rounding function and sticky bit computations is similar to[14]. Russinoff does not cover denormals,exceptions,and round decomposition;however, he states that he handles denormals in unpublished work(private communication).

There are other veri?cation projects for?oating point hardware,e.g.,[1,5,16].All these projects use less intuitive formalizations of IEEE rounding.They do not cover denormals and exceptions.

2Factorings

2.1Basic De?nitions

We abstract IEEE numbers as de?ned in the standard to factorings.A factoring is a triple with sign bit,exponent,and signi?cand.Note that exponent range and signi?cand precision are unbounded.The value of a factoring is

The standard introduces an exponent width,from which constants

and are derived.These constants are used to bound the exponent range.

We call a factoring normal if and.A factoring is called denormal if and.We call a factoring an IEEE factoring if it is either normal or denormal.

Lemma1.A factoring(s,e,f)has zero value,iff.2

The next lemma states that nonzero IEEE factorings are unique:

Lemma2.Let and be IEEE-factorings with nonzero value.It holds

Zero has two IEEE factorings and,called and,respec-tively.

2.2IEEE Factorings

Next,we de?ne the normalization algorithm.We start by de?ning a function, which maps nonzero factorings to factorings with signi?cand between1and2:

Abstract. We report on the formal verification of a theory of IEEE rounding in the theorem prover PVS. The theory consists of a formalization of the IEEE standard, and notations and theorems facilitating the verification of floating point hardware. In part

4 C.Jacobi

We proceed with the de?nition of the function,which maps any(possibly zero) factoring to an IEEE-factoring.Let:

if and,

if and,

if.

The following lemma summarizes the most important properties of the normalization functions:

Lemma3.Let be an arbitrary factoring.It holds:3

1.,if,

2.,if,

3.,

4.is an IEEE-factoring.

Having de?ned the normalization algorithm,we de?ne conversion functions and, which assign factorings to reals:

for

for arbitrary

where if,and otherwise.4

Lemma4.Let.It holds:

1.if,

2.

Lemma5.Let with in the context of.It holds:

if and

otherwise.

Lemmas3to5are proved by de?nition unfolding.

Lemma6.Let be an arbitrary factoring with nonzero value.It holds

1.,i.e.,and coincide for normal numbers.

2.If,it holds.

3.If is an IEEE-factoring,it holds.

Statements1and2are simple consequences of lemma5.Statement3is proved by using lemma2with.

Abstract. We report on the formal verification of a theory of IEEE rounding in the theorem prover PVS. The theory consists of a formalization of the IEEE standard, and notations and theorems facilitating the verification of floating point hardware. In part

Formal Veri?cation of a Theory of IEEE Rounding5

2.3Representable Factorings

Let be the signi?cand precision as de?ned in the standard.A signi?cand is called representable,if has at most digits behind the binary point,i.e.,if. We call an IEEE-factoring semi-representable,if is representable.We call an IEEE-factoring representable,if it is semi-representable,and furthermore

holds.We call a real(semi-)representable,if is(semi-)representable.

Representable numbers exactly correspond to the representable numbers as de?ned in the mon values for are and,called single and double precision,respectively.However,the theory described here is not limited to these values of and.We only assume and.The standard de?nes an encoding of single and double precision IEEE factorings into bit strings of length32 and64,respectively.The idea behind factorings is to leave the bitvector level and argue about the more abstract factorings.This speeds up the veri?cation of hardware.

The following lemma bounds(semi-)representable numbers.

Lemma7.Let be a semi-representable factoring,and be an integer.It holds

1.,

2.,

3.is the largest representable number.

The following lemma characterizes the distance between distinct semi-represent-able factorings:

Lemma8.Let and be semi-representable factorings with values and,let,and be an integer.It holds

and

3Rounding

Since(semi-)representable numbers are not closed under arithmetic operations(e.g., addition,division),the IEEE-standards de?nes four rounding modes:round to near-est,round up,round down,and round to zero.In this section,we de?ne the rounding function,which maps arbitrary reals to semi-representable factorings according to the standard.The de?nition is similar to Miner’s de?nition[13];it only differs in cases of over?ow and under?ow(Sect.4).

3.1De?nition

We start with the de?nition of a function for each rounding mode

,which rounds reals to integers:

if

if

if

otherwise.

Abstract. We report on the formal verification of a theory of IEEE rounding in the theorem prover PVS. The theory consists of a formalization of the IEEE standard, and notations and theorems facilitating the verification of floating point hardware. In part

6 C.Jacobi

By scaling by,reals are rounded to rationals with fractional bits: Further scaling with,,yields the IEEE rounding function:

It is not obvious that this de?nition conforms with the IEEE standard.In section3.3we prove a theorem to convince the reader of the conformance.

3.2Decomposition Theorem

The decomposition theorem we prove in this section decomposes the computation of the rounding function into three steps:-computation(sometimes called pre-normalization in the literature),signi?cand rounding,and a post-normalization.The bene?t of having the decomposition theorem is that it simpli?es the design and veri?cation of rounder implementations.Furthermore,it is a powerful tool in other proofs,e.g.,in theorem7.

The-computation step computes the IEEE factoring,where is the number to be rounded.The signi?cand round step then rounds the signi?cand computed in the -computation to digits behind the binary point.This is formalized in the function :

where is an IEEE factoring,and is a rounding mode.The following lemma states some properties of the function:

Lemma9.

1.,

2.,

3.,

4.is an integer.

Part1follows by expanding the de?nitions of and.For parts2and3one expands the de?nition down to and applies basic properties of the?oor and ceiling functions.Part4is a direct consequence of the de?nition of.

In the case that the signi?cand round returns0or2,the factoring has to be post-normalized;if the signi?cand round returns0,the sign bit is forced to in order to yield.In case the signi?cand round returns2,the exponent is incremented,and the signi?cand is forced to1:

if,

if,

if. Theorem1.The result of the post-normalization is a semi-repre-sentable IEEE-factoring.

Abstract. We report on the formal verification of a theory of IEEE rounding in the theorem prover PVS. The theory consists of a formalization of the IEEE standard, and notations and theorems facilitating the verification of floating point hardware. In part

Formal Veri?cation of a Theory of IEEE Rounding7 Proof.The case is trivial.Assume. By lemma9.3we know,and hence since is an IEEE-factoring. Therefore is an IEEE-factoring,and with lemma9.4it is a semi-representable factoring.

Now assume.Since the input is an IEEE-factoring,we know,and hence is an IEEE-factoring;semi-representability now follows from lemma9.4.

Lemma10..

Proof.Apply lemma9.1and expand de?nitions.

Theorem2(Decomposition Theorem).For any real,and rounding mode

,it holds

Proof.For nonzero rounding results,the claim follows from lemmas6.3and10.Oth-erwise,the claim follows from the de?nitions of,and.

The IEEE factoring of the rounding result can therefore be computed by?rst com-puting the IEEE factoring of,then rounding the signi?cand,and?nally post-normal-izing the result.This decomposition of the rounding function is well known,but has been proved explicitly for the?rst time in[15].The IEEE formalizations by Miner[13] and Harrison[8]do not feature a counterpart of round decomposition.

The decomposition theorem has proved to be of great value in the veri?cation of the V AMP rounding hardware[3].We have veri?ed the individual hardware components for-computation,signi?cand rounding,and post-normalization,and have concluded the correctness of the rounding hardware by means of the decomposition theorem.We believe that the veri?cation of the rounding hardware without the concept of decompo-sition would have been far more complicated.

3.3Correctness of the Rounding Function

We now demonstrate that the de?nition of the IEEE rounding function conforms with the IEEE standard.The speci?cation of the round to nearest mode in the IEEE standard is as follows:

In this mode the representable value nearest to the in?nitely precise result

of any?oating point operation shall be delivered;if the two nearest repre-sentable values are equally near,the one with its least signi?cant bit zero shall be delivered.

Since our formal de?nition of the function does not obviously coincide with this informal de?nition,the following theorem is proved.This theorem hopefully convinces the reader of the conformance of our rounding de?nition.

Theorem3.Let and be a semi-representable number.

Abstract. We report on the formal verification of a theory of IEEE rounding in the theorem prover PVS. The theory consists of a formalization of the IEEE standard, and notations and theorems facilitating the verification of floating point hardware. In part

8 C.Jacobi

1.For any rounding mode,is semi-representable.

2.is a nearest semi-representable number:.

3.If there are two nearest numbers,then the one with least signi?cant bit zero is cho-

sen:and implies

is even.

Similar theorems exist for the three remaining rounding modes.

Proof.Part1is a trivial consequence of theorems1and2.Part2and3rely on the following fact proved by Miner in PVS[13]:

is even.

Let and.It is easy to adopt the above fact to the -function:

and(1)

is even.

We now prove part2.We may assume that,since otherwise the claim is trivial.From the decomposition theorem and the de?nition of the post-normalization we know that.Now ing lemma8(where we set

and)results in

(2) Using the triangle inequality,(1),and(2)together yield

(3) Equations(1)and(3)yield part2.Assume otherwise that.Since

we have,and therefore,since is an IEEE factoring.Hence .Lemma7.2with gives.Together this implies

(4) Again,(1)and(4)yield part2.The proof of part3is similar.

Similar informal speci?cations exist in the standard for the three remaining rounding modes,and conformance theorems for these have been proved in PVS.

Theorem4.For any real and rounding mode,is semi-representable,if and only if.

Proof.If,is semi-representable by theorem3.1.Conversely,if is semi-representable and,then the round result must equal by theorem3.2. The claim for the remaining rounding modes follows analogously from their respective conformance theorems.

Abstract. We report on the formal verification of a theory of IEEE rounding in the theorem prover PVS. The theory consists of a formalization of the IEEE standard, and notations and theorems facilitating the verification of floating point hardware. In part

Formal Veri?cation of a Theory of IEEE Rounding9 4Exceptions and Wrapped Exponents

The IEEE standard de?nes?ve exceptions:invalid operation(INV),division by zero (DIVZ),over?ow(OVF),under?ow(UNF),and inexact result(INX).The INV and DIVZ exceptions are trivial,and therefore not of interest in this paper.

The standard requires that each occurrence of an exception shall set a status?ag and call a trap handler.The trap handler can be disabled on the user’s request.We do not describe the actual handling of the status?ags and the trap handling,since this is part of the CPU,not part of the FPU.However,since the detection of exceptions,as well as the ?nal result of?oating point operations depend on whether the trap handlers are enabled or disabled,we need the enable?ags for the over?ow and under?ow exceptions OVFen and UNFen,respectively.They are provided by the CPU.

Over?ow.The standard de?nes the over?ow exception as follows:

The over?ow exception shall be signaled whenever the destination format’s largest?nite number is exceeded in magnitude by what would have been the rounded?oating-point result were the exponent range unbounded.

In lemma7we stated that is the format’s largest rep-resentable value.Since our rounding function by de?nition rounds as if the exponent range was unbounded above,we can de?ne the OVF exception as follows:

OVF

Here,is the exact result of a?oating point operation.The OVF exception depends on the rounding mode,since different rounding modes round large numbers differently to either,or to the next value outside the format’s range.

Under?ow.The standard de?nes the under?ow exception as follows:

Two correlated events contribute to under?ow.One is the creation of a tiny nonzero result between().The other is extraordinary loss of accu-racy

When an under?ow trap()is not enabled(),under?ow shall be signaled when both tininess and loss of accuracy have been detected.When an under-?ow trap()is enabled,under?ow shall be signaled when tininess is detected regardless of loss of accuracy.

For each of the contributing events,the standard leaves the choice between two different implementations.We use tininess before rounding(instead of after rounding)and inex-act result as loss of accuracy(instead if denormalization loss).Tininess before rounding occurs

when a nonzero result computed as though both exponent range and the precision were unbounded would lie strictly between.

This is formalized as

TINY

Abstract. We report on the formal verification of a theory of IEEE rounding in the theorem prover PVS. The theory consists of a formalization of the IEEE standard, and notations and theorems facilitating the verification of floating point hardware. In part

10 C.Jacobi

Here again,is the exact result of a?oating point operation,and therefore is“computed as though both exponent range and the precision were unbounded.”An inexact result occurs

when the delivered result differs from what would have been computed were both exponent range and precision unbounded.

We formalize this as

LOSS

Loss of accuracy only syntactically depends on the rounding mode,since this is a required parameter to the-function.From theorem4it follows LOSS

LOSS for distinct rounding modes.

Having de?ned tininess and loss of accuracy,we can de?ne the under?ow exception: UNF TINY LOSS UNFen

As mentioned above,the standard leaves other choices for the de?nition of TINY and LOSS.We refer the reader to[8,15]for lemmas about the relations between the different de?nitions.

Wrapped Exponent.In case of an over?ow or under?ow with corresponding traps enabled,the standard requests to deliver a biased result to the trap handler: Trapped over?ows()shall deliver to the trap handler the result obtained by dividing the in?nitely precise result by and then rounding.The bias adjust

is192in the single,1536in the double format.

Note that with exponent width and,respectively.Analo-gously to over?ows,trapped under?ows shall deliver the result obtained by multiplying the exact result with and then rounding.This is captured in the following de?nition. Again,is the exact result of a?oating point operation:

if OVF and OVFen

if UNF and UNFen

otherwise.

Now we are ready to de?ne the?nal?oating point result of operations yielding the exact result:

Multipliying the result with before rounding scales the result into the representable range.

Lemma11.Let be the exact result of an operation,and be a rounding mode.As-sume(this is ful?lled for operations).Let.

1.OVF

2.TINY

Abstract. We report on the formal verification of a theory of IEEE rounding in the theorem prover PVS. The theory consists of a formalization of the IEEE standard, and notations and theorems facilitating the verification of floating point hardware. In part

Formal Veri?cation of a Theory of IEEE Rounding11 The IEEE factoring of the wrapped result can therefore be computed by adding/sub-

tracting from the exponent of the exact-factoring.The above lemma is used in

conjunction with the decomposition theorem to round the wrapped result.

If an over?ow is detected with disabled trap,the de?nition above returns a

result exceeding.The standard however requests a?nal result of either

or,depending on the sign and the rounding mode.This is formalized as a case-split.We do not cover the details here,since this is a transliteration of Sect.7.3.of the

standard.

Inexact.The standard de?nes the inexact exception as follows:

If the rounded result of an operation is not exact or if it over?ows without an

over?ow trap,then the inexact exception shall be signaled.

It is not clear if the rounded result is meant to be without being wrapped

or,which potentially has been wrapped.Harrison[8]de?nes the inexact exception as

INX LOSS OVF

OVFen

This is the de?nition also used in IBM’s S/390[10,Pg.19-22]and in[15],e.g.It has the advantage that programs can distinguish exact(except for exponent wrapping)from

inexact computations in case of trapped over?ows and under?ows.For example,the above computation can be represented exactly after having been multi-plied with.

Harrison and we think that the standard is ambiguous in this point(personal com-munication).

5-Equivalence

We now de?ne the concept of-equivalence and-representatives[15].This concept is a very concise way to speak about sticky-bit computations.

Let be an integer.Two reals and are said to be-equivalent(),if

or if there exists some with,i.e.,if both and lie in the same open interval between two consecutive integral multiples of.Clearly,if such an exists,it must be.The-representative of is de?ned as

if

5The test-program is available at out website.

Abstract. We report on the formal verification of a theory of IEEE rounding in the theorem prover PVS. The theory consists of a formalization of the IEEE standard, and notations and theorems facilitating the verification of floating point hardware. In part

12 C.Jacobi

If is an integral multiple of,the representative of is itself,and the midpoint of the interval between the surrounding multiples of otherwise.The following lemma summarizes some important facts:

Lemma12.Let be reals,and be integers.

1.is an equivalence relation,

2.,

3.,(representative equivalence)

4.,and,(negative value)

5.,and,(scaling)

6.,(translation)

7.if,(coarsening)

8.,(zero value) Parts1-5are simple consequences of the de?nition,parts6-8are proved by induction on.

The following theorem describes equivalence on factorings:

Lemma13.Let be nonzero reals,

,and be an integer.It holds

1.,

2.and,

3.and,

4.and,

5.and.

Proof.Due to lack of space,we only prove part2.With lemma12.7it suf?ces to proof the claim for.By part1and lemma12.4we may assume.

Since the claim is trivial for,we further assume that

by de?nition of-equivalence.From lemma3.2,we know

,and therefore.We then have,and therefore

.Lemma5proves the claim.

Now we are ready to prove an important theorem,which allows the easy computa-tion of IEEE-factorings corresponding to representatives:

Theorem5.Let,let be the corresponding IEEE factoring,and let be an integer.The IEEE factoring of can be computed by computing the representative of:

Proof.From lemma13.1and13.3we know that and. From lemma5we know.With lemma12.4and12.5, we have.Lemma5gives,and hence .

Abstract. We report on the formal verification of a theory of IEEE rounding in the theorem prover PVS. The theory consists of a formalization of the IEEE standard, and notations and theorems facilitating the verification of floating point hardware. In part

Formal Veri?cation of a Theory of IEEE Rounding13

OR

puting representatives by sticky-computation

Next,we show that the representative of can be computed by a sticky bit computa-tion.Let be a real in binary format such that.Let be an integer,.The-sticky-bit of is the logical OR of all bits(cf.Fig.1):

Theorem6.With the above de?nitions,the representative of can be computed by replacing the less signi?cant bits by the sticky bit:

Proof.By de?nition,,and therefore. Furthermore,,iff.Applying this in the de?nition of proves the claim.

Theorems5and6together allow a very ef?cient computation of representatives (respectively their IEEE-factorings)by or-ing the less signi?cant bits in an OR tree,and replacing them by the sticky bit.This technique is well known[7],but introducing the formalism with-representatives allows for a very concise argumentation about these sticky computations.The veri?cation of the adder circuitry in[3],e.g.,relies heavily on the concept of-equivalence.

6Rounding Representatives

The valuable property of-representatives is that rounding and its representative yields the same result:

Theorem7.Let,,and be a rounding mode.It holds

Proof.In[15],this theorem is proved by geometrical arguments.It is technically very tedious to prove this theorem in the PVS theorem prover.We only give a sketch of the PVS proof.

By theorems2and5it suf?ces to show

By unfolding the de?nitions of and,this is equivalent to

(5)

Abstract. We report on the formal verification of a theory of IEEE rounding in the theorem prover PVS. The theory consists of a formalization of the IEEE standard, and notations and theorems facilitating the verification of floating point hardware. In part

14 C.Jacobi

Since the claim is trivial if,we can assume by the de?nition of-equivalence that,and with.Substituting in(5)yields

(6)

The theorem now follows from the next two lemmas(this“now follows”is the technically complicated part).Lemma14proves that the claim is correct if. Lemma15proves that the same cases apply in the de?nition of on both sides of equation(6).Then the claim again follows by lemma14.

Lemma14.For all and,it holds

Lemma15.For all,and,it holds

Lemma14can be proved by induction on,and some basic properties of the?oor and ceiling-functions from the PVS library.The proof,however,is technical and te-dious.The?rst part of lemma15is proved automatically by the PVS command grind, the second part needs little manual assistance.

From the above theorem,one can conclude that the wrapped and rounded result can be computed using equivalence,too.However,in case of trapped under?ow one needs more precision,namely-equivalence instead of-equivalence:

Theorem8.Let,,and be a rounding mode.It holds

Proof.This follows from lemma11and theorem7.

Not only the rounding can be accomplished by using the representative,but also the detection of exceptions.

Theorem9.Let,,and be a rounding mode.It holds

1.OVF OVF,

2.TINY TINY,

3.LOSS LOSS,

4.UNF UNF,

5.INX INX,where.Here one needs more

precision analogously to theorem8.

Abstract. We report on the formal verification of a theory of IEEE rounding in the theorem prover PVS. The theory consists of a formalization of the IEEE standard, and notations and theorems facilitating the verification of floating point hardware. In part

Formal Veri?cation of a Theory of IEEE Rounding15 Proof.Part1is an immediate consequence of theorem7.Part2follows from lemmas 13.4and13.5.Part3is slightly more complicated.We have to prove

By theorem4,this is equivalent to

is semi-representable is semi-representable

By theorem5and by de?nition of representability,this is equivalent to

We may assume,since otherwise the claim is trivial.Now assume

.Then and hence.In the other case

we have

Abstract. We report on the formal verification of a theory of IEEE rounding in the theorem prover PVS. The theory consists of a formalization of the IEEE standard, and notations and theorems facilitating the verification of floating point hardware. In part

16 C.Jacobi

[15].The concepts of-equivalence and round decomposition greatly simpli?ed the veri?cation of the hardware,since we could break up the hardware into smaller building blocks,which then were veri?ed separately.

Acknowledgments The author would like to thank Christoph Berg,Daniel Kr¨o ning, Silvia M¨u ller,Wolfgang Paul,and Jochen Preißfor valuable discussions. References

1.M.D.Aagaard and C.-J.H.Seger.The formal veri?cation of a pipelined double-precision

IEEE?oating-point multiplier.In ICCAD,pages7–10.IEEE,Nov.1995.

2.G.Barrett.Formal methods applied to a?oating-point number system.IEEE Transactions

on Software Engineering,15(5):611–621,May1989.

3. C.Berg and C.Jacobi.Formal veri?cation of the V AMP?oating point unit.In CHARME

2001,volume2144of LNCS,2001.

4. C.Berg,C.Jacobi,and D.Kroening.Formal veri?cation of a basic circuits library.In Proc.

of IASTED Int.Conf.on Applied Informatics,Innsbruck(AI2001).ACTA Press,2001.

5.Y.-A.Chen and R.E.Bryant.Veri?cation of?oating point adders.In CAV’98,volume1427

of LNCS,1998.

6.G.Even and W.Paul.On the design of IEEE compliant?oating point units.In Proceedings

of the13th Symposium on Computer Arithmetic.IEEE Computer Society Press,1997.

7. puter arithmetic.In[9],1996.

8.J.Harrison.A machine checked theory of?oating point arithmetic.In TPHOL’99,volume

1690of LNCS.Springer,1999.

9.J.L.Hennessy and puter Architecture:A Quantitative Approach.Mor-

gan Kaufmann,San Mateo,CA,second edition,1996.

10.IBM.z/Architecture Principles of Operation.Poughkeepsie,NY,Dec.2000.

11.Institute of Electrical and Electronics Engineers.ANSI/IEEE standard754–1985,IEEE Stan-

dard for Binary Floating-Point Arithmetic,1985.

12. D.Kroening.Formal Veri?cation of Pipelined Microprocessors.PhD thesis,Saarland Uni-

versity,Computer Science Department,2001.

13.P.S.Miner.De?ning the IEEE-854?oating-point standard in PVS.Technical Report TM-

110167,NASA Langley Research Center,1995.

14.J.S.Moore,T.Lynch,and M.Kaufmann.A mechanically checked proof of the AMD5K86

?oating point division program.IEEE Transactions on Computers,47(9):913–926,1998. 15.S.M.Mueller and puter plexity and Correctness.Springer,

2000.

16.J.O’Leary,X.Zhao,R.Gerth,and C.-J.H.Seger.IA-64?oating point operations and the

IEEE standard for binary?oating-point arithmetic.Intel Technology Journal,Q4,1999. 17.S.Owre,N.Shankar,and J.M.Rushby.PVS:A prototype veri?cation system.In CADE11,

volume607of LNAI,pages748–752.Springer,1992.

18. D.M.Russinoff.A mechanically checked proof of IEEE compliance of the?oating point

multiplication,division and square root algorithms of the AMD-K7processor.LMS Journal of Computation and Mathematics,1:148–200,1998.

19. D.M.Russinoff.A mechanically checked proof of correctness of the AMD K5?oating point

square root microcode.Formal Methods in System Design,14(1):75–125,Jan.1999.

20. D.M.Russinoff.A case study in formal veri?cation of register-transfer logic with ACL2:

The?oating point adder of the AMD Athlon processor.In Proceeding of FMCAD-00,vol-ume1954of LNCS.Springer,2000.

本文来源：https://www.bwwdw.com/article/lfg1.html