• 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
          • Lint-warning-suppression
          • Warning-basics
          • Vl-warning
          • Vl-warninglist-add-ctx
          • Vl-warninglist->types
          • Propagating-errors
          • Vl-reportcard
          • Vl-some-warning-fatalp
          • Clean-warnings
          • Lint-whole-file-suppression
          • Warn
          • Vl-warninglist
          • Vl-remove-warnings
          • Vl-keep-warnings
          • Flat-warnings
          • Vl-some-warning-of-type-p
          • Vl-msg
          • Vl-warning-add-ctx
          • Vl-print-warning
          • Vmsg-binary-concat
          • Ok
          • Vl-trace-warnings
          • Fatal
          • Vmsg
        • Getting-started
        • Utilities
        • Printer
        • Kit
        • Mlib
        • Transforms
      • X86isa
      • Svl
      • Rtl
    • Software-verification
    • Math
    • Testing-utilities
  • Vl

Warnings

Support for handling warnings and errors.

Many parts of VL can run into situations where we want to issue warnings or cause errors. In these situations, VL creates vl-warning objects. These warnings can be attached to major design elements such as modules and interfaces. They can later be collected, examined, filtered, etc.

New users: You may wish to see warning-basics for a broad discussion of VL's philosophy toward handling warnings before looking at the functions below.

Quick Guide

VL includes many functions for creating, collecting, printing, filtering, and otherwise working with warnings.

  • The core warning data structure is a vl-warning, but more often these are found in a vl-warninglist, which are often called warnings accumulators.
  • For creating warnings, there are some convenient macros for extend warnings accumulators with new warnings; see ok, warn, fatal. As a new alternative to warnings accumulators, see also vmsg, vl-warning-add-ctx, and the special patbind-wmv binder for b*.
  • Functions for displaying, filtering, etc. a warning list include:
    • vl-warnings-to-string and vl-print-warnings
    • vl-clean-warnings and vl-warning-sort
    • vl-keep-warnings and vl-remove-warnings
    • vl-some-warning-fatalp and vl-some-warning-of-type-p.
  • You can get a vl-reportcard that summarizes the warnings that are attached to design elements such as modules, interfaces, etc. A report card can also be printed, filtered, etc., see vl-reportcard for details. You can alternately extract all of the warnings as a list of flat-warnings.
  • Fatal warnings can be propagated throughout a design to transitively any superior design elements as having fatal warnings somewhere below. See propagating-errors.
  • VL hackers may want to know about vl-trace-warnings, which just traces warning creation in a nice way so that you can see warnings as they are created (e.g., between print statements or other kinds of tracing.)
  • Warnings are heavily used in vl-lint, which features some special mechanisms for suppressing warnings; see lint-warning-suppression.

Subtopics

Lint-warning-suppression
An attribute- mechanism for suppressing particular warnings when using vl-lint.
Warning-basics
General introduction to vl-warning objects and error handling in VL.
Vl-warning
Fundamental warning object used throughout vl.
Vl-warninglist-add-ctx
(vl-warninglist-add-ctx x ctx) maps vl-warning-add-ctx across a list.
Vl-warninglist->types
(vl-warninglist->types x) maps vl-warning->type across a list.
Propagating-errors
A mechanism for propagating fatal errors from submodules up to all modules that rely on these submodules.
Vl-reportcard
A (typically fast) alist associating names to warnings.
Vl-some-warning-fatalp
Check if any warning is marked as fatal.
Clean-warnings
A transform to clean up all the warnings in a design.
Lint-whole-file-suppression
A filter for dropping warnings from whole modules (and other design elements) based on filenames.
Warn
Extend a warnings accumulator with a non-fatal warning.
Vl-warninglist
A list of vl-warning-p objects.
Vl-remove-warnings
Remove warnings of certain types.
Vl-keep-warnings
Keep only warnings of certain types.
Flat-warnings
Extract flat lists of warnings from various design elements.
Vl-some-warning-of-type-p
Check if there are any warnings of certain types.
Vl-msg
Vl-warning-add-ctx
Vl-print-warning
Pretty-print a vl-warning.
Vmsg-binary-concat
Ok
A convenient shorthand for calling vl-warninglist-fix.
Vl-trace-warnings
Pretty-print warnings as they are created.
Fatal
Extend a warnings accumulator with a fatal warning.
Vmsg
Similar to msg; constructs a vl-msg that can be used with ~@ directives in VL's formatted-printing routines.