Vectorization of Verilog Designs and its Effects on Verification and Synthesis
La vectorisation est présentée comme une optimisation de compilateur qui remplace des opérations sur des valeurs scalaires par une opération sur des valeurs vectorielles. Dans l'écosystème Verilog, elle est peu répandue car Verilog ne garantit pas que le signal vectorisé se comporte comme une entité de mot, même si la notation vectorielle est supportée. Toutefois, la vectorisation apporte des bénéfices en réduisant la complexité symbolique, ce qui aide les outils de vérification formelle à raisonner sur des fonctions booléennes et des transitions d'état. L'article présente un vecteuriseur Verilog construit sur l'infrastructure CIRCT, capable d'identifier des motifs de vectorisation tels que les affectations inversées, les expressions complexes et les assignations inter-modules. Des expérimentations avec des outils EDA montrent que pour Jasper, le vecteuriseur améliore le temps d’élaboration de 28,12 % et réduit la consommation mémoire de 51,30 % sur 1 157 conceptions de ChiBench.