		Search-engine friendly clone of the ACL2 documentation.

Hardware-verification

Vl2014

The VL Verilog Toolkit, 2014 Edition. This is a "stable" fork of vl for compatibility with esim.

What are VL and VL2014?

The vl Verilog Toolkit is a large ACL2 library for working with Verilog and SystemVerilog source code, developed at Centaur Technology by Jared Davis and Sol Swords.

The 2014 Edition of VL is a "stable" fork of VL that is meant to provide continuing support for older tools, notably including esim, and also including other internal Centaur tools that are based on earlier versions of VL.

The 2014 Edition is not under active development. You should probably not use it for new projects, and it may be best to work toward eventually transitioning older tools away from it, in favor of the "main" version of vl.

Note that you can tell which version of VL you are using as follows.

Main Edition: centaur/vl directory, vl package.
2014 Edition: centaur/vl2014 directory, vl2014 package.

Since each version uses its own package, it is possible to load both versions into the same ACL2 project simultaneously. This may be of use when transitioning code from the 2014 Edition to the main edition.

Why is there a 2014 Edition?

VL has a long history. Its development started in 2008. At that time, our goal was only to implement support for Verilog-2005. Over the next several years, we used VL to implement many tools, many of which were based around esim. ESIM is a purely bit-level backend.

In 2014, we began extending VL with features from SystemVerilog and also began work on a new, vector-level backend, sv. Throughout 2014, and into the start of 2015, we made substantial changes to VL and transitioned our internal projects to SV.

Much of this work was compatible with ESIM and expanded what the VL/ESIM flow could handle. For instance: during this time, the ESIM flow gained better support for ANSI-style ports, SystemVerilog style global parameters, basic SystemVerilog idioms like always_comb and logic data types, and so on. Other certain SystemVerilog features (structs, arrays, etc.) would have been difficult to support in ESIM, so we only added them to the VL/SV flow.

In February 2015, we began working on a substantial change to VL's expression representation. It became apparent that supporting ESIM through this change would require updating a large body of code. This would be a major cost to maintain code that we were no longer using.

In light of this, we decided that it was time to end support for the ESIM flow in VL, but we did not want to abandon ESIM altogether. As a compromise, we decided to create a stable fork of VL, based on the last version of VL that works with ESIM. This fork would allow older tools and proofs to continue to function, while giving us the freedom to move more quickly on the new versions of VL without having to continually update the ESIM flow.

Subtopics

Warnings: Support for handling warnings and errors.
Primitives: The primitive modules targetted by VL.
Use-set: Tool for detecting unused and unset wires.
Syntax: Representation of Verilog structures.
Getting-started: Getting started with VL2014.
Utilities: Generic utilities that are unrelated to Verilog processing, but which are provided by the VL books.
Loader: Finds and loads Verilog source files.
Transforms: High-level transformations for rewriting and simplifying Verilog modules.
Lint: A linting tool for Verilog and SystemVerilog.
Mlib: Module Library -- A collection of various functions for working with Verilog modules.
Server: The VL server powers the Module Browser, a web-based interface for viewing Verilog designs.
Kit: A command-line program for using VL in basic ways.
Printer: Applicative "printer" for building strings.
Esim-vl: Functions for working with E modules produced by VL.
Well-formedness: Sanity checks for the well-formedness of Verilog modules.