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.

翻译：向量化是一种编译器优化技术，它将多个标量值上的操作替换为单个向量值上的操作。尽管在rustc、clang和gcc等传统编译器中较为常见，但向量化在Verilog生态系统中并不普遍。这是因为即使Verilog支持向量表示法，该语言并未提供向量化信号作为字级实体行为的语义保证：综合工具仍将多个单独赋值与单个向量赋值解析为同一组并行线网连接。然而，向量化在其他领域具有重要优势。特别地，即使在底层硬件保持不变的情况下，它也能降低符号复杂性。Cadence Jasper等形式验证工具在符号层面运行：它们推理布尔函数、状态转移和等价类，而非单个线网或门电路。当这些工具能够将总线视为单个符号实体时，其扩展效率更高。本文通过引入Verilog向量化器支持这一观点。该向量化器基于CIRCT编译基础设施构建，能够识别多种向量化模式，包括反向赋值、涉及复杂表达式的赋值以及模块间赋值。通过对部分电子设计自动化（EDA）工具进行实验，在ChiBench集合的1,157个设计上，该技术使Jasper工具的精化时间缩短28.12%，内存消耗降低51.30%。