FPGA狀態機綜合可靠性探究 ①

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

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

0 引言

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

1 狀態機安全實現設置

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

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

圖1 XST綜合選項安全屬性設置

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

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

以下是一個狀態機的定義示例，使用safe_implementation設置了狀態機安全實現的綜合屬性，使用safe_recovery_state將恢復態指定為s1狀態。

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";

狀態機綜合后的編碼結果、安全實現結果等信息均可從綜合報告中進行查閱。

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

2 狀態機安全實現分析

將上述定義的狀態機設計成為s1至s5循環運轉的狀態機，作為設計輸入進行差異化分析。

對于XILINX公司FPGA開發，建立ISE工程，使用XST進行綜合，狀態機不設置安全屬性，綜合編碼結果如表1所示。

表1 狀態機編碼映射表

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

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

FFD1=FFD3 * FFD2

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

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

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

圖2 XILINX廠商FPGA未設置安全屬性的狀態機電路圖

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

對于這同一編碼，當狀態機設置安全屬性，其綜合報告提示狀態機設置了恢復態Recovery State為s1，即三級寄存器應為000。

綜合結果如圖3所示：

圖3 XILINX廠商FPGA設置安全屬性的狀態機電路圖

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

FFD1=FFD3*FFD2*!FFD1

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

FFD3=!FFD3*!FFD1

其工作方式仍為000→001→010→011→100→000→001……，當狀態機出現101,110,111的無效狀態時，狀態機的運行方式為101→000,110→000,111→000，與綜合報告恢復態數據一致。

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

圖4 ACTEL廠商FPGA未設置安全屬性的狀態機電路圖

由圖4可見，狀態機的運算多項式如下：

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

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

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

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

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

對于這同一編碼，當狀態機設置安全屬性，綜合結果如圖5所示：

圖5 ACTEL廠商FPGA設置安全屬性的狀態機電路圖

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

3 狀態機安全實現設置對邏輯等價性驗證的影響

FPGA設計從設計輸入到最終的燒錄程序要經過綜合、實現、布局布線等多個環節的網表轉化，為了驗證各環節轉化的網表功能相同，在FPGA驗證中會使用邏輯等價性的驗證方法。

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

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

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

第三步：映射關鍵點。等價性驗證工具會根據名稱或功能將兩個網表對應的關鍵點進行關聯，從而劃分出相應的組合邏輯。

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

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

圖6 關鍵點映射圖

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

4 結束語

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