• Top
  • Documentation
  • Books
  • 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
  • Math
  • Testing-utilities

• 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.