Design And Formal Verification Of Floating Point Estimate Module

Data processing is the most important feature of our time,as the emergence of new technologies such as artificial intelligence,deep learning and 5G,higher requirements are put forward for computing.Vector floating point unit supporting SIMD is widely used in the design of superscalar process nowadays.The data width of vector floating point unit is 128 bit,due to the huge input state space,it is almost impossible to ensure the completeness of test space for simulation,especially corner cases.Formal verification is applied to block and subunit level design in industry such as floating point unit due to systematic and efficient way to explore exhaustively all reachable state space.The estimate subunit of this thesis is able to complete the approximation to the reciprocal,squarer root reciprocal,exponential and logarithmic by piecewise linear approximate based on look-up table.The design is a good balance of speed and area and greatly improves the processor performance by supporting vector operation.The output of estimate subunit is approximate and needs to meet the relative error.The binary outputs need to be converted to decimal numbers for computing relative error which introduce complex arithmetic operations,the complex arithmetic operations will increase the state space rapidly and bring the explosion for formal engines based on BDD and SAT.In order to solve the problem of memory explosion,the paper adopts a variety of strategies based on the structure of estimate subunit.The mainstream formal verification tools realize RTL-RTL/RTL-GATE equivalence checking.The paper establishes reference model using C language and realizes RTL-C equivalence checking based on ATEC.