[acl2/acl2] d66833: VL: preprocessor updates and miscellaneous tweaks

[GitHub]

Branch: refs/heads/master
Home: https://github.com/acl2/acl2
Commit: d66833bb2fe70a03995f47091376508b143c80dc
https://github.com/acl2/acl2/commit/d66833bb2fe70a03995f47091376508b143c80dc
Author: Jared C. Davis <jared....@gmail.com>
Date: 2016-09-28 (Wed, 28 Sep 2016)

Changed paths:
M books/GNUmakefile
M books/centaur/sv/cosims/Makefile
A books/centaur/sv/cosims/pp1/spec.sv
A books/centaur/sv/cosims/pp2/spec.sv
A books/centaur/sv/cosims/pp3/spec.sv
A books/centaur/sv/cosims/pp4/spec.sv
A books/centaur/sv/cosims/pp5/spec.sv
A books/centaur/sv/cosims/protect/spec.sv
A books/centaur/sv/failtest/protect1.v
A books/centaur/sv/failtest/protect2.v
M books/centaur/vl/kit/lint.lisp
M books/centaur/vl/lint/lucid.lisp
M books/centaur/vl/linttest/Makefile
M books/centaur/vl/linttest/bits/check.rb
M books/centaur/vl/linttest/dpi/check.rb
M books/centaur/vl/linttest/duplicates/check.rb
M books/centaur/vl/linttest/extension/check.rb
M books/centaur/vl/linttest/fussy/check.rb
M books/centaur/vl/linttest/implicit/check.rb
M books/centaur/vl/linttest/leftright/check.rb
M books/centaur/vl/linttest/lucid/check.rb
M books/centaur/vl/linttest/multi/check.rb
M books/centaur/vl/linttest/oddexpr/check.rb
M books/centaur/vl/linttest/overflow/check.rb
M books/centaur/vl/linttest/params/check.rb
M books/centaur/vl/linttest/portcheck/check.rb
M books/centaur/vl/linttest/sameports/check.rb
M books/centaur/vl/linttest/shadowcheck/check.rb
M books/centaur/vl/linttest/translateoff/check.rb
M books/centaur/vl/linttest/trunc/check.rb
M books/centaur/vl/loader/lexer/strings.lisp
M books/centaur/vl/loader/lexer/tests.lisp
M books/centaur/vl/loader/lexer/top.lisp
M books/centaur/vl/loader/parser/udps.lisp
M books/centaur/vl/loader/preprocessor/tests.lisp
M books/centaur/vl/loader/preprocessor/top.lisp
M books/centaur/vl/loader/top.lisp
M books/centaur/vl/mlib/fmt.lisp
M books/centaur/vl/util/sum-nats.lisp

Log Message:
-----------
VL: preprocessor updates and miscellaneous tweaks

Added preprocessor support for `__FILE__ and `__LINE__.

Added preprocessor support for (ignoring) `protect and
`endprotect. These aren't in the standard, but are apparently
some archaic Verilog-XL thing for encryption and are still
supported by commercial tools like NCV/VCS. Added some cosims
and failtests related to these.

Added preprocessor/lexer support for (ignoring) `timescale
`myscale. Formerly we allowed (and ignored) things like
`timescale 1ns/1ps, but we failed to support things like
`timescale `myscale because we just did not try to do any
macro-expansion here. (This was a bit tricky to do efficiently.
Short story: we now preserve the `timescale token through
preprocessing, and wait until lexing to eat it and its argument.)

Removed a preprocessor restriction about not using compiler
directives within a `define. For example, we now permit things
like `define foo `ifdef bar ... `endif.

Fixed a preprocessor bug with `" sequences in `define macros
without arguments. For example:

`define FOO `"FOO`"
$display(`FOO);

was essentially expanding into:

$display(`"FOO`");

