• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
      • Sv
      • Fgl
      • Vwsim
      • Vl
        • Syntax
        • Loader
        • Warnings
        • Getting-started
        • Utilities
        • Printer
        • Kit
          • Vl-lint
            • Vl-lintconfig-p
              • Parse-vl-lintconfig
              • Vl-lintconfig
              • *vl-lintconfig-usage*
              • Make-vl-lintconfig
              • Change-vl-lintconfig
              • Honsed-vl-lintconfig
              • Make-honsed-vl-lintconfig
              • Vl-lintconfig->topmods
              • Vl-lintconfig->strict
              • Vl-lintconfig->stmt-limit
              • Vl-lintconfig->start-files
              • Vl-lintconfig->shell
              • Vl-lintconfig->search-path
              • Vl-lintconfig->search-exts
              • Vl-lintconfig->readme
              • Vl-lintconfig->quiet
              • Vl-lintconfig->post-shell
              • Vl-lintconfig->plusargs
              • Vl-lintconfig->no-typo
              • Vl-lintconfig->no-sv-use-set
              • Vl-lintconfig->no-html
              • Vl-lintconfig->mem
              • Vl-lintconfig->include-dirs
              • Vl-lintconfig->ignore-files
              • Vl-lintconfig->ignore
              • Vl-lintconfig->help
              • Vl-lintconfig->global-packages
              • Vl-lintconfig->elab-limit
              • Vl-lintconfig->edition
              • Vl-lintconfig->dropmods
              • Vl-lintconfig->defines
              • Vl-lintconfig->debug
              • Vl-lintconfig->cclimit
            • Condcheck
            • Lint-warning-suppression
            • Lucid
            • Lvaluecheck
            • Vl-interfacelist-alwaysstyle
            • Truncation-warnings
            • Vl-modulelist-alwaysstyle
            • Skip-detection
            • Vl-lint-report
            • Vl-lintresult
            • Vl::vl-design-sv-use-set
            • Oddexpr-check
            • Leftright-check
            • Duplicate-detect
            • Selfassigns
            • *vl-lint-help*
            • Arith-compare-check
            • Dupeinst-check
            • Qmarksize-check
            • Lint-whole-file-suppression
            • Run-vl-lint-main
            • Logicassign
            • Run-vl-lint
            • Vl-print-certain-warnings
            • Duperhs-check
            • Vl-lint-top
            • Sd-filter-problems
            • Vl-modulelist-add-svbad-warnings
            • Vl-module-add-svbad-warnings
            • Check-case
            • Vl-lint-extra-actions
            • Drop-lint-stubs
            • Vl-lint-print-warnings
            • Drop-user-submodules
            • Check-namespace
            • Vl-lintconfig-loadconfig
            • Vl-lint-design->svex-modalist-wrapper
            • Vl-delete-sd-problems-for-modnames-aux
            • Vl-collect-new-names-from-orignames
            • Vl-lint-print-all-warnings
            • Vl-design-remove-unnecessary-modules
            • Vl-delete-sd-problems-for-modnames
            • Vl-always-check-style
            • Vl-vardecllist-svbad-warnings
            • Vl-vardecl-svbad-warnings
            • Vl-reportcard-remove-suppressed
            • Vl-reportcard-keep-suppressed
            • Vl-alwayslist-check-style
            • Vl-remove-nameless-descriptions
            • Vl-lint-apply-quiet
            • Vl-warninglist-remove-suppressed
            • Vl-warninglist-keep-suppressed
            • Vl-print-eliminated-descs
            • Vl-module-alwaysstyle
            • Vl-jp-reportcard-aux
            • Vl-interface-alwaysstyle
            • Vl-design-alwaysstyle
            • Vl-jp-description-locations
            • Vl-jp-reportcard
            • Vl-pp-stringlist-lines
            • Vl-jp-design-locations
            • Vl-datatype-svbad-p
            • Unpacked-range-check
            • Sd-problem-major-p
            • Vl-alwaysstyle
          • Vl-server
          • Vl-gather
          • Vl-zip
          • Vl-main
          • Split-plusargs
          • Vl-shell
          • Vl-json
        • Mlib
        • Transforms
      • X86isa
      • Svl
      • Rtl
    • Software-verification
    • Math
    • Testing-utilities
  • Vl-lint

