Implemenation and Formal Verification of 64-bit Pipelined Floating Point Unit

• Main Authors: Yue-Fon Lin, 林裕峰
• Other Authors: Yirng-An Chen
• Format: Others
• Language: zh-TW
• Published: 2001
• Online Access: http://ndltd.ncl.edu.tw/handle/72816588406463752429

碩士 === 國立交通大學 === 資訊科學系 === 89 === In this thesis, we present an implemented design "Floating Point Unit", and extend Chen and Bryant's method to verify a pipelined arithmetic circuit. First, implement a 64-bit pipelined Floating Point Unit that supports IEEE double precision and all of four IEEE rounding modes. Then this design is verified with two methods, "Random Test Pattern Generation" and our verification system extended from "Chen and Bryant's method". Random test pattern generation method is to use test patterns generated randomly to do the simulation and the "Chen and Bryant's method" verifies designs by an extended word-level SMV using reusable specifications without knowing the circuit implementation. Word-level SMV is improved by using Multiplicative Power HDDs (*PHDDs), and by incorporating conditional symbolic simulation as well as a short-circuiting technique. Our verification method is based on the "Chen and Bryant's method" and extended to handle the pipelined arithmetic circuit. Based on a case analysis, the specification of the FP adder is divided into several hundred implementation-independent sub-specifications. The second method is extended to verify the pipelined arithmetic circuit. It only takes 7378.1 seconds for us to fully verify a 64-bit pipelined floating point unit.