• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
      • Sv
      • Vwsim
      • Fgl
      • Vl
        • Syntax
        • Loader
        • Warnings
          • Lint-warning-suppression
          • Warning-basics
          • Vl-warning
            • Vl-warning-p
            • Vl-warning-fix
            • Make-vl-warning
            • Vl-warning-equiv
            • Vl-warning->suppressedp
            • Change-vl-warning
            • Vl-warning->type
            • Vl-warning->msg
            • Vl-warning->fatalp
            • Vl-warning->args
            • Vl-warning->fn
            • Vl-warning->context
          • Vl-warninglist-add-ctx
          • Vl-warninglist->types
          • Propagating-errors
          • Vl-reportcard
          • Vl-some-warning-fatalp
          • Clean-warnings
          • Lint-whole-file-suppression
          • Vl-keep-warnings
          • Warn
          • Vl-warninglist
          • Vl-remove-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
    • Testing-utilities
    • Math
  • Warnings

Vl-warning

Fundamental warning object used throughout vl.

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.
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 — ACL2::true-list
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.
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.
suppressedp — booleanp
Indicates that this warning was suppressed by an ignore attribute.
context
Context object for this warning; should be NIL or printable with "~a".

Subtopics

Vl-warning-p
Recognizer for vl-warning structures.
Vl-warning-fix
Fixing function for vl-warning structures.
Make-vl-warning
Basic constructor macro for vl-warning structures.
Vl-warning-equiv
Basic equivalence relation for vl-warning structures.
Vl-warning->suppressedp
Get the suppressedp field from a vl-warning.
Change-vl-warning
Modifying constructor for vl-warning structures.
Vl-warning->type
Get the type field from a vl-warning.
Vl-warning->msg
Get the msg 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->fn
Get the fn field from a vl-warning.
Vl-warning->context
Get the context field from a vl-warning.