Formal verification of a theory of ieee rounding

1、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

2、 part formal veri?cation of a theory of ieee rounding christian jacobi saarland university,computer science department 66123saarbru cken,germany cjcs.uni-sb.de tel+49-681-302-4129,fax-4290 october12,2021 abstract.we report on the formal veri?cation of a theory of ieee rounding in the theorem prover

3、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 blo

4、cks,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 in6,15,a theory of ieee rounding was presented.this theory is used in15to prove the correctness of a?oating point unit(fpu).this paper des

5、cribes the formal veri?cation of this theory of rounding in the theorem prover pvs17.the veri?ed theory has been successfully used to formally verify the complete fpu3. the theory consists of a formalization of the ieee standard75411,and notations and theorems facilitating the veri?cation of?oating

6、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

7、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 pa

8、rtitions 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

9、 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?oati

10、ng 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 f

11、ormalization 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 depen

12、ds 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

13、ieee compliant?oating point unit3. 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 dlx9,15,a risc processor based on the mips instruction set.the v amp features an out

14、-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 built4.the veri?cation of the tomasulo cpu core is?nished12.the veri?cation of the cache has just be

15、gun.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,divis

16、ion(by newton-raphson iteration),comparisons,and conversion between the?oating point formats and between?oating point numbers and integers3. 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 hardwa

17、re 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 from6,15.the

18、paper-and-pencil proofs in6,15served 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 in6,15had bugs, and most proofs had gaps which had to be?lled for the formal veri?cation

19、. miner has previously formalized the ieee standard in pvs13.our de?nition of the rounding function is based on this work,since the de?nition in6,15is informal. miners formalization does not comprise theorems related to our-equivalence and round decomposition theorems. another formalization of the i

20、eee standard was given by harrison8in 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).harrisons for-malization has no counterpart to round decomposition.he has theorems related to the com

21、putation of exceptions of-equivalent numbers8,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 roundin

22、g 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 z2.in14,moore et

23、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.in1820,russinoff proves the correctness of the amd k5 square root,and the amd athlon square root,division,

24、and addition algorithms.his formalization of the rounding function and sticky bit computations is similar to14. 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 p

25、rojects 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,expon

26、ent,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

27、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

28、 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

29、 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

30、 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 w

31、here 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-fa

32、ctoring,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 f

33、acilitating 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

34、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

35、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

36、 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

37、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., addi

38、tion,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 miners de?nition13;it

39、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

40、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

41、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

42、-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 t

43、he 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

44、 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 re

45、turns0or2,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

46、-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?catio

47、n 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

48、-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.

49、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 in15.the ieee form

50、alizations by miner13 and harrison8do 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 hardware3.we have veri?ed the individual hardware components for-computation,signi?cand rounding,and post-normali

51、zation,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 tha

52、t 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 nea

53、rest 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 conformanc

54、e 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 o

55、f 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 round

56、ing modes. proof.part1is a trivial consequence of theorems1and2.part2and3rely on the following fact proved by miner in pvs13: 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 deco

57、mposition 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 p