DSP 中存儲保護單元的設計與斷言驗證

肖海鵬， 謝海情， 汪 東

（1 長沙理工大學 物理與電子科學學院， 長沙410005； 2 湖南轂梁微電子有限公司， 長沙410005）

0 引 言

數字信號處理器（Digital Signal Processor，DSP）廣泛應用于雷達、聲納、數字通信以及語音視頻信號處理［1］。 為保證DSP 能夠正常有序工作，防止某些非法訪問或操作破壞DSP 的存儲空間，需在DSP 中加入存儲保護功能［2-3］。

存儲空間的數據保護方法有兩種：軟件保護和硬件保護。 軟件保護是DSP 中沒有集成硬件模塊或有硬件模塊但不使用，只依靠軟件來保護存儲空間，但軟件保護嚴重影響DSP 的處理速度；硬件保護是DSP 中集成有專門檢測和限制對存儲空間訪問的硬件，訪問請求需要按照其屬性接受存儲保護單元的檢測，一旦用戶訪問存儲保護區域但不具有訪問權限則產生指令預取中止和數據訪問中止。

功能驗證是數字集成電路設計中至關重要的環節，主要有模擬仿真驗證和形式化驗證兩種［4-6］。隨著芯片規模和復雜度的增加，模擬仿真驗證存在測試向量完備性差的缺點。 而形式化驗證基于嚴格的數學模型和嚴密的推理與證明，遍歷待測設計的整個狀態空間，具有很好的完備性［7］。 其中，斷言驗證是用于性質（屬性）檢驗的一種常用的形式化驗證［8-10］。

為了實現訪問請求的屬性檢查，本文設計一個存儲保護單元，通過檢查訪問請求是否取自于存儲保護區域，請求訪問的目的地址是否屬于存儲保護區域以及存儲空間是否受到CSM（Code Secure Model）保護三方面的信息，來決定是否允許用戶訪問存儲保護區域，實現存儲空間的數據保護功能。 另外，為保證功能驗證的完備性，采用斷言驗證完成存儲保護單元的功能驗證，并在X-DSP 全芯片環境下采用FPGA 原型驗證，完成存儲保護單元的功能測試。

1 存儲保護單元設計

本文設計的X-DSP 存儲保護單元功能框圖如圖1 所示，主要包括：代碼安全模塊CSM、Memory Controller 模塊以及CPU_Core 模塊。 代碼安全模塊CSM 實現從片上Flash 讀取密碼并作全0、全1 判斷以及與密匙寄存器進行密碼匹配，輸出結果CSM，其值為1 時，X-DSP 受CSM 保護，反之，則未受CSM 保護。 Memory Controller 模塊實現安全屬性檢查，輸出安全屬性標簽給CPU_Core 模塊。 CPU_Core 模塊實現相應的CPU 功能以及安全屬性檢查，以檢查結果決定是否允許用戶訪問存儲保護區域，用安全屬性標簽來決定是否產生指令預取中止和數據訪問中止。

圖1 存儲保護單元功能框圖Fig. 1 The formal structure diagram of memory protection unit

其工作原理：存儲保護單元檢查三方面的信息：（1）存儲空間是否受CSM 保護。 （2）訪問目的地址是存儲保護區域還是非保護區域。 （3）請求本身屬性是安全還是不安全，即產生請求的指令是取自于保護區域還是非保護區域。 如果請求本身是安全的，訪問目的地址位于存儲保護區域，則放行；如果請求本身是不安全的，但訪問目的地址位于存儲保護區域，則阻止；而對非保護區域的訪問請求則不做檢查。

此外，在調試仿真器連接X-DSP 時，如果CSM為0，對調試軟件的請求、訪存地址是非保護區域以及取指請求不做檢查。 如果CSM 為1 時，調試軟件通過JTAG 方式訪問存儲空間被阻止， 產生Disconnect 的命令脈沖送給調試軟件并斷開仿真器連接。

2 存儲保護單元的斷言驗證

2.1 驗證平臺

存儲保護單元的斷言驗證流程如圖2 所示。 其中，形式屬性驗證工具FPV App 完成存儲保護單元的斷言驗證，驗證所編寫的功能屬性在存儲保護單元的RTL（Register Translation Level，RTL）代碼設計中已實現了屬性所描述的功能。

