Automatic Synthesizability Checking of Hardware Descriptions

Automatic Synthesizability Checking of Hardware Descriptions

Shevtsov A.A. (MSU, Moscow, Russia; ISP RAS, Moscow, Russia)
Churkin Y.A. (ISP RAS, Moscow, Russia)
Buchatskiy R.A. (ISP RAS, Moscow, Russia)
Kamkin A.S. (MSU, Moscow, Russia; ISP RAS, Moscow, Russia)
Melnik D.M. (ISP RAS, Moscow, Russia)

Abstract

Modern VLSI design flows use the Verilog and SystemVerilog hardware description languages for both logic synthesis and simulation. However, not every language construct is synthesizable, the sets of supported constructs differ across synthesis tools, and the tools do not always diagnose non-synthesizable constructs: a construct may be silently dropped or reinterpreted, causing a mismatch between the behavior of the RTL model and the synthesized netlist. Problems discovered late in the design flow require corrections at every stage and incur significant time and financial costs, which motivates automated synthesizability checking of RTL descriptions. This paper presents a set of 34 synthesizability rules for Verilog and SystemVerilog hardware descriptions formulated on the basis of the IEEE/IEC 62142-2005 standard, the STARC RTL Design Style Guide, and the Reuse Methodology Manual, as well as the experience of commercial tools. The rules cover constructs not used in synthesis, the semantics of hardware element descriptions, and synthesis–simulation divergence. Static checkers verifying source code against these rules were implemented within the SVAN static analysis system: ten new checkers were developed (SYNTH14–SYNTH23), one existing checker was updated (SYNTH13), and further rules are covered by previously implemented SVAN checkers. A configurable conservativeness mechanism is proposed that adapts checker strictness to the capabilities of a particular synthesis tool, including the use of data-flow analysis; recommended checker configurations were derived for the Yosys, Vivado, and Genus synthesis tools. An evaluation using the open-source Yosys synthesis tool confirmed that non-synthesizable constructs can be processed silently with altered semantics, demonstrating the practical value of early static checking. A comparison with the commercial SpyGlass analyzer revealed specific gaps in its analysis, and rule violations were found in all ten open-source projects the checkers were applied to; one of the violations was reported to the developers of the OpenC910 project.

Keywords

static analysis; synthesizability; logic synthesis; SystemVerilog; Verilog; hardware description language; RTL; VLSI; EDA; Yosys.

Edition

Proceedings of the Institute for System Programming, vol. 38, issue 4, part 2, 2026, pp. 45-66

ISSN 2220-6426 (Online), ISSN 2079-8156 (Print).

DOI: 10.15514/ISPRAS-2026-38(4)-18

For citation

Shevtsov A.A., Churkin Y.A., Buchatskiy R.A., Kamkin A.S., Melnik D.M. Automatic Synthesizability Checking of Hardware Descriptions. Proceedings of the Institute for System Programming, vol. 38, issue 4, part 2, 2026, pp. 45-66 DOI: 10.15514/ISPRAS-2026-38(4)-18.

Full text of the paper in pdf Back to the contents of the volume