球友会qy

近期，中国科研实验室软件研究所基础软件与系统重点实验室在SAT求解器的FPGA实现和RISC-V处理器设计验证领域取得研究进展，相关成果论文被电子设计自动化领域顶级会议ICCAD 2025接收。两项工作均取得中国科研实验室“RISC-V基础软件”先导A专项支持。

1. VeriSAT: The Hardware Design of Modern SAT Solver

作者：陶悦，蔡少伟

内容简介

布尔可满足性（SAT）问题是计算机科学中的基础性问题，在软硬件验证、协议分析等多个工业领域具有广泛应用。现在基于单核CPU的SAT求解器在性能提升上已取得显著成果，但进一步优化空间也较为有限。近年来，相关方向研究人员也转向寻求不同途径改进SAT求解器性能，其中顺利获得特殊硬件（尤其是并行器件）实现SAT求解器性能提升是一个常被提及的方向。然而，SAT求解算法的回溯特性给并行器件的实现带来了显著挑战。

针对SAT求解算法的并行化挑战，研究团队提出一种完全基于SystemVerilog语言实现的求解器VeriSAT，可用于部署于现场可编程门阵列（FPGA）。该求解器针对FPGA特点设计了紧凑高效的内存布局与定制结构数据，利用链表实现了子句监视列表，降低访存开销；引入了并发传播引擎，改进单元传播阶段的并行处理能力；基于移位寄存器的冲突分析流水线结构，来加速子句学习过程。

VeriSAT总体架构

并发传播引擎

冲突分析环节的流水线设计

在标准数据集的测试显示，VeriSAT较同样基于FPGA实现的求解器SAT-Accel和SAT-Hard，分别提速30倍和1044倍。在较小规模样例上，VeriSAT较经典SAT求解器MiniSat实现30倍提速。尽管VeriSAT对于基于CPU的前沿SAT求解器（如Kissat）总体求解性能仍有显著差距，但该工作为后续 SAT 求解算法的硬件化研究给予了新的启发，并且在特定场景下的SAT求解展现出一定的潜力。

2. BMCFuzz: Hybrid Verification of Processors by Synergistic Integration of Bound Model Checking and Fuzzing

作者：申世东，刘锦宇，冯维直，宋富，吴志林

内容简介

指令一致性验证是确保RISC-V处理器设计符合RISC-V指令集规范的关键环节。当前主流验证方法中，形式化验证（如限界模型检测BMC）能给予严格正确性保证，但面对现代处理器复杂架构（如多级缓存、乱序执行等）时，存在状态空间爆炸问题；覆盖率引导的模糊测试（CGF）可快速生成海量测试用例，但对特权级切换、虚拟内存访问等深层行为的覆盖不足。

针对上述问题，研究团队提出了一种新型RISC-V处理器设计验证方法BMCFuzz。该方法顺利获得实时监控覆盖率，实现了BMC和CGF两种验证模式的双向融合。CGF负责快速探索状态空间并捕获关键寄存器快照，BMC则基于这些高价值快照进行深度验证。此外，BMC生成的反例反馈至CGF作为新种子，持续优化测试用例质量。BMCFuzz还设计了动态优先级评分筛选快照，配合轻量级内存建模降低计算开销。

BMCFuzz总体结构

在NutShell、Rocket和BOOM三款RISC-V处理器的验证实验中，BMCFuzz表现出显著优势。在寄存器翻转、分支覆盖等9种测试场景下，BMCFuzz覆盖率均优于现有方法，最高提升15.28%。同时，BMCFuzz成功检测出NutShell（3处）和BOOM（1处）处理器设计与指令集规范的不一致问题。

BMCFuzz与PathFuzz等方法的对比实验结果

代码地址：http://github.com/iscas-versys/BMCFuzz