一種基于數(shù)據(jù)相關性的亂序處理器驗證方法

摘要：亂序執(zhí)行是現(xiàn)代微處理器設計中普遍采用的提高流水線性能的方法，但亂序執(zhí)行并亂序退出的全亂序結構在超標量處理器中應用并不普遍，這種全亂序的結構對基于參考模型的處理器正確性驗證提出了巨大的挑戰(zhàn)。主要介紹了從處理器的程序行為是否正確的最終標準——程序員可見的結構變量按程序行為進行順序變化的角度對全亂序結構的處理器驗證提出了一種全新的解決方法。

關鍵詞：亂序執(zhí)行；數(shù)據(jù)相關性；流水線調(diào)度

中圖分類號：TP302文獻標識碼：A 文章編號：1009-3044(2011)04-0829-03

A Method for Verification of Out-of-order Processor Based on Data Dependencies

NING Yong-bo， LI Qian， LI Qiang， ZHANG Qi-bin

(Jiangnan Institute of Computing Technology， Wuxi 214083， China)

Abstract: Out-of-order instruction execution is widely used in modern microprocessors for improve the performance of pipeline. But those processors with both out-of-order execution and out-of-order retire are not at large. This takes great challenge for verification those processors with full out-of-order architecture. Then present a new approach to the verification of Out-of-order processor from the point of structure variable changed that according to the program at programmer-lever， which is the final slandered for verify the behavior of processor. Our approach can avoid the affect come from the indeterminacy of control flow.

Key words: out-of-order execution; data dependencies; pipeline dispatch

1 概述

隨著處理器技術的不斷發(fā)展，分支預測、亂序執(zhí)行、寄存器重命名、開發(fā)指令級并行和數(shù)據(jù)級并行的硬件機制、cache等技術不斷涌現(xiàn)，這些都是提高流水線性能的有效手段。其中亂序執(zhí)行(out-of-order execution)是目前處理器設計中應用較為廣泛的技術。亂序執(zhí)行，是指多條指令在消除了相關性之后可以不按程序規(guī)定的順序、發(fā)送給多個執(zhí)行部件并行執(zhí)行的技術。根據(jù)執(zhí)行部件的狀態(tài)和各指令能否提前執(zhí)行的具體情況分析后，將能提前執(zhí)行的指令立即發(fā)送給執(zhí)行部件執(zhí)行，由于各執(zhí)行部件的延時不一致，執(zhí)行結果可能不按規(guī)定順序給出。采用亂序執(zhí)行技術的目的是為了充分發(fā)揮各功能部件的并行性，提高發(fā)射寬度，從而提高CPU的運行程序的速度。在順序退出的處理器結構中，指令的提交順序由重排序緩沖將各執(zhí)行結果按指令順序重新排列，并按序退出，以保證程序行為上的正確。而在采用指令亂序寫回的處理器中，指令的退出及執(zhí)行結果寫回也是亂序的，這時程序的指令序①無法捕捉，但仍然保證程序的結構序②。

這些新技術不斷應用的同時，也給處理器的驗證工作提出了眾多挑戰(zhàn)[1]。本文在已有驗證工作的基礎上，根據(jù)指令間的數(shù)據(jù)依賴關系，針對這種全亂序結構處理器的驗證，提出了一種基于結構序的亂序處理器驗證方法，解決了亂序退出帶來的指令序無法捕捉的問題。

2 亂序的產(chǎn)生

為了提高流水線的性能，現(xiàn)代微處理器采用不同的調(diào)度策略。流水線調(diào)度策略主要有兩種：一是靜態(tài)調(diào)度，根據(jù)軟件的行為特征進行優(yōu)化來編譯調(diào)度指令代碼次序，主要依據(jù)程序未執(zhí)行時的行為特征和統(tǒng)計數(shù)據(jù)進行的調(diào)度策略；另一種是動態(tài)調(diào)度，通過硬件在程序執(zhí)行時重新安排代碼的執(zhí)行序列來減少競爭引起的流水線停頓時間。

現(xiàn)代微處理器大都采用動態(tài)調(diào)度技術，即允許處理器改變指令執(zhí)行的次序，以克服相關性，增加并行性。動態(tài)調(diào)度的算法有兩種：計分牌算法和Tomasulo算法。

記分牌算法：

