| Summary: | 碩士 === 國立交通大學 === 資訊科學系 === 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.
|
|---|
