Vectorization of Verilog Designs and its Effects on Verification and Synthesis

TL;DR

This paper introduces a Verilog vectorizer built on CIRCT that recognizes various vectorization patterns, improving formal verification scalability by reducing elaboration time and memory usage.

Contribution

It presents a novel Verilog vectorizer that enhances verification and synthesis processes by treating buses as single symbolic entities.

Findings

Improves Jasper verification tool elaboration time by 28.12%.

Reduces memory consumption in Jasper by 51.30%.

Effective on 1,157 designs from ChiBench collection.

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.