丁宗杰，門(mén)永平，白正堯，陳 銳

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

0 引言

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

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

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

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

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

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

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

以下是一個(gè)狀態(tài)機(jī)的定義示例，使用safe_implementation設(shè)置了狀態(tài)機(jī)安全實(shí)現(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)機(jī)綜合后的編碼結(jié)果、安全實(shí)現(xiàn)結(jié)果等信息均可從綜合報(bào)告中進(jìn)行查閱。

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

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

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

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

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

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

各LUT查找表中運(yùn)算多項(xiàng)式如下所示：

FFD1=FFD3 * FFD2

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

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

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

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

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

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

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

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

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

FFD1=FFD3*FFD2*!FFD1

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

FFD3=!FFD3*!FFD1

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

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

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

由圖4可見(jiàn)，狀態(tài)機(jī)的運(yùn)算多項(xiàng)式如下：

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

4 結(jié)束語(yǔ)

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