Unveiling Cross-checking Opportunities in Verilog Compilers
Yike Zhou, Yanyan Jiang, Jian Lu · ACM Transactions on Design Automation of Electronic Systems · 2025
The landscape of Verilog toolchains for electronic design automation (EDA) is diverse, and their reliability is crucial, as errors can lead to significant debugging challenges and delays in development. Methodologies such as testing and formal verification have been applied to identify and eliminate defects in these toolchains. We propose a framework named VeriXmith to interconnect design tools involved in logical synthesis and simulation for cross-checking. These tools process circuit designs and produce outputs in different languages, such as Verilog netlists from synthesizers and C++ programs from simulators. Since these outputs represent the same circuit semantics, we can leverage this semantic consistency to verify the tools that translate one representation into another. Our approach involves creating semantics extractors to extend the range of circuit representations available for semantic equivalence checking by converting them into a canonical and comparable form. Additionally, we develop mutation operators for Verilog designs to introduce new data/control paths and language constructs, enhancing the diversity of circuit designs as test inputs. By validating semantic equivalence, our framework successfully identifies defects in existing Verilog toolchains. An exploratory experiment uncovers 31 previously unknown bugs in well-known open-source Verilog tools, including Verilator and Yosys.