記分牌是一集中控制部件，其功能是控制數(shù)據(jù)寄存器與處理部件之間的數(shù)據(jù)傳送。在記分牌中保存有與各處理部件相關聯(lián)寄存器中的數(shù)據(jù)裝載情況。當一個處理部件所要求的數(shù)據(jù)都已就緒（裝載完畢），記分牌允許處理部件開始執(zhí)行。在執(zhí)行完成后，處理部件通知記分牌釋放相關資源。所以在記分牌中記錄了數(shù)據(jù)寄存器和多個處理部件狀態(tài)的變化情況，通過它來檢測和消除或減少數(shù)據(jù)相關性，加快程序執(zhí)行速度。其思想是盡可能提早指令的執(zhí)行。當一條指令暫停執(zhí)行時，如果其他后繼指令與暫停指令及已發(fā)射的指令無任何相關，則仍然可以發(fā)射，執(zhí)行。

Tomasulo算法：

Tomasulo方法在記分牌算法的基礎上，采用的寄存器重命名的實現(xiàn)方法，把記分牌中的寄存器名用一大組虛擬寄存器的名來代替，即用虛擬寄存器集來代替真實的寄存器組，消除了WAR和WAW的假相關。Tomasulo算法主要分三步：發(fā)射、執(zhí)行和寫結果。該方法通過將有效的操作數(shù)保存在保留站中，避免指令直接從寄存器中讀取數(shù)據(jù)。當一條指令發(fā)射后，就在保留站中為其分配一個條目，用以保存該指令的操作碼和操作數(shù)。在該指令執(zhí)行完成后，其結果由數(shù)據(jù)總線送入目標寄存器中。

動態(tài)調(diào)度允許指令在資源得到滿足的情況下即可得到執(zhí)行，其帶來的問題就是指令的亂序執(zhí)行，指令的發(fā)射及執(zhí)行都有可能是亂序的。亂序執(zhí)行能夠在存在數(shù)據(jù)相關時，盡量避免暫停流水線。在亂序執(zhí)行處理器中，多采用重排序緩沖 (Re-Order Buffer ROB)結構來保證指令的退出是按照程序序的。重排序緩沖技術本質(zhì)上是一種寄存器重命名技術，它在指令提交時，要求必須按照程序序提交到存儲單元，指令執(zhí)行完畢后，便能保證最終結果順序提交。

3 常用驗證方法

對一個設計的功能驗證就是將設計者的意圖與觀察到設計的行為進行比較，來確定它的一致性[2]，目前常用的亂序執(zhí)行處理器功能驗證方法主要有形式驗證和參考模型驗證，此外還有采用邏輯演繹法進行驗證[3-4]。在順序執(zhí)行的處理器中，指令的執(zhí)行是順序的，其執(zhí)行結果依次寫入存儲單元中，寫入的過程也是嚴格按照程序的順序。而在亂序執(zhí)行處理器中，由于流水線可提供多個功能單元、并行執(zhí)行，因而指令可在資源得到滿足的情況下提前執(zhí)行，這就使得指令的執(zhí)行過程具有隨機性，與程序順序不吻合。其執(zhí)行流的不確定性，無法預知指令執(zhí)行的確切時間及順序，給指令級的驗證提出了挑戰(zhàn)。

