丁宗杰，門永平，白正堯，陳 銳

(中國空間技術(shù)研究院 西安分院，西安 710000)

0 引言

FPGA研制過程一般需進行設(shè)計輸入、設(shè)計綜合、實現(xiàn)與布局布線、芯片編程等幾個階段。設(shè)計輸入是將所設(shè)計的系統(tǒng)或電路以開發(fā)軟件要求的某種形式表示出來，并輸入給EDA工具的過程，常用的方法有硬件描述語言(HDL)和原理圖輸入方式等。設(shè)計綜合是將設(shè)計輸入編譯成基本邏輯單元組成的邏輯連接網(wǎng)表。針對狀態(tài)機，綜合器提供了一個名為安全實現(xiàn)的綜合屬性，綜合器根據(jù)該屬性設(shè)置的不同對設(shè)計輸入的狀態(tài)機完成不同的網(wǎng)表轉(zhuǎn)化，從而使綜合后的邏輯網(wǎng)表表現(xiàn)出不同的功能。本文結(jié)合常用的XILINX公司的ISE集成開發(fā)環(huán)境和ACTEL公司的LIBERO集成開發(fā)環(huán)境對FPGA狀態(tài)機安全實現(xiàn)綜合屬性的作用與應(yīng)用進行分析與探究，同時通過等價性驗證的方式分析狀態(tài)機安全實現(xiàn)設(shè)置對網(wǎng)表轉(zhuǎn)化的影響。

1 狀態(tài)機安全實現(xiàn)設(shè)置

ISE集成開發(fā)環(huán)境下的XST綜合器和LIBERO集成開發(fā)環(huán)境下的Synplify綜合器可進行FPGA狀態(tài)機的安全實現(xiàn)。狀態(tài)機的安全實現(xiàn)是通過綜合器增加的邏輯電路使狀態(tài)機從一個非法狀態(tài)恢復(fù)到特定狀態(tài)，當狀態(tài)機運行進入一個無效狀態(tài)時，通過綜合器增加的邏輯，可以使狀態(tài)機恢復(fù)到一個已知態(tài)，我們一般將該狀態(tài)稱之為恢復(fù)態(tài)。該功能被稱為狀態(tài)機安全實現(xiàn)。

使用XST綜合器應(yīng)用狀態(tài)機安全實現(xiàn)可以通過設(shè)置綜合選項方式和應(yīng)用safe_implimentation約束的方式。綜合選項設(shè)置方式是打開XST綜合選項面板，在HDL Options選項中設(shè)置-safe_implementation參數(shù)，該參數(shù)默認值為“NO”，即不進行狀態(tài)機安全屬性設(shè)置，當將該參數(shù)設(shè)置為YES時，則XST進行狀態(tài)機安全實現(xiàn)綜合。安全屬性設(shè)置如圖1所示。

圖1 XST綜合選項安全屬性設(shè)置

使用safe_implimentation約束的方法是在代碼中使用attribute safe_implementation語句來進行狀態(tài)機安全屬性設(shè)置。

XST對狀態(tài)機進行安全屬性設(shè)置，其恢復(fù)態(tài)默認為復(fù)位時的狀態(tài)，也可以通過safe_recovery_state參數(shù)將恢復(fù)態(tài)指定為特定的狀態(tài)。

以下是一個狀態(tài)機的定義示例，使用safe_implementation設(shè)置了狀態(tài)機安全實現(xiàn)的綜合屬性，使用safe_recovery_state將恢復(fù)態(tài)指定為s1狀態(tài)。

typestate_type is (s1,s2,s3,s4,s5);

signal state,next_state: state_type ;

attributefsm_encoding : string;

attributefsm_encoding of state,next_state : signal is "sequential";

attributesafe_implementation : string;

attributesafe_implementation of state,next_state: signal is "yes";

attributesafe_recovery_state : string;

attributesafe_recovery_state of state,next_state : signal is "s1";

狀態(tài)機綜合后的編碼結(jié)果、安全實現(xiàn)結(jié)果等信息均可從綜合報告中進行查閱。

在使用Synplify綜合器對ACTEL公司FPGA進行設(shè)計時，可以在Synplify中建立sdc約束文件，在sdc文件中的attributes面板中進行狀態(tài)機的安全屬性設(shè)置。也可在代碼中通過增加attribute syn_encoding進行設(shè)置。

