		Search-engine friendly clone of the ACL2 documentation.

Vl2014

Getting-started

Getting started with VL2014.

Introduction

VL2014 (hereafter VL) is an ACL2::ACL2 library for working with Verilog and SystemVerilog source code. It includes:

An internal representation for Verilog syntax,
A loader for parsing Verilog source code into this representation,
Utilities for inspecting and analyzing parsed 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 esim models of Verilog modules for formal verification with ACL2. This is the basis for much of Centaur's formal verification efforts.
The VL kit is a standalone command-line executable that you can build on top of ACL2 and VL. It includes commands for linting Verilog designs, converting Verilog modules into a JSON format, and other commands.
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; server.
(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 Davis. Embedding ACL Models in End-User Applications. In Do-Form 2013. April, 2013, Exeter, UK.

We imagine that other users of VL may wish to reuse its parsing and transformations to easily implement other tools.

Starting Points

If you want to use VL to do formal verification of hardware, you might start with the ACL2::esim-tutorial, which is a hands-on guide that will take you through using VL and esim to verify some simple circuits.

The first step in using VL in any other capacity on a real project 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 code for vl-simplify to see the transforms used in the esim flow. You could also look at run-vl-lint-main which uses a different transformation sequence for toward linting.

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.

Subtopics

Supported-constructs: Notes about the subset of Verilog and SystemVerilog that vl2014 supports.