• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Debugging
    • Projects
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
        • Symbolic-test-vectors
          • Defstv
          • Stv-compile
          • Symbolic-test-vector-format
          • Stv-implementation-details
          • Compiled-stv-p
          • Stv-run-for-all-dontcares
          • Stv-run
          • Stv-process
          • Stv-run-check-dontcares
          • Symbolic-test-vector-composition
          • Stv-expand
          • Stv-easy-bindings
          • Stv-debug
          • Stv-run-squash-dontcares
          • Stvdata-p
          • Stv-doc
          • Stv2c
            • Stv2c-opts-p
              • Parse-stv2c-opts
              • Stv2c-opts
              • Make-stv2c-opts
              • Change-stv2c-opts
              • Honsed-stv2c-opts
              • Make-honsed-stv2c-opts
              • *stv2c-opts-usage*
              • Stv2c-opts->stv
              • Stv2c-opts->strict
              • Stv2c-opts->start-files
              • Stv2c-opts->search-path
              • Stv2c-opts->search-exts
              • Stv2c-opts->readme
              • Stv2c-opts->mem
              • Stv2c-opts->help
              • Stv2c-opts->edition
              • Stv2c-opts->defines
            • Stv2c-c-symbol-names
            • Stv2c-outs-structdef
            • Stv2c-ins-structdef
            • Stv2c-c-symbol-name
            • Stv2c-header
            • Stv2c-main
          • Stv-widen
          • Stv-out->width
          • Stv-in->width
          • Stv->outs
          • Stv-number-of-phases
          • Stv->ins
          • Stv-suffix-signals
          • Stv->vars
        • Esim-primitives
        • E-conversion
        • Esim-steps
        • Patterns
        • Mod-internal-paths
        • Defmodules
        • Esim-simplify-update-fns
        • Esim-tutorial
        • Esim-vl
      • Vl2014
      • Sv
      • Fgl
      • Vl
      • X86isa
      • Svl
      • Rtl
    • Software-verification
    • Testing-utilities
    • Math
  • Stv2c

Stv2c-opts-p

Command line options for the stv2c tool.

(stv2c-opts-p x) is a std::defaggregate of the following fields.

  • help — Show a brief usage message and exit.
        Invariant (booleanp help).
  • readme — Show a more elaborate README message and exit.
        Invariant (booleanp readme).
  • stv — The symbolic test vector that will be used to run the module.
        Invariant (stringp stv).
  • start-files — Verilog files to parse. (Not options; this is the rest of the command line, hence :hide t).
        Invariant (string-listp start-files).
  • search-path — 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).
  • defines — Set up definitions to use before parsing begins. Equivalent to putting `define VAR 1 at the top of your Verilog file. You can give this option multiple times.
        Invariant (string-listp defines).
  • 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 (vl2014::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).

Source link: stv2c-opts-p

Subtopics

Parse-stv2c-opts
Parse arguments from the command line into a stv2c-opts-p aggregate.
Stv2c-opts
Raw constructor for stv2c-opts-p structures.
Make-stv2c-opts
Constructor macro for stv2c-opts-p structures.
Change-stv2c-opts
A copying macro that lets you create new stv2c-opts-p structures, based on existing structures.
Honsed-stv2c-opts
Raw constructor for honsed stv2c-opts-p structures.
Make-honsed-stv2c-opts
Constructor macro for honsed stv2c-opts-p structures.
*stv2c-opts-usage*
Automatically generated usage message.
Stv2c-opts->stv
Access the stv field of a stv2c-opts-p structure.
Stv2c-opts->strict
Access the strict field of a stv2c-opts-p structure.
Stv2c-opts->start-files
Access the start-files field of a stv2c-opts-p structure.
Stv2c-opts->search-path
Access the search-path field of a stv2c-opts-p structure.
Stv2c-opts->search-exts
Access the search-exts field of a stv2c-opts-p structure.
Stv2c-opts->readme
Access the readme field of a stv2c-opts-p structure.
Stv2c-opts->mem
Access the mem field of a stv2c-opts-p structure.
Stv2c-opts->help
Access the help field of a stv2c-opts-p structure.
Stv2c-opts->edition
Access the edition field of a stv2c-opts-p structure.
Stv2c-opts->defines
Access the defines field of a stv2c-opts-p structure.