适用于SystemC/C++验证的形式化解决方案

SystemC/C++ 设计的验证要求

虽然 SystemC/C++ 编程风格已使用多年，但最近出现了一些特定使用模式，它们推动工程团队采用共同的设计流程。这包括抽象算法设计代码用作高层次综合 (HLS) 工具的输入，虚拟平台模型用于早期软件测试，可配置的知识产权 (IP) 模块，等等。

HLS 用于将“大部分为非时序化”的抽象 SystemC/C++ 设计表示转换为完全时序化的寄存器传输级 (RTL) 设计模块，该工具已被许多大型半导体和电子系统公司使用。作为一种快速生成具有不同微架构的设计组件，同时快速高效地优化算法处理数据路径的方法， HLS 工具特别受欢迎。其在控制逻辑以及具有更详细时序的一般元器件上的使用，也变得越来越普遍。

图 1. SystemC/C++ 高层次设计流程

SystemC/C++ 设计的验证主要通过如下方式进行：利用 GCC 等标准软件编译器编译设计表示，并以与软件设计类似的方式调试代码。Open SystemC International (OSCI) SystemC C++ 类库（现已标准化为 IEEE 1666-2011）引入了使用户体验更像 RTL 仿真的功能，但仍有许多问题让 SystemC 代码的验证任务非常复杂和艰巨，包括调试、运行时性能和测试复杂性。该级别的形式化技术一直很稀少。

常见 SystemC/C++ HLS 流程所用的算法描述常常仅使用 C 或 C++ 代码。这些描述经过测试，以确保算法本身正确运行。SystemC 类库函数用于提供 HLS 工具所需的极少硬件细节，例如基本时序、复位功能等。综合工具生成 RTL 代码，然后将其应用于更传统的设计细化流程和验证过程。

设计验证分为 SystemC 和 RTL 两个级别。很明显，工程师更愿意验证和调试原始 SystemC 设计，而只在综合后检查功能等效性，类似于传统的 RTL 开发过程。然而，由于缺乏有效的 SystemC/C++ 设计验证环境，工程师们不得不采用更传统的 HDL 验证。

随着工程师提高其设计方法的抽象级别，验证级别自然也要相应地提高。在 HLS 之前的算法级别，要求直接根据其规范验证设计，而较少关注编码细节。功能规范很容易用断言来表示，因此，使用能够针对设计严格测试断言的形式化技术是一种自然的选择。新的控制密集型算法，现在用 SystemC 编写，仅使用仿真特别难以验证。

西门子 EDA 的 360 DV SystemC/C++ 验证功能旨在满足这些要求。

适用于 SystemC/C++ 设计的360 DV 简介

西门子 EDA 是西门子数字化工业软件的一部分，其针对 SystemC/C++ 代码提供的设计验证 (DV) 解决方案是 360 DV 形式化验证产品线的一部分。它支持将广泛的形式化技术应用于以 C++ 或 SystemC 编写的、具有不同时序和代码抽象级别的设计组件。

适用于 SystemC/C++ 的 360 DV-Inspect 提供了一系列自动化结构检查、安全检查和激活检查，可将这些检查应用于设计，而无需手动创建断言。这对于高层次综合之前的设计代码签核特别有用。该产品包含对 SystemC/C++ 设计特别有用的检查，如下所述。

适用于 SystemC/C++ 的 360 DV-Verify 是一款基于断言的形式化验证工具，它功能齐全，支持针对 SystemC/C++ 设计代码测试综合断言。这些断言可以使用简单的 C 断言语句编写，也可以是完整的 SystemVerilog 断言 (SVA)，其中包含所有时间、并发结构体。对 SystemC/C++ 设计运用时间断言的能力是该技术的独特功能。

图 2. SVA 配合 SystemC/C++ 设计使用

作为 360 DV 核心的西门子 EDA 形式化技术平台由多个证明引擎组成，这些引擎利用一系列标准和专有算法来提供深入的代码分析。与其他解决方案相比，它始终表现出高收敛度，另外还提供快速、高容量的操作。该平台可以处理一系列语言，包括支持轻松设置和使用的功能。强大的调试环境为快速跟踪设计或测试问题提供了一条清晰的途径。

