六十四位元管線化浮點運算器之實作及正規驗証

Abstract

在現今VLSI的製程技術越來越進步，越多的功能被整合進單一顆的晶片，換句話說只要一顆晶片就能擁有在這之前許多顆的晶片整合能來才的強大功能，這在效能上或是速度上都有顯著的差異。 以一般市場上處處可見的個人電腦(PC)來看，其中的心臟：中央處理器(CPU)。英特爾(INTEL)公司自從486的中央處理器開始，就將整個浮點運算器整合進去，而浮點運算器的功能顧名思義是用來專門處理浮點數方面的運算，意即數字方面有小點數的運算，這可以運用到平常生活中日漸熱門的3D遊戲中的3D材質的貼圖，幾何的顯示運算等等都扮演著一個相當重要的角色。 我們再從市場購買欲的觀點來看，在購買一顆中央處理器時，浮點運算處理器的能力也是成為要購買一個中央處理器時的一個重要指標。由此看來，浮點運算處理器在中央處理器中，是很重要的一個單元，因此，我們選擇了設計一顆浮點運算處理器。 但是考慮設計出一顆晶片時，不單只是要保証其速度上的快速，還要保証其功能上的正確性，舉例來說英特爾(INTEL)當時宣稱用了上兆個測試樣本(test pattern)，但從之前奔騰(Pentium)除法錯誤及後來的820晶片錯誤，在在都顯示出以模擬(Simulation)為主的方法，已無法完全確保其設計的正確性，因此，以正規驗証方法去驗証一個電路的正確性就成了一種趨勢了。為了証明正規驗証的效率，在實驗中我們還採取了亂數產生的測試樣本(Random Generation Test Pattern) 去做模擬的驗証。 因此，我們先設計一個六十四位元管線化浮點運算器，再利用上述提及的兩種方法去做驗証，在正規驗証的方法方面，這裡是採用陳盈安博士及 Randle E. Bryant博士的方法，進而擴充去驗証一個管線化的電路；而在另一個方法，則是利用亂數去產生測試樣本，實驗結果上顯示，正規驗証的方法能較有效的去驗証我們所設計的浮點運算器。

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.