圖2 存儲保護單元的斷言驗證流程Fig. 2 Assertion-based verification flow of memory protection unit

2.2 功能屬性

編寫存儲保護單元功能屬性并斷言，驗證以下功能屬性點：（1）檢查請求訪問目的地址是否屬于存儲保護區域，輸出安全屬性標簽。 （2）當請求是由存儲保護區域發出，并且訪問目的地址是存儲保護區域，則放行。 （3）當請求不是存儲保護區域發出，但訪問目的地址是存儲保護區域，CSM 為1 時，阻止，CSM 為0 時，放行。 （4）訪問目的地址不是存儲保護區域時，則不做任何檢查。 （5） Memory Controller 根據CSM 和安全屬性標簽控制片選信號的輸出，即是否允許用戶訪問存儲保護區域。 （6）根據安全屬性標簽與CSM 來控制調試仿真器的訪問請求。 屬性建立步驟如圖3 所示。

圖3 屬性的建立步驟Fig. 3 The building flow of the property

采用System Verilog Assertions 屬性描述語言編寫存儲保護單元的功能屬性并斷言，如例1 所示。

例1：property one；

pwl_key_true ｜-＞！ CSM.CSM ＆＆ ！ CSM.ECSL；

endproperty

assert_one： assert property （one）；

cover_one： cover property （one）；

例1 中，屬性one 根據代碼安全模塊的PWL 密碼與密匙寄存器值匹配成功信號pwl_key_true 為1時，在當前時鐘周期內檢查CSM 信號與ECSL 信號是否為0（CSM 與ECSL 初始值為1）。

2.3 驗證結果與分析

編寫腳本運行FPV 工具，工具自動遍歷存儲保護單元的所有狀態空間，驗證所編寫的功能屬性是否正確以及功能是否實現。 存儲保護單元的斷言驗證結果如圖4 所示。 結果顯示，所編寫的功能屬性有42 條，均被驗證通過，并且編寫的功能屬性描述正確且在RTL 代碼設計中已實現屬性所描述的功能。

3 FPGA 原型驗證

FPGA 原型驗證測試平臺如圖5 所示，將XDSP 全芯片代碼映射至FPGA，采用TI CCS 調試軟件作為測試工具，使用XDS 仿真器與FPGA 相連，通過CCS 軟件調試操作來驗證存儲保護單元的物理實現。

FPGA 原型驗證結果如下：X-DSP 上電復位，編寫測試程序寫入存儲空間，當CSM 為0 時，存儲空間未受到保護，單步執行測試程序，其結果如圖6 所示，程序運行成功，存儲空間數據可以正常訪問。 在圖7 中。 通過CCS 調試軟件的program 操作設置密碼后，CSM 變為1，存儲空間受CSM 保護。 這時，重新單步執行測試程序，JTAG 訪問請求被阻止，產生了Disconnect 的命令脈沖送給調試軟件，致使調試仿真器斷開連接。

圖4 存儲保護單元的斷言驗證結果Fig. 4 The result of memory protection unit assertion -based verification

圖5 FPGA 原型驗證測平臺Fig. 5 The testing platform of FPGA prototype verification

圖6 CSM＝0 時程序運行結果Fig. 6 The program running result of CSM＝0

圖7 CSM＝1 時程序運行結果Fig. 7 The program running result of CSM＝1

從圖6、7 可知，在X-DSP 存儲空間處于保護狀態（CSM＝1）和非保護狀態（CSM ＝0）兩種情況下完成了存儲保護單元的功能測試。 表明存儲保護單元實現了X-DSP 存儲空間的數據保護功能，阻止不具有訪問權限的用戶訪問存儲保護區域，同時產生指令預取中止和數據訪問中止，并斷開仿真器連接。

4 結束語

本文針對X-DSP 存儲空間的訪問安全問題，基于硬件保護方法完成了存儲保護單元的RTL 代碼設計，并采用System Verilog Assertions 編寫存儲保護單元的功能屬性描述，用斷言驗證方法完成了存儲保護單元的功能驗證。 同時，在X-DSP 芯片驗證環境下采用FPGA 原型驗證，完成了存儲保護單元的功能測試。 結果表明，所設計的存儲保護單元實現了X-DSP 存儲空間的數據保護功能。 此外，斷言驗證方法不僅保證了功能驗證的完備性，還縮短了產品開發周期。