Paper
Vectorization of Verilog Designs and its Effects on Verification and Synthesis
Authors
Maria Fernanda Oiveira Guimarães, Ulisses Rosa, Ian Trudel, João Victor Amorim Vieira, Augusto Amaral Mafra, Mirlaine Crepalde, Fernando Magno Quintão Pereira
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.
Metadata
Related papers
Fractal universe and quantum gravity made simple
Fabio Briscese, Gianluca Calcagni • 2026-03-25
POLY-SIM: Polyglot Speaker Identification with Missing Modality Grand Challenge 2026 Evaluation Plan
Marta Moscati, Muhammad Saad Saeed, Marina Zanoni, Mubashir Noman, Rohan Kuma... • 2026-03-25
LensWalk: Agentic Video Understanding by Planning How You See in Videos
Keliang Li, Yansong Li, Hongze Shen, Mengdi Liu, Hong Chang, Shiguang Shan • 2026-03-25
Orientation Reconstruction of Proteins using Coulomb Explosions
Tomas André, Alfredo Bellisario, Nicusor Timneanu, Carl Caleman • 2026-03-25
The role of spatial context and multitask learning in the detection of organic and conventional farming systems based on Sentinel-2 time series
Jan Hemmerling, Marcel Schwieder, Philippe Rufin, Leon-Friedrich Thomas, Mire... • 2026-03-25
Raw Data (Debug)
{
"raw_xml": "<entry>\n <id>http://arxiv.org/abs/2603.17099v1</id>\n <title>Vectorization of Verilog Designs and its Effects on Verification and Synthesis</title>\n <updated>2026-03-17T19:39:56Z</updated>\n <link href='https://arxiv.org/abs/2603.17099v1' rel='alternate' type='text/html'/>\n <link href='https://arxiv.org/pdf/2603.17099v1' rel='related' title='pdf' type='application/pdf'/>\n <summary>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.</summary>\n <category scheme='http://arxiv.org/schemas/atom' term='cs.PL'/>\n <category scheme='http://arxiv.org/schemas/atom' term='cs.AR'/>\n <published>2026-03-17T19:39:56Z</published>\n <arxiv:comment>12 pages, 16 figures, 4 algorithms, 4 theorems</arxiv:comment>\n <arxiv:primary_category term='cs.PL'/>\n <author>\n <name>Maria Fernanda Oiveira Guimarães</name>\n </author>\n <author>\n <name>Ulisses Rosa</name>\n </author>\n <author>\n <name>Ian Trudel</name>\n </author>\n <author>\n <name>João Victor Amorim Vieira</name>\n </author>\n <author>\n <name>Augusto Amaral Mafra</name>\n </author>\n <author>\n <name>Mirlaine Crepalde</name>\n </author>\n <author>\n <name>Fernando Magno Quintão Pereira</name>\n </author>\n </entry>"
}