		Search-engine friendly clone of the ACL2 documentation.

Note-7-1-books

Note-7-1-vl

Notes about changes to vl and esim in ACL2 Version 7.1.

VL Fork

There have been many changes to vl and esim. Most notably, VL has been forked into two versions.

vl2014 is a ``stable'' fork of VL.: It lives in a new directory: books/centaur/vl2014; It uses the VL2014 package.; It continues to work with esim and other, older tools.; It is no longer under active development by Centaur.
vl continues as the ``development'' version of VL.: It continues to live in: books/centaur/vl.; It continues to use the VL package.; It no longer supports esim.; It remains under active development.; It targets a new backend (instead of esim) which is still under development.; It may be rather unstable and not yet particularly usable.

The new vl code base is in many cases significantly different than vl2014. It features a new, more strongly typed expression representation, generally better abstractions for working with scopes/hierarchy and types, and new approaches to elaboration and sizing that can handle much more of SystemVerilog. More information on the motives and consequences of this split can be found in the documentation for vl2014.

Largely in support of this fork, many books have been reorganized. Many books that are specific to the VL/ESIM flow have been moved into the ESIM directory:

centaur/vl/top.lisp --> centaur/vl/defmodules.lisp (with a stub)
centaur/vl/defmodules.lisp --> centaur/esim/defmodules.lisp
centaur/vl/translation.lisp --> centaur/esim/translation.lisp
centaur/vl/toe --> centaur/esim/vltoe (filenames have been unsmurfed)
centaur/vl/util/esim-lemmas.lisp --> centaur/esim/vltoe
centaur/vl/transforms/occform/* --> centaur/esim/occform

Various other files have also been moved into ESIM:

centaur/tutorial --> centaur/esim/tutorial
centaur/vcd --> centaur/esim/vcd
centaur/regression --> centaur/esim/tests

Many other minor file-name changes have been made to help improve the organization of the code base.

The various VL flows are also now better separated. For instance:

The ESIM flow no longer performs certain linter checks that are better handled by VL-Lint. For instance, it no longer generates a classic use-set-report since the new Lucid reporting is much better.
The vl model command (based on the ESIM flow) is no longer used in the module browser. Instead, the module browser now reads .vlzip files that are produced by the vl zip command, which is independent of ESIM.

Extended Support for Verilog/SystemVeriog

The new VL (and in some cases VL2014) now have better support for at least the following Verilog/SystemVerilog features:

.* connections that involve interface ports,
return statements in functions,
inside expressions like a inside {b, c, [d:e]},
generate constructs,
System functions like $bits and $clog2,
Unpacked dimensions in various contexts,
Matched end : foo style endings on blocks,
Declarations on unnamed blocks,
Typedefs with a single unpacked dimension, i.e., typedef ... foo_t [3],
Ports whose expressions involve parameters,
Scope expressions and other complex hierarchical expressions,
Module level begin/end blocks (not in the spec but supported by simulators),
Package imports in block statements, functions, and tasks,
Certain complex assignment patterns,
The `", `\`\", and `` escapes in `define macros,
Certain macro invocations in `include/`ifdef forms,

vl::vl-lint Improvements

The loader works harder to attach parse-time warnings to the appropriate modules.

The new vl::lucid check is a far more capable check for unused, unset, and multiply driven wires, with proper understanding of SystemVerilog scoping. The old use-set and multidrive warnings have been retired.

Heuristic improvements have been made to leftright checking, extension/fussy size warnings for '1/'0/..., and duplicate instance checking involving interfaces and portless modules. Extension warning heuristics are also now attachable.

Improved the warning messages for zero-sized replications, overflowing integer literals, and generally for warnings where expressions involve parameters after unparameterization.

Portcheck now warns about stylistically undesirable ports such as foo[3:0].

There is now a basic suite of system-level tests directed at the linter; see the linttest directory. These tests have shed light on many minor linter bugs.