一種面向SRAM 型FPGA 的三模冗余分區自修復方法研究*

王 鵬，劉正清，田 毅

（中國民航大學 適航學院，天津 300300）

0 引言

隨著航天技術的蓬勃發展，航天系統對電子器件的性能要求越來越高。在航天電子設備的設計中，基于SRAM 的FPGA 由于其現場可編程性、維修成本低等優點，使其比專用集成電路（Application Specific Integrated Circuits，ASICs）更有優勢。航天環境中的電子系統設計，不僅要滿足對性能的需求，數據傳輸時的可靠性和電子系統的可用性也必須得到保證。暴露在高電磁輻射中，工作中的電子器件會持續受到高能粒子撞擊以致輻射效應，如單粒子翻轉（SEU）等[1]，由輻射引起的單粒子翻轉在導致空間環境中電子系統失效的原因中占很大的比例。所以需要提高電路的抗輻射干擾能力。

三模冗余（TMR）是一種廣為人知的抗干擾容錯技術，可以對單粒子翻轉有較好的容錯效果[2]。該方法使用3個相同的邏輯塊同步執行相同的任務，每個邏輯塊相應的輸出通過表決器比較并進行多數表決，進而在一定時期將故障產生的影響屏蔽起來，使得發生故障的電路依舊可以在一段時間里繼續工作。這種方式并未將故障解決，隨著故障的持續增加，系統仍然有發生失效的可能性。所以如果使三模冗余電路具有一定的自修復能力，則可提高系統的可用性，圖1 即為一個標準的TMR 結構。本文從自修復的角度對傳統的三模冗余進行分區改進，并分析分區和刷新頻率對系統可用性帶來的影響。

圖1 標準TMR 結構

1 TMR 分區

在基于SRAM 型FPGA 中，用戶的組合和時序邏輯都是由定制邏輯存儲單元實現的，也就是SRAM 單元。當翻轉發生在FPGA 中的綜合組合邏輯中時，它實際對應于LUT 單元或在控制布線單元的一個位翻轉。在LUT存儲單元翻轉意味著組合邏輯發生了改變。影響只能在配置位流的下一次載入時才會被修正。這種翻轉的效果與LUT 定義的組合邏輯的固定故障（1 或0）相關。這意味著，除非使用一些檢測技術，在FPGA 的組合邏輯發生的翻轉將被存儲單元鎖存。布線的翻轉可以連接或斷開陣列中線的連接，可能產生有永久的影響，其效果可以映射到FPGA 實現的組合邏輯的一個開路或短路回路。故障也將在配置位流的下一次加載被修正。

需要注意的是使用TMR 本身是不夠的，為了避免FPGA 的錯誤，還要求比特流強制性不斷地進行重新加載，這就是所謂的刷新過程。刷新使系統能夠修復SEU導致的配置存儲器的錯誤而不破壞其操作。在本研究中使用盲刷新（定時刷新）來進行修復SEU 的操作[3]。盲刷新的優勢在于可以不用精確定位故障點，減少操作；劣勢在于需要將整體目標電路配置全部刷新，如果周期設置得不合理，將大大降低目標電路的使用時間[4]。

將兩種技術結合可以在容錯的基礎上增加自修復的能力，將單純的容錯電路轉化為可以定時修復故障的容錯電路，可以有效減少故障累積。

2 模型檢測

模型檢測是一種成熟的驗證技術，用于驗證有限狀態的系統的正確性[5]。給定系統的模型，根據標記的狀態轉換和與時間邏輯相關的屬性進行仿真計算，模型檢查算法會遍歷系統中有可能出現的所有狀態以驗證系統的性能。概率模型檢查可以對表現出隨機行為但狀態有限的系統進行建模。在本文中由于需要利用系統的數據流圖來進行建模，所以使用具有過渡和狀態標簽的連續時間馬爾科夫模型來進行隨機建模。

在本文中將使用PRISM 驗證工具[6]來進行建模和分析，文獻[7-8]中表明可以使用PRISM 驗證工具進行構建馬爾科夫模型。首先對分區三模冗余，使用連續時間馬爾科夫鏈對系統進行建模。然后利用系統的數據流圖，對分區數量、刷新頻率等參數進行預期。最后使用PRISM 驗證使用概率瞬態邏輯[9]表示的與系統可用性相關的屬性。

3 模型建立及定量分析

3.1 模型建立

在本文中選擇的待測電路為FIR 濾波器電路。濾波器通常用于數字通信系統中，例如信號分離、降噪等。對于從衛星到無人飛行任務中的所有航天應用，通信都是一個基本問題，所以數字濾波器在此類系統中非常重要[10]。為了說明此方法的適用性，故使用SCU 模型分析8 比特64 抽頭FIR 濾波器，FIR 濾波器在有足夠運算能力的前提下可以無限增加精度[11]。N 抽頭FIR 濾波器的離散脈沖響應可以表示為：

其中，x[ ]、y[ ]和h[ ]分別表示輸入、輸出和單位脈沖響應。

