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:
- An internal representation for Verilog syntax,
- A loader for parsing Verilog source code into this representation,
- Utilities for inspecting, analyzing, and manipulating these designs,
- Various transforms that can simplify these designs, and
- Pretty-printing and other report-generation functions.
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:
- VL can build sv models of Verilog modules for formal
verification with ACL2. This is the basis for much of Centaur's formal
- The VL kit is a standalone command-line program that you can build
on top of ACL2 and VL. It provides some high-level commands that you can use
to do things like lint your design directly from the command line. It also
provides an interactive shell for an instant way to start up ACL2 with VL
- VL has been used to build a web-based ``module browser'' that lets you see
the source code for our modules with, e.g., hyperlinks for navigating between
wires and following wires. This is now integrated into the VL kit; see
- (unreleased) We have used VL to implement samev, a sequential
equivalence checking tool with a tick-based timing model that handles both RTL
and transistor-level constructs.
- (unreleased) We have used it to implement VL-Mangle, a web-based
Verilog refactoring tool. A paper describing this tool can be found in: Jared
ACL Models in End-User Applications. In Do-Form
2013. April, 2013, Exeter, UK.
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
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
code for run-vl-lint-main to see a transformation sequence geared toward
linting. You might also see vl-design->sv-design to see how the new
sv flow works.
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
- Notes about the subset of Verilog and SystemVerilog that vl