An introduction to VL, with suggested starting points for how to get started with evaluating it for use in your own projects.
VL is an ACL2 library for working with SystemVerilog (and also regular Verilog) source code, developed at Centaur Technology by Jared Davis and Sol Swords. At a high level, VL includes:
Much of VL is general purpose Verilog processing code that is independent of particular analysis or back-end tool. This approach has allowed us to use VL to implement a family of Verilog-related tools. Here are some examples:
We imagine that parts of VL may be useful for implementing other SystemVerilog processing tools.
The first step in using VL for anything is probably to try to get it to parse your design; see the documentation for the loader. You may want to read the notes about supported-constructs.
Once you have parsed your design (or at least some portion of it) you will have a list of modules. You might want to at least glance through the documentation for syntax, which explains how modules are represented. This may be particularly useful if you are going to write your own analysis tools.
You may find it useful to pretty-print modules, see for instance vl-ppcs-module and perhaps more generally the VL printer.
After getting a feel for how modules are represented, it would be good to
look at the available transforms. For instance, you might look at the
If you are going to write any Verilog-processing tools of your own, you should probably read through how VL deals with warnings and then take a look at mlib, which provides many functions for working with expressions and ranges, finding modules and module items, working with the module hierarchy, generating fresh names, and working with modules at the bit level.