基于符号执行的SystemC外设跨层级验证方法对比研究

《IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems》：Comparing Methods for the Cross-Level Verification of SystemC Peripherals with Symbolic Execution

本文针对虚拟原型中SystemC外设验证难题，提出CrosSym和SEFOS两种创新方案。研究通过修改SystemC内核（CrosSym）或优化符号执行引擎（SEFOS），首次实现RTL与TLM层级的跨平台验证。实验表明，两种工具在保持与现有技术相当性能的同时，成功检测出300多个变异体，为复杂硬件设计提供了更全面的验证手段。

　　

在现代硬件设计领域，随着集成电路复杂度的指数级增长，设计错误的早期发现变得至关重要。虚拟原型（Virtual Prototypes, VPs）作为高层次硬件模型，允许开发者在硅片制造前就开始软件开发和系统验证，显著降低了后期修改的成本。SystemC作为业界标准的建模语言，支持从事务级（Transaction Level Modelling, TLM）到寄存器传输级（Register Transfer Level, RTL）的多层次抽象描述，为早期验证提供了理想平台。然而，这种灵活性也带来了新的挑战——如何确保不同抽象层级模型之间的一致性？

传统的仿真测试方法只能覆盖有限的状态空间，而形式化验证技术虽然能提供更全面的保证，但往往需要复杂的模型转换。符号执行（Symbolic Execution）作为从软件领域引入的技术，通过用符号变量代替具体值，能够系统性地探索程序的执行路径，成为解决这一难题的有力工具。但在SystemC环境下，其独特的线程调度机制和通信接口给符号执行带来了三大障碍：系统线程实现的SC_THREAD、基于互斥锁的信号端口机制，以及大型类对象导致的求解器性能瓶颈。

针对这些挑战，研究人员在《IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems》上发表了创新性研究成果，提出了两种截然不同的解决方案。CrosSym采用修改SystemC内核的策略，通过实现轻量级替代内核支持符号执行；而SEFOS则反其道而行，通过扩展KLEE符号执行引擎来适配原生SystemC内核。这两种方案共同构建了首个支持SystemC外设跨层级验证的完整框架。

研究团队采用了系统化的验证方法学，建立了包含测试基准生成、LLVM中间表示编译、符号执行引擎集成的完整流程。该流程支持三种验证场景：TLM外设独立验证、RTL外设独立验证以及RTL≤TLM跨层级等价验证。针对外设验证的特殊性，团队还提出了通信接口与功能逻辑分离验证的策略，有效避免了接口交互带来的状态空间爆炸问题。

在技术实现方面，CrosSym的核心贡献在于设计了支持TLM和RTL特性的替代内核。该内核改进了现有方案的事件通知机制，实现了完整的信号端口通信和时钟同步功能。特别是对SC_THREAD的代码转换技术，使得线程控制流无需系统线程切换即可正确执行。SEFOS则深入分析了SystemC的协程式多任务机制，通过拦截PThread相关系统调用，在符号执行引擎内部模拟线程调度行为。其创新的数组最小化技术（Array Minimization）通过动态裁剪对象数组中无关元素，显著降低了SMT求解器的查询负担。

验证结果分析显示，两种工具在四类典型外设（PLIC中断控制器、GCD计算模块、哈希模块和映射模块）上均表现出色。在RTL PLIC验证中，工具成功发现了优先级阈值比较逻辑错误（E1）和超限优先级处理不一致（E2）两个关键缺陷。跨层级验证场景下，虽然求解复杂度显著增加，但仍在合理时间内完成了大部分状态的探索。

在性能对比方面，研究揭示了有趣的发现。对于简单外设（如映射模块），两种工具均能在15分钟内完成全状态探索；而对于包含复杂循环结构的外设（如GCD模块），符号执行时间可能超过24小时。SEFOS凭借数组最小化技术，在TLM PLIC案例中将超时测试用例从5个减少到2个，证明了该优化的有效性。与现有技术SymSysC相比，CrosSym在时间开销增加不超过10%的情况下，支持了更丰富的RTL特性；SEFOS则在保持原生SystemC兼容性的同时，实现了更具竞争力的性能。

变异测试评估进一步验证了工具的缺陷检测能力。通过对300多个故意注入的变异体进行测试，两种工具在15分钟内成功识别了大部分功能异常。特别值得注意的是，在某些场景下，跨层级验证相比独立验证能更快发现缺陷，这揭示了不同验证策略之间存在复杂的互补关系。

然而，研究也暴露了符号执行技术的固有局限性。面对S2C基准测试中的复杂模块，两种工具都出现了内存耗尽或超时的情况，这表明在处理大规模设计时仍需进一步优化。状态空间爆炸和复杂符号表达式求解仍然是制约实用化的主要瓶颈。

该研究的创新价值在于首次系统性地解决了SystemC外设跨层级验证的完整技术链。CrosSym和SEFOS不仅提供了实际可用的开源工具，更重要的是展示了两种技术路线的优缺点和适用场景。对于注重验证效率的场景，CrosSym的轻量级内核是更优选择；而对于需要保持设计原型的场景，SEFOS的无侵入验证更具优势。

这项工作的理论意义在于深化了对硬件描述语言符号执行本质的理解。通过具体分析SystemC的线程模型和对象机制，研究为其他类似语言的验证提供了重要参考。实践上，工具已成功应用于实际外设验证，为工业界提供了一套可靠的验证解决方案。

未来研究方向包括针对无限循环的摘要技术、路径相似性优化以及面向SystemC的特化搜索策略等。随着这些技术的成熟，符号执行有望成为虚拟原型验证的标准手段，最终推动整个硬件设计流程的自动化和可靠化发展。