Unveiling Cross-checking Opportunities in Verilog Compilers

技术方案与技术路线详解

Verilog作为硬件描述语言（HDL），其工具链（如综合器Yosys、仿真器Verilator）的可靠性直接影响芯片设计的正确性。然而，工具链的复杂性、优化算法的多样性以及语言规范的多版本兼容性问题，导致编译器错误频发。传统测试方法（如随机测试、形式化验证）虽有效，但存在以下不足：

VeriXmith的核心思想是通过跨工具交叉检查（Cross-checking）验证语义一致性，其技术方案分为三个关键模块：

工具集成：
- 变异器实现：基于tree-sitter-verilog解析AST，确保变异语法正确。
- 编译工具适配：支持Yosys（综合）、Verilator（仿真）、sv2v（SystemVerilog转Verilog）等工具的输出格式兼容。
性能优化：
- 符号执行超时控制：单周期仿真限时1000秒，避免路径爆炸。
- 失败去重：基于错误消息和堆栈跟踪聚类，减少人工排查量。

有效性验证：
- 发现31个未知错误：涵盖编译器崩溃（9例）、错误编译（14例）、规范不符（7例）、库缺陷（1例）。
- 典型错误示例：
  - Yosys解析器缺陷：无法处理转义标识符（如\a[1]）。
  - Verilator优化错误：幂运算符（**）引发内部错误。
  - PySMT库逻辑错误：误实现按位异或非（BVXnor）。
扩展性验证：
- 输入源对比：GitHub真实代码触发最多错误（图4），因覆盖更广语言特性。
- 空间贡献分析：变异和编译空间扩大错误发现概率（图3）。

创新：
- 首个体化的Verilog工具链交叉检查框架，整合生成、编译、验证工具。
- 语义感知变异提升测试输入有效性，优于传统随机生成。
局限：
- 组合等价性假设：要求状态严格对齐，不适用于激进优化（如状态编码）。
- 非确定性处理：部分测试输入含不确定逻辑值（X值），需手动过滤。

VeriXmith通过变异生成-多工具编译-形式化验证的技术路线，系统化提升了Verilog工具链的可靠性。未来可扩展至：

该框架为硬件编译生态的持续可靠性工程提供了参考架构，具有重要工业价值。

以下是VeriXmith框架中跨工具交互的一个具体示例，展示了如何通过多工具协同验证发现潜在错误：

module top(input clk, input [2:0] i, output reg [2:0] o);
  always @(posedge clk)
    o <= ((3'h6) & (~i)) ? 3'h0 : i;
endmodule

此模块的功能是：在每个时钟上升沿，若 (3'h6 & ~i) 为真，则输出 o 置零，否则输出 i。

变异阶段
VeriXmith通过MakeArray变异操作符，可能将i转换为多维数组，生成新的测试输入。
编译阶段
- 路径1（Yosys综合）：
  1
  yosys -p "synth; write_smt2 output.smt2" input.v
  Yosys将Verilog转换为SMTLIB格式，但在处理表达式((3'h6) & (~i))时错误地引入了一个自由变量（应为常量0），导致SMT公式存在不确定性。
- 路径2（Verilator仿真）：
  1
  verilator -O3 --cc input.v --exe sim_main.cpp
  Verilator将Verilog编译为C++仿真代码。符号执行工具KLEE对C++代码进行单周期分析，正确推导出((3'h6) & (~i))恒为0，因此o始终等于i。
等价性检查
- SMT求解器（如Z3）对比两者的SMT公式：
  - Yosys生成的公式允许((3'h6) & (~i))为0或1（错误）。
  - KLEE生成的公式约束((3'h6) & (~i))必须为0（正确）。
- 检查结果：发现语义不一致，触发非等价（Non-equivalence）错误。

根本原因：Yosys在处理按位与运算符时未正确优化常量表达式，错误地保留了自由变量。
跨工具价值：
- 单一工具测试无法发现：若仅测试Yosys的综合结果，可能因缺乏参照而忽略错误。
- 工具协同验证：通过Verilator生成的C++仿真代码作为“黄金参考”，暴露了Yosys的逻辑错误。

sv2v与Verilog兼容性错误
- 输入：SystemVerilog的output reg [15:0] r声明。
- sv2v转换：错误地生成Verilog的output reg [15:0] r（Verilog不允许output reg）。
- Icarus Verilog验证：后续工具（如Icarus）在解析转换后的Verilog时报错，触发合规性错误（Compliance Bug）。
Verilator优化选项崩溃
- 输入：包含幂运算符**的代码。
- Verilator -O3优化：内部断言失败导致崩溃。
- KLEE符号执行路径：未生成有效输出，触发意外终止（Unexpected Termination）错误。