Vectorization of Verilog Designs and its Effects on Verification and Synthesis
Recorded: March 22, 2026, 10 p.m.
| Original | Summarized |
[2603.17099] Vectorization of Verilog Designs and its Effects on Verification and Synthesis
Skip to main content Learn about arXiv becoming an independent nonprofit. We gratefully acknowledge support from the Simons Foundation, member institutions, and all contributors. > cs > arXiv:2603.17099 Help | Advanced Search All fields Search open search GO open navigation menu quick links Login Computer Science > Programming Languages arXiv:2603.17099 (cs) [Submitted on 17 Mar 2026] 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. Subjects: Programming Languages (cs.PL); Hardware Architecture (cs.AR) ACM classes: Report number: Cite as: Focus to learn more arXiv-issued DOI via DataCite (pending registration) Submission history From: Fernando Quintao Pereira [view email] [v1]
Full-text links: 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 authorsView PDFHTML (experimental)TeX Source view license < prev | new Change to browse by: References & Citations NASA ADSGoogle Scholar export BibTeX citation BibTeX formatted citation loading... Data provided by: Bookmark
Bibliographic Tools Bibliographic and Citation Tools Bibliographic Explorer Toggle Bibliographic Explorer (What is the Explorer?) Connected Papers Toggle Connected Papers (What is Connected Papers?) Litmaps Toggle Litmaps (What is Litmaps?) scite.ai Toggle scite Smart Citations (What are Smart Citations?) Code, Data, Media Code, Data and Media Associated with this Article alphaXiv Toggle alphaXiv (What is alphaXiv?) Links to Code Toggle CatalyzeX Code Finder for Papers (What is CatalyzeX?) DagsHub Toggle DagsHub (What is DagsHub?) GotitPub Toggle Gotit.pub (What is GotitPub?) Huggingface Toggle Hugging Face (What is Huggingface?) Links to Code Toggle Papers with Code (What is Papers with Code?) ScienceCast Toggle ScienceCast (What is ScienceCast?) Demos Demos Replicate Toggle Replicate (What is Replicate?) Spaces Toggle Hugging Face Spaces (What is Spaces?) Spaces Toggle TXYZ.AI (What is TXYZ.AI?) Related Papers Recommenders and Search Tools Link to Influence Flower Influence Flower (What are Influence Flowers?) Core recommender toggle CORE Recommender (What is CORE?) Author About arXivLabs arXivLabs: experimental projects with community collaborators Which authors of this paper are endorsers? | About contact arXivClick here to contact arXiv subscribe to arXiv mailingsClick here to subscribe Copyright Web Accessibility Assistance arXiv Operational Status |
This research paper, authored by Oiveira Guimarães, Rosa, Trudel, Amorim Vieira, Mafra, Crepalde, and Pereira, investigates the application of vectorization techniques to Verilog designs and its resultant effects on verification and synthesis processes. The core argument centers around the existing limitations of Verilog’s native support for vector operations, despite their prevalence in other compilers like rustc, clang, and gcc. The paper posits that Verilog’s handling of vector notation lacks the semantic guarantees necessary for true vector-level optimization, leading to inefficiencies in synthesis tools. Essentially, the authors demonstrate that even when Verilog supports vector notation, synthesis tools still resolve multiple assignments to individual parallel wire connections, negating the potential benefits of vectorization. The key contribution of the work is the introduction of a Verilog vectorizer, built upon the CIRCT compilation infrastructure. This vectorizer identifies and exploits several key vectorization patterns within Verilog code, including inverted assignments, complex expressions, and inter-module assignments. The performance of this vectorizer was evaluated through experimentation with Electronic Design Automation (EDA) tools, specifically Cadence Jasper. The results, presented on 1,157 designs from the ChiBench collection, showed a significant improvement: a 28.12% reduction in elaboration time and a 51.30% decrease in memory consumption. These findings stem from the vectorizer’s ability to treat bus signals as single, symbolic entities, mirroring the approach used in formal verification tools like Jasper, which operate at a symbolic level rather than analyzing individual wires and gates. The efficiency gains are attributed to the reduced symbolic complexity associated with treating bus signals as single, unified entities. The paper details four algorithms and four theorems supporting these results. The research is published under arXiv:2603.17099 and categorized within the Programming Languages (cs.PL) and Hardware Architecture (cs.AR) fields, with MSC class 68N20 and ACM classes D.3.4. |