		Search-engine friendly clone of the ACL2 documentation.

Vl2014

Kit

A command-line program for using VL in basic ways.

vl2014 is mainly an ACL2 library, and a lot of its functionality and features are available only from within ACL2. However, to make VL more widely approachable, we have bundled up certain pieces of it into a command line program, which we call the Kit.

The kit is ordinarily built by running make vl in the acl2/books directory. The source files are found in acl2/books/centaur/vl2014/kit but the resulting executable is put into acl2/books/centaur/vl2014/bin and is simply named vl.

This vl program is really just a wrapper for several sub-commands:

VL 2014 -- VL Verilog Toolkit, 2014 Edition
Copyright (C) 2008-2015 Centaur Technology <http://www.centtech.com>

Usage: vl2014 <command> [arguments]

Commands:

  help    Print this message, or get help on a particular VL command
  json    Convert Verilog designs into JSON files (for easy parsing)
  lint    Find potential bugs in a Verilog design
  model   Translate Verilog designs for the ACL2 theorem prover
  stv2c   Translate symbolic runs of Verilog designs into C++
  pp      Preprocess Verilog designs
  gather  Collect Verilog files into a single file
  server  Start a VL web server (for web-based module browsing)
  shell   Interactive VL shell (for experts)

Use 'vl2014 help <command>' for help on a specific command.

Subtopics

Vl-model: The vl model command.
Vl-json: The vl json command.
Vl-gather: The vl gather command.
Vl-server: The vl server command.
Vl-pp: The vl pp command.
Vl-lint: The vl lint command.
Vl-main: The top-level vl meta-command.
Vl-toolkit-other-command: Handler for additional vl toolkit commands.
Vl-help: The vl help command.