每個分區中的一行模件組合定義為一個域，每個域的故障率即由所有模塊的故障率和表決器的故障率加和決定。

其中，λi表示模塊i 的故障率，λvoter表示表決器的故障率。

在TMR 中，雖然同一分區中每個域在物理上是獨立的，但故障率相同，所以每個分區的故障率λP為：

圖2 顯示了一個雙分區TMR 數據流圖。第二分區中比第一分區多了3 個表決器，其中每個模件的故障率λm為：

圖2 待測電路雙分區三模冗余數據流圖

在本文的實驗中，λbit=5.79×10-13SEUs/bit/s 代表了30 000 英尺高度SRAM 芯片IMS1601 的SEU 概率[12-13]，Nkey表示關鍵比特數量，關鍵比特數量可以從模件的表征庫（Characterization Library）查詢到[14]。

基于每個域的故障率、用戶定義的分區數量和刷新頻率，然后構建系統的連續時間馬爾科夫模型并使用PRISM 建模語言進行編碼。之后使用PRISM 模型檢查器驗證不同的可靠性和可用性屬性，根據定量分析的結果來評估系統是否符合要求。

首先從TMR 的每個分區開始建模，定義一個有N個分區的系統為：

其中，每個Pi∈P 表示一個TMR 分區。

對于單粒子翻轉模型，每個模塊的失效是獨立的。由于配置IP（導致單粒子翻轉發生）產生的故障時間呈指數分布，假定配置刷新概率也遵循指數分布，即μ=1/τ，其中τ 表示刷新間隔[15-16]。

圖3 顯示了一個可自動修復TMR 的馬爾科夫模型。最左邊的模塊表示三模電路有3 個域正常運行，此時分區的失效率是3λ；中間的有兩個域正常運行，失效率是2λ；最右邊的只有一個域正常運行，系統失效。在這個模型中μ 代表刷新頻率。

圖3 一個可自動修復三模冗余馬爾科夫模型

每個Pi∈P 都可以被描述為一個連續時間馬爾科夫模型。定義：

圖4 顯示了一個雙分區可自動修復的三模冗余馬爾科夫模型。其中λpj和λpi分別表示兩個分區的失效率。狀態④，⑤，⑦，⑧表示系統可運行；狀態0，①，②，③表示系統失效。系統運行情況可由下式表示：

圖4 雙分區三模冗余的單粒子翻轉馬爾科夫模型

在本文的分析中，生成了3 種馬爾科夫模型，分別為無分區、雙分區和四分區。模型的復雜度從無分區到四分區的總狀態數和轉換次數隨著分區數量的增加而增加，分區會變得比較復雜，因為在單獨的域中對同步的SCU 進行建模需要越來越多的轉換，為了能夠保持這種建模方式的可管理性，將每個分區分別作為PRISM 語言中的模塊，并利用PRISM 模型檢查工具進行模塊的并行組合（代表TMR 分區），以生成完整的分析模型。表1為通過PRISM 建模及仿真出的模型狀態統計。

表1 模型狀態統計

3.2 定量分析

可用性定義為系統正常運行的時間和系統運行的時間的比率。圖5 顯示了無分區/雙分區/四分區時系統的可用性與不同的刷新間隔之間的關系。在PRISM 中可以用R{“up_time”}=?[C ＜=T]/T，T=1 month.來做屬性檢測。評估時將刷新間隔定為15 min～4 h。從圖5 中可以看出，當刷新間隔增加時，系統的可用性降低。然而，當刷新間隔相同時，具有更多分區的可用性有著明顯的提高，對于可用性而言，分區數量對于較長的刷新間隔有著比較重要的影響。例如在刷新間隔為4.00 h 的時候，無分區的可用性在0.975 左右，雙分區的可用性在0.985 左右，四分區的可用性則達到了0.99 以上。由于TMR，將面積和功耗至少增加300%，頻繁的刷新將浪費掉很多系統資源。

圖5 無分區/雙分區/四分區的可用性對比

對于這樣的情況，增加分區數量可以提供一個好的解決方案，而不是更頻繁地進行刷新。例如，如果設計人員的目標是高于0.99 的可用性，并設計中沒有考慮分區，那么設計人員可能會考慮用頻繁的刷新來滿足一些要求。這時設計人員可以采用多分區的TMR 來滿足需求，從圖5 中可以看到，當系統四分區時，即使刷新間隔延遲2 h 也可以滿足相同的可用性。使用這種方法，設計者可以確定滿足給定刷新頻率的設計要求的分區數量，反之也同樣可以通過分區數量來確定合適的刷新頻率。

4 結論

本文針對SRAM 型FPGA 的結構特點，將電路分為若干模塊，采用三模冗余和配置刷新相結合的方法對電路的性能進行優化，建立模型并用PRISM 驗證工具進行檢驗。實驗結果表明，該設計可以有效提高電路的可用性。在設計系統時，可以綜合考慮電路結構、資源分配情況來合理地調整分區數量和刷新間隔，靈活組合，以使電路有更佳的性能。