一句话：提出 VeriEQ 框架，用等价电路变换生成语义等价的 Verilog 程序，以蜕变测试高效检测仿真器与综合器的行为偏差缺陷。
Verilog 仿真器与综合器对芯片设计至关重要，但流程复杂易引入缺陷，其中行为偏差缺陷（BDB）尤为严重：细微语义偏差即可使芯片偏离设计意图，甚至构成硬件后门。本文提出基于蜕变测试的框架 VeriEQ：分析历史 BDB 的结构模式以设计代码模板提高触发概率；用带位宽与符号性约束的等价电路变换规则生成语义等价变体；并以内联偏差检查机制在单个 testbench 中嵌入多个等价模块提升效率。在四款主流仿真器与综合器上，相比最先进工具加速 138.1%–4161.9%，共发现 33 个未知缺陷（29 个 BDB、4 个挂起），全部确认、27 个已修复，其他工具仅发现 1–7 个。
Verilog simulators and synthesizers play a critical role in chip design and verification. However, due to the complexity of simulation and synthesis processes, they easily introduce various types of bugs. Among them, Behavioral Deviation Bugs (BDBs) are particularly severe, as they can cause incorrect results by introducing subtle semantic deviations that make the chip behave differently from its intended design, potentially enabling hardware backdoors. In this work, we propose VeriEQ, an automated framework based on the idea of metamorphic testing, which detects BDBs by generating semantically equivalent Verilog programs. First, to increase the likelihood of triggering BDB, we analyze the structural patterns of historical BDB and design a Verilog code template. Second, we generate semantically equivalent variants by applying equivalence circuit transformation rules. These rules include constraints on bit-width and signedness to ensure logical consistency before and after the transformation. Finally, we design an inlined deviation checking mechanism that embeds multiple equivalent modules within a single testbench to improve testing efficiency. We implement and evaluate VeriEQ on four mainstream Verilog simulators and synthesizer. Experimental results show that VeriEQ achieves a 138.1% to 4161.9% speedup over state-of-the-art tools. In total, VeriEQ successfully detects 33 previously unknown bugs, including 29 BDBs, along with 4 hang bugs as additional findings. All discovered bugs have been confirmed, with 27 already fixed. In contrast, the other tools are able to detect only 1 to 7 bugs.
@article{paperbot3794,
title = {VeriEQ: Finding Verilog Simulators and Synthesizers Bugs with Equivalence Circuit Transformation},
author = {Zhen Yan and Yuanliang Chen and Fuchen Ma and Zehong Yu and Dalong Shi and Yu Jiang},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {OOPSLA1},
year = {2026},
doi = {10.1145/3798235}
}