• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
        • Warnings
        • Primitives
        • Use-set
        • Syntax
        • Getting-started
        • Utilities
        • Loader
        • Transforms
        • Lint
        • Mlib
        • Server
        • Kit
          • Vl-model
          • Vl-json
          • Vl-gather
          • Vl-server
          • Vl-pp
          • Vl-lint
          • Vl-main
          • Vl-toolkit-other-command
          • Vl-help
        • Printer
        • Esim-vl
        • Well-formedness
      • Sv
      • Fgl
      • Vwsim
      • Vl
      • X86isa
      • Svl
      • Rtl
    • Software-verification
    • Math
    • Testing-utilities
  • 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.