西门子 EDA 解决方案以支持形式灵活性而著称，可用来解决一系列问题，而且同样适用于 SystemC/C++ 设计。这些工具可以在高度交互模式下使用，方便用户以“假设分析”的使用方式快速查看设计如何运行。它们可以构成完整的指标驱动验证解决方案的基石，并为 SoC 平台上的 IP 集成提供一种有效的验证机制。

自动形式化 SystemC/C++ 设计评估

360 DV 中的全自动功能也可以应用于 SystemC/C++ 硬件设计代码。在设计过程中尽早消除错误可以节省下游的许多工程设计时间，尤其是设计过程从微架构抽象级别开始时更是如此。

360 DV-Inspect 提供一系列自动化检查，这些检查利用形式化引擎的强大能力对设计代码进行深入的静态分析，而无需手动编写断言。这种设计检查技术基于代码结构分析运行场景，以寻找潜在的错误，因而远远超越了传统的代码检查工具。安全检查（例如越界访问数组或状态机死锁）、激活检查以及结构分析（包括经典的仿真和综合操作失配问题），全都具备。

图 3. SystemC/C++ 代码中的死锁检查

此外，DV-Inspect 提供了一些特别适用于 SystemC 代码的检查。例如，检查哪些寄存器已被显式初始化很重要。SystemC 变量在仿真中会自动初始化，但 HLS 工具会忽略这些初始化。这会导致难以调试的仿真综合失配问题。DV-Inspect 还检查尚未被初始化的寄存器及未定义的操作或多个驱动器能否在设计中传播 X（未知）值。SystemC 仿真中不存在未知值的概念，因此需要进行形式化分析以发现传播问题。 SystemC 还缺乏非阻塞赋值，因此导致了顺序仿真语义与硬件中的并行操作之间出现竞争条件和失配的情况。

DV-Inspect 可以找出许多仿真或 HLS 都不会进行检查的问题，包括特定数据类型问题（例如定点运算） 导致的意外行为，以及与并发相关的问题（例如竞争条件评估）。DV-Inspect 提供有价值的综合前签核，以节省整体开发时间和资源。

图 4. 针对 SystemC/C++ 代码的广泛检查

基于顺序断言的SystemC/C++ 验证

360 DV-Verify 为 SystemC 和其他 SystemC/C++ 设计提供基于断言的完整验证解决方案。该工具接受大多数 SystemC 函数，允许针对一系列代码抽象测试断言，从事务级模型 (TLM) 到详细 RTL，一直到网表，从几乎无时序到周期精准的完整表示。

简单的 ANSI C 断言和全时、并发 SystemVerilog 断言 (SVA)，均可配合 SystemC/C++ 设计使用。这种断言描述的灵活性允许复用其他设计的现有断言，或将其用作模板，以减少与新格式相关的学习开销。它还支持一致的综合前和综合后流程，相同的断言（如果编写时考虑到流程）可以在 SystemC/C++ 业界标准模型及其 RTL 综合后的衍生模型上复用。此外，针对 RTL 环境创建的验证知识产权 (VIP) 断言集，例如总线协议验证器，可以在 SystemC/C++ 代码上复用。

这一独特的能力支持顺序断言，后者可用于描述规范元素、预期的设计特征和要针对抽象代码进行测试的故障条件。这样，工程师便可在 SystemC/C++ 级别处理其业界标准设计，确保设计在综合之前符合规范。它在可针对不同微架构选项实施规范的级别上实现了全面的形式化解决方案。最后，它消除了使用综合后的 RTL 代码调试 SystemC/C++ 设计的间接性。

形式化技术已成为硬件设计功能验证的关键组成部分。为了提高抽象级别并利用高层次综合，许多设计人员已转向 SystemC/C++。这种方法加快了硬件设计过程，但为了相应地减少验证时间，必须把重点放在 SystemC/C++ 源代码上，而不是 HLS 后的 RTL 设计上。适用于 SystemC/C++ 的 360 DV 解决方案满足这一需求，为高级设计提供自动化设计检查和基于断言的全面验证。HLS 用户可以充分利用先进的形式化验证方法，西门子 EDA 解决方案使这一切成为可能。