which is not correct. Fixed this (and probably related bugs with
things like `` and `\`") by using the real macro-text expansion
routine even in the case where the `define macro has no
arguments. Also added a cosim to make sure it keeps working.

Fixed a preprocessor bug with line continuations. In `defines,
we previously expanded a line continuation into a space, which
doesn't seem to match tools like NCV and VCS in certain cases
involving nested `define forms. We now expand \<newline> into a
single newline character, which seems to match better. Add a few
cosims to check this behavior.

Added lexer support for escaped forward slashes in string
literals, i.e., you can now write "\/" and similar. I don't
think SystemVerilog-2012 $5.9 is very clear on whether this is
allowed, but the new behavior appears to match NCV/VCS.

Changed preprocessor error messages to use ~f0 instead of ~s0 for
file names, so that long paths don't get broken up across lines
in weird ways.

Fixed a minor bug with the vl-fmt ~@ directive error messages.

Fixed a minor bug with parsing UDP edge symbols.

Tweaked memory allocation configuration for the "vl lint" command
(basically: use vl-gc correctly).

Extend cosims testing Makefile to pass NCV_FLAGS and VCS_FLAGS to
NCVerilog and VCS, to support use in environments where any extra
flags might be desired.

Made nats-from tail-recursive and added a safety valve to Lucid's
lint check to avoid problems when handling very wide wires.

Tweaked linter test to be able to support additional Ruby
configurations.

Added a "make vlfull" target to the main books/Makefile, which is
the same as "make vl" except that it also runs the SV cosims that
are expected to be passing (which requires commercial Verilog
simulators).

Extended the "vl lint" kit command's handling of --debug so that
it enables loader debugging, and adjust the loader so that when
debugging is enabled more messages are printed.

Added a dumb warning to the VL loader to detect multiple
occurrences of the same start file, i.e., if you try to load
foo.v multiple times you'll now get a warning and it will ignore
the second occurrence.


Commit: 58726c264a0a19c5c682a30d74a6ba01bbc65bde
https://github.com/acl2/acl2/commit/58726c264a0a19c5c682a30d74a6ba01bbc65bde
Author: David L. Rager <rag...@gmail.com>
Date: 2016-09-29 (Thu, 29 Sep 2016)

Changed paths:
M books/GNUmakefile
M books/centaur/sv/cosims/Makefile
A books/centaur/sv/cosims/pp1/spec.sv
A books/centaur/sv/cosims/pp2/spec.sv
A books/centaur/sv/cosims/pp3/spec.sv
A books/centaur/sv/cosims/pp4/spec.sv
A books/centaur/sv/cosims/pp5/spec.sv
A books/centaur/sv/cosims/protect/spec.sv
A books/centaur/sv/failtest/protect1.v
A books/centaur/sv/failtest/protect2.v
M books/centaur/vl/kit/lint.lisp
M books/centaur/vl/lint/lucid.lisp
M books/centaur/vl/linttest/Makefile
M books/centaur/vl/linttest/bits/check.rb
M books/centaur/vl/linttest/dpi/check.rb
M books/centaur/vl/linttest/duplicates/check.rb
M books/centaur/vl/linttest/extension/check.rb
M books/centaur/vl/linttest/fussy/check.rb
M books/centaur/vl/linttest/implicit/check.rb
M books/centaur/vl/linttest/leftright/check.rb
M books/centaur/vl/linttest/lucid/check.rb
M books/centaur/vl/linttest/multi/check.rb
M books/centaur/vl/linttest/oddexpr/check.rb
M books/centaur/vl/linttest/overflow/check.rb
M books/centaur/vl/linttest/params/check.rb
M books/centaur/vl/linttest/portcheck/check.rb
M books/centaur/vl/linttest/sameports/check.rb
M books/centaur/vl/linttest/shadowcheck/check.rb
M books/centaur/vl/linttest/translateoff/check.rb
M books/centaur/vl/linttest/trunc/check.rb
M books/centaur/vl/loader/lexer/strings.lisp
M books/centaur/vl/loader/lexer/tests.lisp
M books/centaur/vl/loader/lexer/top.lisp
M books/centaur/vl/loader/parser/udps.lisp
M books/centaur/vl/loader/preprocessor/tests.lisp
M books/centaur/vl/loader/preprocessor/top.lisp
M books/centaur/vl/loader/top.lisp
M books/centaur/vl/mlib/fmt.lisp
M books/centaur/vl/util/sum-nats.lisp

Log Message:
-----------
Merge pull request #647 from jaredcdavis/vl

VL: preprocessor updates and miscellaneous tweaks


Compare: https://github.com/acl2/acl2/compare/4d8c221493b5...58726c264a0a

[GitHub]

Branch: refs/heads/testing