2 狀態(tài)機安全實現(xiàn)分析

將上述定義的狀態(tài)機設(shè)計成為s1至s5循環(huán)運轉(zhuǎn)的狀態(tài)機，作為設(shè)計輸入進行差異化分析。

對于XILINX公司FPGA開發(fā)，建立ISE工程，使用XST進行綜合，狀態(tài)機不設(shè)置安全屬性，綜合編碼結(jié)果如表1所示。

表1 狀態(tài)機編碼映射表

狀態(tài)s1至狀態(tài)s5分別對應(yīng)000至100。其綜合后電路如圖2所示，state[1]至state[3]分別對應(yīng)FFD1至FFD3寄存器：

各LUT查找表中運算多項式如下所示：

FFD1=FFD3 * FFD2

FFD2= (!FFD3*FFD2 )+(FFD3*!FFD2)

FFD3= (!FFD3*FFD2)+(!FFD3*!FFD1)

狀態(tài)機state[1:3]運行方式為：000→001→010→011→100→000→001……，綜合后狀態(tài)機運行方式與設(shè)計輸入相同。

圖2 XILINX廠商FPGA未設(shè)置安全屬性的狀態(tài)機電路圖

當狀態(tài)機出現(xiàn)101,110,111的無效狀態(tài)時，狀態(tài)機的運行方式為101→010,110→011,111→100，從這個例子可以看到該狀態(tài)機恢復(fù)到了一個有效狀態(tài)，但不可控不確定。

對于這同一編碼，當狀態(tài)機設(shè)置安全屬性，其綜合報告提示狀態(tài)機設(shè)置了恢復(fù)態(tài)Recovery State為s1，即三級寄存器應(yīng)為000。

綜合結(jié)果如圖3所示：

圖3 XILINX廠商FPGA設(shè)置安全屬性的狀態(tài)機電路圖

增加安全屬性綜合后，電路相對于之前寄存器位置和查找表發(fā)生了一定的變化，其狀態(tài)機運算多項式如下：

FFD1=FFD3*FFD2*!FFD1

FFD2=(!FFD1*!FFD2*FFD3)+(!FFD1*FFD2*!FFD3)

FFD3=!FFD3*!FFD1

其工作方式仍為000→001→010→011→100→000→001……，當狀態(tài)機出現(xiàn)101,110,111的無效狀態(tài)時，狀態(tài)機的運行方式為101→000,110→000,111→000，與綜合報告恢復(fù)態(tài)數(shù)據(jù)一致。

對于ACTEL公司FPGA開發(fā)，建立Libero工程，使用synplify進行綜合，狀態(tài)機不設(shè)置安全屬性，狀態(tài)機綜合編碼方式與上述XILINX公司FPGA設(shè)計保持一致，綜合結(jié)果如圖4所示：

圖4 ACTEL廠商FPGA未設(shè)置安全屬性的狀態(tài)機電路圖

由圖4可見，狀態(tài)機的運算多項式如下：

state[0]= !state[2]*!state[0]

state[1]= state[0]^ state[1]

state[2]= state[1]* state[0]

狀態(tài)機state[2]state[1]state[0]運行方式為：000→001→010→011→100→000→001……

當狀態(tài)機出現(xiàn)101,110,111的無效狀態(tài)時，狀態(tài)機的運行方式為101→010,110→010,111→100，從這個例子可以看到該狀態(tài)機恢復(fù)到了一個有效狀態(tài)，但不可控不確定。

對于這同一編碼，當狀態(tài)機設(shè)置安全屬性，綜合結(jié)果如圖5所示：

圖5 ACTEL廠商FPGA設(shè)置安全屬性的狀態(tài)機電路圖

增加狀態(tài)機安全屬性后，綜合的電路和未增加安全屬性的電路發(fā)生了一定的變化。電路A部分仍然是三級寄存器組成的狀態(tài)機，其工作方式仍為000→001→010→011→100→000→001……，電路B和電路C則是額外增加部分。電路B部分的組合邏輯，將狀態(tài)機的有效狀態(tài)和無效狀態(tài)做了區(qū)分，分別輸出邏輯0和邏輯1。電路B的輸出經(jīng)過電路C的兩級寄存器state_illegalpipe1和state_illegalpipe2采樣后與外部復(fù)位共同作用在狀態(tài)機的異步復(fù)位/置位端。該電路中一旦狀態(tài)機出現(xiàn)無效狀態(tài)，則會通過電路B和電路C向狀態(tài)機發(fā)送一個復(fù)位信號，對狀態(tài)機進行自復(fù)位。