形式驗證方法使用理論證明的方法，證明處理器模型的行為等同于處理器指令集架構（ISA），ISA將提供處理器指令級的抽象[5]。這種驗證方法在流水線及超標量處理器上應用較多，但亂序執(zhí)行處理器存在的指令間的并行性，造成了指令執(zhí)行的復雜性，使得處理器功能的抽象十分困難。Skakkebaek和Jones利用理論證明器SVC(Stanford Validity Checkered），采用分步驗證的方法，驗證了亂序執(zhí)行。該方法的第一步，首先將亂序處理器設計修改為一個順序抽象模型。在抽象的過程中，去掉了亂序邏輯，使得指令能夠順序執(zhí)行，解決了亂序調(diào)度帶來的問題，從而建立了亂序實現(xiàn)和順序抽象間的等價關系。第二步中，利用Burch和Dill提出的流水線自動排空的方法，證明了這個亂序抽象模型和ISA的功能是等價的。該方法在實現(xiàn)流水線排空時，需要編譯器的支持，在程序中添加標記。但隨著微處理器規(guī)模及復雜性的增大，這種形式驗證越發(fā)困難。

另一種是參考模型驗證法，它是業(yè)界在大規(guī)模IC的驗證中普遍采用的方法。針對指令級的驗證，參考模型的建模方法大多采用功能模型，但功能模型仍是一種順序模型，不能準確表示微結構中指令的亂序執(zhí)行和退出。由于全亂序微結構的設計中無法捕獲真正的指令序，所以如何用順序執(zhí)行的功能模型來驗證全亂序的微結構設計中執(zhí)行和退出的實時過程是否正確，是此驗證方法的重大挑戰(zhàn)。下面介紹一種基于結構序的亂序過程比較方法。

4 基于數(shù)據(jù)流的驗證

1）方法概述

為了解決亂序處理器中，由于指令亂序退出的不確定性帶來的驗證問題，本文提出了一種基于數(shù)據(jù)相關性的驗證方法，通過寄存器對執(zhí)行流進行再組織，形成針對某一寄存器的數(shù)據(jù)流，并與順序模型的數(shù)據(jù)流進行比對，以實現(xiàn)正確性的驗證。文中的驗證方法，需要使用一個順序執(zhí)行處理器參考模型，用作亂序模型的對照模型。程序中間結果的保存，主要有寫寄存器和寫主存兩種，文中只考慮寫回寄存的情況，處理寫回主存數(shù)據(jù)可采用類似方法。

無論是記分牌策略還是Tomasulo策略，都需要保證指令間的相關性。對于指令I和指令I’，若在程序順序中，指令I是最后一次對指令I’的源寄存器有寫操作，則這兩條指令間存在數(shù)據(jù)相關性，稱為寫后讀相關。此外，還有讀后寫和寫后寫相關。存在數(shù)據(jù)相關性的指令發(fā)射也是順序的。如圖1所示。

如果兩條指令間存在相關性，則它們的執(zhí)行順序必定和它們在程序中的順序是一致的，如圖中指令I1和I4之間的調(diào)度，由于指令I4需要用到源數(shù)據(jù)R1，來自指令I1的計算結果的寫回，它們直接存在數(shù)據(jù)相關性，因而它們的執(zhí)行必須是順序的，二者之間的調(diào)度次序與順序調(diào)度完全相同。

W.Damm和A.Pnueli使用形式驗證方法，通過建立一個非確定性抽象的ISA，并引入一個中間抽象層，驗證了亂序執(zhí)行[6]。在他們的方法中，證明了如果不存在預測執(zhí)行，亂序執(zhí)行和順序執(zhí)行處理器在運行相同程序時，會產(chǎn)生相同的中間結果，如對寄存器或存儲器寫回，即存在數(shù)據(jù)相關性的指令，它們對寄存器的寫回也是按照順序執(zhí)行的次序進行寫入的。這為數(shù)據(jù)流相關的驗證方法提供了理論依據(jù)。從W.Damm和A.Pnueli的證明可得出：

定理一：如果不存在預測執(zhí)行，一個亂序執(zhí)行處理器設計是正確的，當且僅當其中間結果與參考模型是等價的，即結構序是等價的。

2）寄存器模型建立

我們在方法中建立寄存器模型，并用此模型生成對應的數(shù)據(jù)流軌跡。通過與參考模型比較軌跡文件，實現(xiàn)對亂序處理器的驗證。由于記分牌和Tomasulo的調(diào)度不同，我們將分別對寄存器建立模型。

在采用記分牌調(diào)度的策略的處理器模型中，我們?yōu)槊總€寄存器增加一個唯一的標識位ID，用于標識寄存器號。對于每條發(fā)射的指令，根據(jù)其目標寄存器號唯一對應一個ID標識，記錄該指令的PC值以及寫入寄存器的數(shù)據(jù)。增加cnt位，作為寫回計數(shù)器，用以記錄程序對該寄存器的寫回次數(shù)。根據(jù)定理一可知，對于某一固定寄存器的每次寫回，其發(fā)起寫回的指令、寫回數(shù)據(jù)以及寫回次序與參考模型是等價的，因而該寄存器的數(shù)據(jù)軌跡也是相同的。即使存在循環(huán)指令，雖然其PC值可能相同，但寫入數(shù)據(jù)的順序不受影響。如圖2所示。

即在與參考模型的比對中，存在對任意的寄存器ID，若cntin-order=cntout-of-order，則必有PCin-order=PCout-of-order ，valuein-order=valueout-of-order。在軌跡比較過程中，如果亂序處理器中所有寄存器的數(shù)據(jù)流軌跡均和參考模型的軌跡相同，即二者在運行同樣程序時，中間結果寫回軌跡是相同的，則可認為此亂序處理器是正確的。

若要在Tomasulo調(diào)度策略下使用我們的方法，就需要解決該策略在處理兩種相關性所帶來的問題。

在消除讀后寫相關時，指令I需要先讀寄存器R1的數(shù)據(jù)，指令I’的結果要寫回R1。

ADDR2，R1，R3；//R1+R3－>R2指令I

MULR1，R4，R5；//R4×R5－>R1 指令I’

