• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
        • Warnings
          • Vl-warninglist->types
          • Vl-warning
            • Vl-warning-p
            • Vl-warning-fix
            • Vl-warning-equiv
            • Make-vl-warning
            • Change-vl-warning
            • Vl-warning->type
            • Vl-warning->fatalp
            • Vl-warning->args
            • Vl-warning->msg
            • Vl-warning->fn
          • Propagating-errors
          • Vl-reportcard
          • Vl-warning-sort
          • Lint-warning-suppression
          • Clean-warnings
          • Warn
          • Vl-print-warnings-with-header
          • Vl-some-warning-fatalp
          • Vl-print-warnings-with-named-header
          • Flat-warnings
          • Vl-remove-warnings
          • Vl-keep-warnings
          • Vl-print-warnings
          • Vl-some-warning-of-type-p
          • Vl-clean-warnings
          • Vl-warnings-to-string
          • Vl-warninglist
          • Vl-print-warning
          • Ok
          • Vl-trace-warnings
          • Fatal
        • Primitives
        • Use-set
        • Syntax
        • Getting-started
        • Utilities
        • Loader
        • Transforms
        • Lint
        • Mlib
        • Server
        • Kit
        • Printer
        • Esim-vl
        • Well-formedness
      • Sv
      • Fgl
      • Vwsim
      • Vl
      • X86isa
      • Svl
      • Rtl
    • Software-verification
    • Math
    • Testing-utilities
  • Warnings

Vl-warning

Fundamental warning object used throughout vl2014.

This is a product type introduced by defprod.

Fields
type — symbolp
A symbol, most often a keyword symbol, that describes very broadly what kind of warning this is. There is no particular discipline or strategy for assigning types to warnings, but the basic goal is to be able to use these types to filter out or group up similar warnings.
fatalp — booleanp
Indicates whether this error is so severe that the module ought to be thrown away and not subjected to further translation. See the general discussion in warnings for more information on how this is used.
msg — stringp
A more detailed message describing what went wrong. This string should be acceptable to vl-fmt; it is similar to the "format strings" used by ACL2's cw function, but there are some important differences, e.g., not all fmt directives are supported, and extra Verilog-specific directives are available.
args — true-listp
Arguments that will be composed with the tilde directives in msg when the warning is displayed to the user. That is, a directive like ~x0 refers to the first argument, ~x1 to the second, etc.
fn — symbolp
A symbol, intended to be the name of the function that caused the warning. This is intended to be useful for VL debugging, to help make the source of the warning more apparent. Only good discipline (and handy macros) ensure that this is correctly reported.

Subtopics

Vl-warning-p
Recognizer for vl-warning structures.
Vl-warning-fix
Fixing function for vl-warning structures.
Vl-warning-equiv
Basic equivalence relation for vl-warning structures.
Make-vl-warning
Basic constructor macro for vl-warning structures.
Change-vl-warning
Modifying constructor for vl-warning structures.
Vl-warning->type
Get the type field from a vl-warning.
Vl-warning->fatalp
Get the fatalp field from a vl-warning.
Vl-warning->args
Get the args field from a vl-warning.
Vl-warning->msg
Get the msg field from a vl-warning.
Vl-warning->fn
Get the fn field from a vl-warning.