Vl-lintconfig-p

Command-line options for running vl lint.

(vl-lintconfig-p x) is a defaggregate of the following fields.

  • start-files — The list of files to process.
        Invariant (string-listp start-files).
  • plusargs — The list of +args, with plusses removed.
        Invariant (string-listp plusargs).
  • help — Show a brief usage message and exit.
        Invariant (booleanp help).
  • readme — Show a more elaborate README and exit.
        Invariant (booleanp readme).
  • search-path — Control the search path for finding modules. You can give this switch multiple times, to set up multiple search paths in priority order.
        Invariant (string-listp search-path).
  • search-exts — Control the search extensions for finding modules. You can give this switch multiple times. By default we just look for files named "foo.v" in the --search directories. But if you have Verilog files with different extensions, this won't work, so you can add these extensions here. EXT should not include the period, e.g., use "--searchext vv" to consider files like "foo.vv", etc.
        Invariant (string-listp search-exts).
  • include-dirs — Control the list of directories for `include files. You can give this switch multiple times. By default, we look only in the current directory.
        Invariant (string-listp include-dirs).
  • topmods — Limit the scope of the report to MOD. By default we include all warnings for any module we encounter. But if you say "--topmod foo", we suppress all warnings for modules that foo does not depend on. You can give this switch multiple times, e.g., "--topmod foo --topmod bar" means: only show warnings for foo, bar, and modules that they depend on.
        Invariant (string-listp topmods).
  • quiet — Suppress all warnings that about MOD. You can give this switch multiple times, e.g., "-q foo -q bar" will hide the warnings about modules foo and bar.
        Invariant (string-listp quiet).
  • dropmods — Delete MOD from the module hierarchy before doing any linting at all. This is a gross (but effective) way to work through any bugs in the linter that are triggered by certain modules. The dropped modules are removed from the module list without destroying modules above them. This may occasionally lead to false warnings about the modules above (e.g., it may think some wires are unused, because the module that uses them has been removed.).
        Invariant (string-listp dropmods).
  • ignore — Ignore warnings of this TYPE. For instance, "--ignore oddexpr" will suppress VL_WARN_ODDEXPR warnings. Note that there are much finer-grained ways to suppress warnings; see "vl lint --readme" for more information.
        Invariant (string-listp ignore).
  • ignore-files — Ignore warnings from modules in filename. For instance, "--ignore-file foo.v" will suppress all warnings from modules in foo.v (from any directory). You can also give absolute paths, in which case only exact matches will be suppressed. Note that there are much finer-grained ways to suppress warnings; see "vl lint --readme" for more information.
        Invariant (string-listp ignore-files).
  • defines — Set up definitions to use before parsing begins. For instance, "--define foo" is similar to "`define foo" and "--define foo=3" is similar to "`define foo 3". Note: these defines are "sticky" and will override subsequent `defines in your Verilog files unless your Verilog explicitly uses `undef. You can give this option multiple times.
        Invariant (string-listp defines).
  • cclimit — Limit for the const check. This is a beta feature that is not yet released. Setting N to 0 (the default) disables the check. Otherwise, limit the scope of the check to at most N sub-expressions.
        Invariant (natp cclimit).
  • global-packages — Consider the given package to be global for purposes of the globalparams check; i.e., parameters defined in this package should not be defined anywhere else.
        Invariant (string-listp global-packages).
  • elab-limit — Default 10000. Recursion limit for elaboration. This usually shouldn't matter or need tinkering. It's a safety valve against possible loops in elaboration, e.g., to resolve parameter P you need to evaluate parameter Q, which might require you to resolve R, which might depend hierarchically on P, and so on. So if you hit this there's probably something wrong with your design.
        Invariant (natp elab-limit).
  • stmt-limit — Default 80. Recursion limit for compiling statements, e.g., unrolling loops and figuring out when they terminate. For linting we use a low default limit that is meant to avoid wasting an inordinate amount of time compiling troublesome loops. Increasing this may avoid svex translation warnings, but may result in bad performance in some cases.
        Invariant (natp stmt-limit).
  • no-typo — Disable typo detection (it is sometimes slow).
        Invariant (booleanp no-typo).
  • no-html — Reduce the file size of vl-warnings.json by printing the warnings there in text-only mode.
        Invariant (booleanp no-html).
  • no-sv-use-set — Disable sv-use-set check.
        Invariant (booleanp no-sv-use-set).
  • edition — Which edition of the Verilog standard to implement? Default: "SystemVerilog" (IEEE 1800-2012). You can alternately use "Verilog" for IEEE 1364-2005, i.e., Verilog-2005.
        Invariant (vl-edition-p edition).
  • strict — Disable VL extensions to Verilog.
        Invariant (booleanp strict).
  • mem — How much memory to try to use. Default: 4 GB. Raising this may improve performance by avoiding garbage collection. To avoid swapping, keep this below (physical_memory - 2 GB).
        Invariant (posp mem).
  • debug — Print extra information for debugging.
        Invariant (booleanp debug).
  • shell — Instead of running the linter, enter an ACL2 shell where the linter configuration has been saved as constant vl::*vl-user-lintconfig*.
        Invariant (booleanp shell).
  • post-shell — After running the linter, enter an ACL2 shell where the linter configuration has been saved as constant vl::*vl-user-lintconfig*.
        Invariant (booleanp post-shell).

Source link: vl-lintconfig-p

Subtopics

Parse-vl-lintconfig
Parse arguments from the command line into a vl-lintconfig-p aggregate.
Vl-lintconfig
Raw constructor for vl-lintconfig-p structures.
*vl-lintconfig-usage*
Automatically generated usage message.
Make-vl-lintconfig
Constructor macro for vl-lintconfig-p structures.
Change-vl-lintconfig
A copying macro that lets you create new vl-lintconfig-p structures, based on existing structures.
Honsed-vl-lintconfig
Raw constructor for honsed vl-lintconfig-p structures.
Make-honsed-vl-lintconfig
Constructor macro for honsed vl-lintconfig-p structures.
Vl-lintconfig->topmods
Access the topmods field of a vl-lintconfig-p structure.
Vl-lintconfig->strict
Access the strict field of a vl-lintconfig-p structure.
Vl-lintconfig->stmt-limit
Access the stmt-limit field of a vl-lintconfig-p structure.
Vl-lintconfig->start-files
Access the start-files field of a vl-lintconfig-p structure.
Vl-lintconfig->shell
Access the shell field of a vl-lintconfig-p structure.
Vl-lintconfig->search-path
Access the search-path field of a vl-lintconfig-p structure.
Vl-lintconfig->search-exts
Access the search-exts field of a vl-lintconfig-p structure.
Vl-lintconfig->readme
Access the readme field of a vl-lintconfig-p structure.
Vl-lintconfig->quiet
Access the quiet field of a vl-lintconfig-p structure.
Vl-lintconfig->post-shell
Access the post-shell field of a vl-lintconfig-p structure.
Vl-lintconfig->plusargs
Access the plusargs field of a vl-lintconfig-p structure.
Vl-lintconfig->no-typo
Access the no-typo field of a vl-lintconfig-p structure.
Vl-lintconfig->no-sv-use-set
Access the no-sv-use-set field of a vl-lintconfig-p structure.
Vl-lintconfig->no-html
Access the no-html field of a vl-lintconfig-p structure.
Vl-lintconfig->mem
Access the mem field of a vl-lintconfig-p structure.
Vl-lintconfig->include-dirs
Access the include-dirs field of a vl-lintconfig-p structure.
Vl-lintconfig->ignore-files
Access the ignore-files field of a vl-lintconfig-p structure.
Vl-lintconfig->ignore
Access the ignore field of a vl-lintconfig-p structure.
Vl-lintconfig->help
Access the help field of a vl-lintconfig-p structure.
Vl-lintconfig->global-packages
Access the global-packages field of a vl-lintconfig-p structure.
Vl-lintconfig->elab-limit
Access the elab-limit field of a vl-lintconfig-p structure.
Vl-lintconfig->edition
Access the edition field of a vl-lintconfig-p structure.
Vl-lintconfig->dropmods
Access the dropmods field of a vl-lintconfig-p structure.
Vl-lintconfig->defines
Access the defines field of a vl-lintconfig-p structure.
Vl-lintconfig->debug
Access the debug field of a vl-lintconfig-p structure.
Vl-lintconfig->cclimit
Access the cclimit field of a vl-lintconfig-p structure.