• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
    • Vwsim
    • Fgl
    • Vl
      • Syntax
      • Loader
      • Warnings
      • Getting-started
      • Utilities
      • Printer
      • Kit
        • Vl-lint
        • Vl-server
        • Vl-gather
        • Vl-zip
        • Vl-main
          • Vl-toolkit-other-command
          • Vl-help
        • Split-plusargs
        • Vl-shell
        • Vl-json
      • Mlib
      • Transforms
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Testing-utilities
  • Math

• Kit

Vl-main

Top level entry point into the kit. This just handles the command-line parsing and invokes the right sub-command for the vl executable.

Signature

(vl-main &key (state 'state)) → state

Note that the kit is extensible and it is relatively easy to add new commands even without releasing your code. See in particular vl-toolkit-other-command.

Definitions and Theorems

Function: vl-main-fn

(defun
 vl-main-fn (state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard t))
 (let
   ((__function__ 'vl-main))
   (declare (ignorable __function__))
   (b* ((state (set-debugger-enable :bt-break))
        (- (gc-verbose t))
        (- (acl2::tshell-ensure))
        ((mv argv state) (oslib::argv))
        ((unless (consp argv))
         (b* ((state (vl-help '("help"))))
             (exit-fail)
             state))
        ((cons cmd args) argv)
        ((when (or (equal cmd "help")
                   (equal cmd "-h")
                   (equal cmd "--help")))
         (b* ((state (vl-help args)))
             (exit-ok)
             state))
        ((when (equal cmd "lint"))
         (b* ((state (vl-lint-top args)))
             (and (not (intersectp-equal '("--shell" "--post-shell")
                                         args))
                  (exit-ok))
             state))
        ((when (equal cmd "gather"))
         (b* ((state (vl-gather-top args)))
             (exit-ok)
             state))
        ((when (equal cmd "zip"))
         (b* ((state (vl-zip-top args)))
             (exit-ok)
             state))
        ((when (equal cmd "json"))
         (b* ((state (vl-json-top args)))
             (exit-ok)
             state))
        ((when (equal cmd "server"))
         (b* ((state (vl-server-top args)))
             state))
        ((when (equal cmd "shell"))
         (b* ((state (vl-shell-top args)))
             state)))
       (vl-toolkit-other-command cmd args state))))

Subtopics

Vl-toolkit-other-command

Attachable handler for extending the VL kit with additional commands.

Vl-help

Show help on how to use VL kit commands.