Verilog设计的向量化及其对验证和综合的影响
Vectorization of Verilog Designs and its Effects on Verification and Synthesis

原始链接: https://arxiv.org/abs/2603.17099

本文介绍了一种基于 CIRCT 基础设施的新型 Verilog 向量化器,解决了 Verilog 语言中缺乏 Rust 和 C++ 等语言中常见的向量化技术的问题。虽然 Verilog 支持向量表示法,但传统工具通常将向量视为单个信号,从而阻碍了优化。 作者证明,将向量视为单个符号实体——特别是对于 Cadence Jasper 等形式验证工具而言——可以显著提高性能。他们的向量化器识别用于优化的常见模式,包括复杂的赋值和模块间连接。 使用 ChiBench 集合进行的实验表明,Jasper 获得了显著改进:**阐明时间减少了 28.12%**,**内存消耗减少了 51.30%**。这突出了向量化在降低符号复杂度和增强 Verilog 设计中验证流程的可扩展性方面的潜力,即使在不改变底层硬件的情况下也是如此。

对不起。
相关文章

原文

[Submitted on 17 Mar 2026]

View a PDF of the paper titled Vectorization of Verilog Designs and its Effects on Verification and Synthesis, by Maria Fernanda Oiveira Guimar\~aes and 5 other authors

View PDF HTML (experimental)
Abstract:Vectorization is a compiler optimization that replaces multiple operations on scalar values with a single operation on vector values. Although common in traditional compilers such as rustc, clang, and gcc, vectorization is not common in the Verilog ecosystem. This happens because, even though Verilog supports vector notation, the language provides no semantic guarantee that a vectorized signal behaves as a word-level entity: synthesis tools still resolve multiple individual assignments and a single vector assignment into the same set of parallel wire connections. However, vectorization brings important benefits in other domains. In particular, it reduces symbolic complexity even when the underlying hardware remains unchanged. Formal verification tools such as Cadence Jasper operates at the symbolic level: they reason about Boolean functions, state transitions, and equivalence classes, rather than about individual wires or gates. When these tools can treat a bus as a single symbolic entity, they scale more efficiently. This paper supports this observation by introducing a Verilog vectorizer. The vectorizer, built on top of the CIRCT compilation infrastructure, recognizes several vectorization patterns, including inverted assignments, assignments involving complex expressions, and inter-module assignments. It has been experimented with some Electronic design automation (EDA) tools, and for Jasper tool, it improves elaboration time by 28.12% and reduces memory consumption by 51.30% on 1,157 designs from the ChiBench collection.
From: Fernando Quintao Pereira [view email]
[v1] Tue, 17 Mar 2026 19:39:56 UTC (1,067 KB)
联系我们 contact @ memedata.com