指令I和I’需要用到的操作數(shù)均已保存在保留站中，因而指令I’的執(zhí)行，不會改變指令I的源操作數(shù)，因而指令I的執(zhí)行不會受I’的影響。指令I’的源數(shù)據(jù)也已在保留站中，其執(zhí)行結果由數(shù)據(jù)總線寫入寄存器R1時，對數(shù)據(jù)流軌跡的改變不受流水線調(diào)度的影響。故Tomasulo算法在解決讀后寫相關時，不會對寫入寄存器的數(shù)據(jù)軌跡產(chǎn)生影響，因而仍然可以采用數(shù)據(jù)流相關的驗證方法。

在消除寫后寫相關時，指令I及指令I’同時發(fā)射，且均需要對寄存器R1進行寫回。

ADDR1，R2，R3；//R2+R3－>R1指令I

MULR1，R4，R5；//R4×R5－>R1 指令I’

它們的執(zhí)行順序可以隨機，但在程序序中Time I’> Time I，因而，指令I’對寄存器R1的寫回才是最終的寫回結果。在Tomasulo算法調(diào)度時，當產(chǎn)生連續(xù)寫入同一寄存器時，只有最后一次才進行寫回，之前的寫回操作則會被忽略。由于調(diào)度算法忽略了某些寄存器的寫入操作，因而造成了寄存器數(shù)據(jù)流軌跡與參考模型的不一致。

解決的方法是在記分牌策略的寄存器模型上，增加一個有效位Valid及一個標識位Tag，初始時值置為無效，如圖3所示。

在指令發(fā)射時，給每個以寄存器R為目標寄存器的指令添加一個標識位，指令標識信息的添加是按照程序順序遞增的，因而在當前發(fā)射的指令中，標識位最大的那個指令將最終寫回寄存器。當指令進行寫回時，通過查詢寫回指令對應的Tag位，將寄存器的Valid位置為有效。在與參考模型進行比較時，只對標識位有效的寄存器進行比較。

由于Tomasulo算法不支持預測執(zhí)行，所有發(fā)射的指令都會被執(zhí)行，其對寄存器的寫回數(shù)據(jù)均為有效數(shù)據(jù)，因而采用數(shù)據(jù)相關性驗證的方法具有較高的可信度。

5 結束語

流水線動態(tài)調(diào)度策略，通過允許指令的亂序執(zhí)行，最大化的提高了指令執(zhí)行的效率。亂序執(zhí)行在提高流水線的性能同時，也增加了驗證的復雜性。本文首先介紹了亂序問題產(chǎn)生的原因以及一些常用的亂序驗證方法，并對流水線的調(diào)度進行分析。針對執(zhí)行流不確定性的問題，提出了基于數(shù)據(jù)流的驗證方法，降低了驗證的難度，并實現(xiàn)了在采用記分牌及Tomasulo調(diào)度策略的處理器設計中的應用。但在預測執(zhí)行處理器中，由于預測執(zhí)行存在預測成功和預測失敗兩種情況，在預測失敗后需要對寫回的數(shù)據(jù)進行回退，影響數(shù)據(jù)流的軌跡，因而該方法只能在不存在預測執(zhí)行的處理器上使用。同時在實現(xiàn)時，還存在異步及中斷等事件的影響，造成了亂序處理器與參考模型在程序執(zhí)行上的不一致，導致軌跡比較的失敗。

注釋：

① 程序的指令序：程序中的指令順序。

② 程序的結構序：程序中結構變量（程序員可見的變量）的變化順序。

參考文獻：

[1] Taylor S，Quinn M.Functional Verification of a Muliple-issue，Out-of-Order，Superscalar Alpha Processor-The DEC Alpha 21264 Microprocessor[Z].1998.

[2] Glasser M，dam Rose，F(xiàn)itzpatric T.高級驗證方法學[M].王欣，俞俊，羅開杰，等，譯.成都:電子科技大學出版社，2007.

[3] Lahiri S K，Seshia S A，Bryant R E，et al.Modeling and Verification of Out-of-Order Microprocessors in UCLID 2001[EB/OL].http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.10.1301.

[4] Lahiri S K，Bryant R E.Deductive Verification of Advanced Out-of-Order Microprocessors[EB/OL].http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.65.8089.

[5] Skakkaebaek J U，Jones R B，Dill D L.Formal verification of out-of-order execution using incremental flushing[C]//Computer Aided Verification(CAV’98)，LNCS 1427，1998.

[6] Damm W，Pnueli A.Verifying out-of-order executions[C]//CHARME’97，1997.