• 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
          • Propagating-errors
          • Vl-reportcard
            • Vl-reportcard-p
            • Vl-apply-reportcard
            • Vl-reportcard-fix
            • Vl-extend-reportcard-list
            • Vl-design-origname-reportcard
            • Vl-design-reportcard
            • Vl-extend-reportcard
            • Vl-reportcard-revive-invalid-warnings
            • Vl-clean-reportcard
            • Vl-reportcard-equiv
            • Vl-print-reportcard
            • Vl-reportcard-to-string
            • Vl-keep-from-reportcard
            • Vl-reportcard-types
            • Vl-reportcardkey-p
          • 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-reportcard

A (typically fast) alist associating names to warnings.

A report card associates vl-reportcardkey-ps to lists of warnings. Typically the keys are the names of top-level design elements (modules, packages, interfaces, ...). However, as a special case for warnings about top-level design elements that aren't in any container, e.g., top-level parameters or functions, we also allow :design as a key.

There are two common uses for report cards.

  1. When transforming modules, we sometimes want to add a warning to some other module that is "far away," i.e., not the module we're currently rewriting. It would be somewhat awkward to iteratively update the vl-modulelist-p, so instead we might create a report card that associates target module names with the new warnings we want to add to them. The function vl-apply-reportcard can then be used to add these warnings to a design.
  2. Report cards can be useful when we want to print the warnings for a bunch of modules. Depending on the context, we might want to associate either the elaborated (unparameterized) names of modules, or their original names, to their related warnings.

Subtopics

Vl-reportcard-p
Recognizer for vl-reportcard.
Vl-apply-reportcard
Update a design to include any warnings from a vl-reportcard-p.
Vl-reportcard-fix
(vl-reportcard-fix x) is an ACL2::fty alist fixing function that follows the fix-keys strategy.
Vl-extend-reportcard-list
Add a list of warnings to a vl-reportcard-p.
Vl-design-origname-reportcard
Constructs a vl-reportcard-p for a design in terms of original design element names.
Vl-design-reportcard
Constructs a vl-reportcard-p for a design.
Vl-extend-reportcard
Add a single warning to a vl-reportcard-p.
Vl-reportcard-revive-invalid-warnings
Convert any warnings about invalid keys into warnings about the top-level design.
Vl-clean-reportcard
Shrink a vl-reportcard-p and cleans all of its warning lists with vl-clean-warnings.
Vl-reportcard-equiv
Basic equivalence relation for vl-reportcard structures.
Vl-print-reportcard
Pretty-print a vl-reportcard-p.
Vl-reportcard-to-string
Pretty-print a vl-reportcard-p into a string.
Vl-keep-from-reportcard
Filter a reportcard to only keep the warnings of certain types.
Vl-reportcard-types
Collect all types of warnings found in a reportcard.
Vl-reportcardkey-p