3 狀態(tài)機安全實現(xiàn)設(shè)置對邏輯等價性驗證的影響

FPGA設(shè)計從設(shè)計輸入到最終的燒錄程序要經(jīng)過綜合、實現(xiàn)、布局布線等多個環(huán)節(jié)的網(wǎng)表轉(zhuǎn)化，為了驗證各環(huán)節(jié)轉(zhuǎn)化的網(wǎng)表功能相同，在FPGA驗證中會使用邏輯等價性的驗證方法。

邏輯等價性驗證工具采用數(shù)學方法直接比對各階段網(wǎng)表的一致性，其基本思想是，對于做比對的兩個網(wǎng)表如果對于所有可能的輸入其輸出也一致，則證明輸入輸出間的組合邏輯正確，即網(wǎng)表一致。邏輯等價性工具一般按以下步驟執(zhí)行驗證。

第一步：讀取網(wǎng)表。將待比對的兩個網(wǎng)表分別定義為golden(經(jīng)驗證的)和revised(待修訂的)網(wǎng)表，由等價性驗證工具讀取。根據(jù)golden網(wǎng)表來核對其它設(shè)計網(wǎng)表(綜合后網(wǎng)表，布局布線后網(wǎng)表)。設(shè)計流程中任何階段生成的網(wǎng)表都可以用作golden網(wǎng)表，如綜合前網(wǎng)表、布局布線后網(wǎng)表。設(shè)計輸入的網(wǎng)表是最常被采用的golden網(wǎng)表。

第二步：設(shè)置關(guān)鍵點。遵循等價性驗證的基本思想，驗證工具把網(wǎng)表劃分成許多基本的小段，稱為“邏輯錐”。如果所有的邏輯錐等價，則整個網(wǎng)表等價。邏輯錐的輸入輸出就是關(guān)鍵點。關(guān)鍵點主要由網(wǎng)表的基本輸入輸出、觸發(fā)器、寄存器、黑盒子等元素構(gòu)成。

第三步：映射關(guān)鍵點。等價性驗證工具會根據(jù)名稱或功能將兩個網(wǎng)表對應(yīng)的關(guān)鍵點進行關(guān)聯(lián)，從而劃分出相應(yīng)的組合邏輯。

第四步：比對。驗證工具按照數(shù)學方法給邏輯錐輸入激勵，比對輸出，從而驗證邏輯錐的等價性。如果所有邏輯錐都等價，則兩個網(wǎng)表等效。否則調(diào)試非匹配點，確認問題，修改設(shè)計，再次進行比對。

安全屬性使綜合器對設(shè)計增加了額外恢復(fù)電路，從其含義及設(shè)置前后的電路來看綜合后網(wǎng)表與設(shè)計輸入的網(wǎng)表不應(yīng)等價。這里使用的邏輯等價性工具對圖5的設(shè)計輸入與綜合后網(wǎng)表進行驗證，可以看到綜合后網(wǎng)表多出兩個無法映射的關(guān)鍵點，見圖6的state_illegalpipe1和state_illegalpipe2，這兩個關(guān)鍵點對應(yīng)圖5的電路C部分。

圖6 關(guān)鍵點映射圖

對比golden和revised電路圖時可以看到，綜合前狀態(tài)機的復(fù)位只由外部復(fù)位reset決定。而綜合后同一寄存器的復(fù)位由外部復(fù)位reset和內(nèi)部寄存器state_illegalpipe1、state_illegalpipe2輸出信號共同決定，綜合前后的網(wǎng)表已不等價。在將state_illegalpipe1或state_illegalpipe2綁定為不使狀態(tài)機復(fù)位的常量后，綜合前后的網(wǎng)表邏輯等價。

4 結(jié)束語

設(shè)置綜合器的狀態(tài)機安全屬性可以由工具對設(shè)計輸入進行分析并增加額外處理電路，以增強狀態(tài)機運行的可靠性。綜合器默認綜合后電路與設(shè)計輸入保持一致，未應(yīng)用安全屬性，在開發(fā)時可進行相應(yīng)的設(shè)置，同時審查綜合報告對狀態(tài)機綜合結(jié)果進行確認。