		Search-engine friendly clone of the ACL2 documentation.

Note-7-2-books

Note-7-2-vl

Notes about changes to vl and sv in ACL2 7.2.

Below we describe changes since the ACL2 7.1 release to the unstable, development version of vl. Note that the stable version, vl2014, is essentially unchanged except for minor bugfixes. See also note-7-1-vl for some background about VL and VL2014.

Extended SystemVerilog Support

Much of the development work has focused on supporting additional features of SystemVerilog.

Interfaces. VL and SV now have much better support for interfaces. They can now contain functions, tasks, assignments, etc. Modports are now generally understood: they participate in scopes, are sanity checked for name clashes, are supported in submodule instantiation, etc. Interface usage in submodule instances are properly type checked and are generally supported in VL and through SV. Note that interface arrays are not yet supported.

Assertions. VL's parser and pretty-printer now support many SystemVerilog assertion features, including at least sequence/property expressions (see vl::property-expressions), procedural assertions (see vl::vl-assertstmt and vl::vl-cassertstmt), sequence and property declarations (see vl::vl-sequence and vl::vl-property), and module-level assertions (see vl::vl-assertion and vl::vl-cassertion). Note that all of this assertion-related stuff is currently ignored by the SV flow. However, modules with assertions should at least no longer result in parse errors, and these structures may some day be a useful basis for implementing assertion checking tools.

Aliases. Alias constructs should now work in VL and are also supported by SV.

Expressions. The ** (exponent/power) operator, inside operator are now supported in both vl and SV. Note that NCV/VCS disagree about the sizing of inside operators and that in general these operators may be buggy on commercial tools. Added support for a few additional system functions like $dimensions, etc.

Statements. The parsing and representation of vl::statements has been extended in various ways. Note that our support for statements in SV is still rather limited, so just because we can parse these things doesn't necessarily mean they will be handled all the way through the SV flow:

break and continue statements are now implemented.
Statement labels are now supported.
There is better support for subroutine call statements; so we can now parse things like void'(...) and otherwise do slightly better with calls of tasks/functions in statements.
We now permit function calls/task enables with explicit parens but no arguments. (In Verilog-2005, was is syntactically legal to write statements like mytask; but not mytask(); with the explicit parens, even though they seem like they should be equivalent. In SystemVerilog both forms are allowed, but we had previously only supported the mytask; version.)
Block statements (begin/end, fork/join, ...) can now have typedefs. We can now parse fork/join_any and fork/join_none statements.
final statements are now allowed. Much like initial statements, these are simply ignored in the SV flow.

DPI import/exports. DPI import/exports, used to connect SystemVerilog to C programs, are now tolerated by VL's parser and are now to some degree understood by other parts of VL. For instance, they are known to vl::scopestacks and can be considered when checking for name clashes, introducing implicit wires, etc. See vl::vl-dpiimport and vl::vl-dpiexport.

Instances. Module and gate instance arrays can now use the single-expression ranges, i.e., we now support things like:

and foo [3] (o, a, b);
submod foo [3] (a, b, c);

Note that SystemVerilog also allows multiple-dimension instance arrays, but those are still unsupported.

Other. Many bugfixes (e.g., to the parser, scoping, etc) have resulted in VL being able to successfully load additional designs.

Scoping and vl::annotate improvements.

The SV and Linter flows now use a unified vl::annotate meta-transform to prepare the design for analysis. This transform has been significantly improved to do a better job with scoping issues related to functions, tasks, generate constructs, and statements. This provides broad improvements to what VL can successfully parse and translate.

The vl::make-implicit-wires transformation, which plays a surprisingly important role in getting scoping right, now more closely matches commercial tools like NCV and VCS. We are particularly more careful about how implicit wires are inferred from expressions involving indexing/selection like foo[w]. In general, in a structure pattern like '{foo : 3}, it's tricky to tell whether foo is a structure member or a parameter. VL now handles this much better and our strategy is documented; see vl::vl-patternkey-ambiguity. It also used to be that such patterns could fool VL into inferring implicit wires for foo! This has been fixed.

Much of make-implicit-wires has been moved into the related vl::shadowcheck transform. The representation of functions and tasks has been adjusted to better support correct scoping and shadowchecking, and shadowcheck now understands user-defined types. Shadowcheck was also incorrectly handling certain situations with package imports, which has been fixed. It also now checks for name clashes in all scopes and produces good warnings in this case. Finally, shadowcheck treats the global scope in a less incorrect way, fixing many problems with global package imports.

VL's scoping of generates also used to be completely wrong. While it still has some known bugs, it has been significantly improved. The scoping of genvars is also improved. Bugs have also been fixed related to disambiguating types from expressions in functions and tasks, and also in the handling of types versus interfaces in ports.

Generates, Elaboration

One of the trickiest parts of VL is elaboration, where parameters are expanded into constants, generate blocks are resolved, etc. To evaluate a parameter like

parameter foo = $bits(mypkg::mytype_t) + blah2size(settings.blah);

we need to evaluate its expression. This can involve looking up the values of other parameters from other places in the hierarchy, evaluating system and user-defined functions, etc. Functions are defined in terms of statements, so we need to understand statements as well. This all gets to be a very messy mutual recursion.

VL's implementation of elaboration now reuses much of the SV code for converting Verilog expressions into sv::svexes, and is now able to resolve many significantly more complex parameters and generates.

Linter

The vl::vl-lint tool now uses much more of the SV code. It shares the vl::annotate code with the SV flow and also uses SV-based elaboration, which provides much better handling of generates and allows it to unparameterize modules involving types and other complex expressions. The very useful size warnings from VL2014 have also been ported to work with the new SV code base.

Various warning heuristics and messages have been tweaked. We no longer complain about duplicate interface instances, since that's perfectly reasonable. Parse errors have some additional context. Lucid has been extended to understand new features like interfaces and modports, DPI imports/exports, and final blocks.

Test Suites

Significant work has gone into testing VL. VL now has three test suites:

centaur/vl/linttest — tests of Linter functionality. This notably includes a lot of tests of scoping and sizing issues.
centaur/sv/cosims — tests comparing VL+SV behavior against that of commercial simulators such as NCV and VCS. These are our main tests of SV. You can also search for no_ncv or no_vcs to discover places where VL disagrees with one tool or another (e.g., because the commercial tools don't agree.)
centaur/sv/failtest — tests that ensure VL+SV report fatal errors for modules that have some bad problem. This turns out to be a nice way to test many scoping issues and make sure that we will reject bad constructs.

Running make vl in the acl2/books directory now automatically also runs all of the linttests and failtests. It doesn't automatically run the cosims, since that requires commercial simulators.)

Each of the test suites has been extended considerably, especially in the tricky areas of scoping, implicit wire creation, generate handling, and also in order to test new features like interface support. Many of the old VL2014 systest tests have also been ported to the new cosims format.

Other Notes

VL and SV are still evolving rapidly and a lot is in flux.

There has been significant renaming of files, moving of files, and deleting of dead files. The documentation has gotten a lot of work in some areas, but of course there is more to do.

Numerous minor bugfixes in all areas of VL are not mentioned, but can be found in the change log.