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 存储空间的数据保护功能。 此外，断言验证方法不仅保证了功能验证的完备性，还缩短了产品开发周期。