• 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-blamealist
            • Vl-design-propagate-errors
            • Vl-blame-alist-to-reportcard
            • Vl-blame-alist
            • Vl-design-zombies
            • Vl-blamealist-count
          • 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-simplify

Propagating-errors

The error handling strategy used by vl-simplify.

As described in warnings, our transforms can sometimes run into severe problems, e.g., we might run into an instance of an undefined module. In this case, the transform should typically extend the module with a fatal warning.

In the context of vl-simplify, we generally want to throw away any design elements (e.g., modules, packages, etc.) that have fatal errors, so that we only produce a formal model of whatever part of the design is well-formed and supported.

For various reasons, it's a good idea to throw away any these bad parts of the design as early as possible. The main reason for this is that it easier to identify the root cause of the problem. Problems tend to snowball. It's much better to see a single fatal error from the first transform that hit a problem than to see dozens errors from different transforms that all have the same underlying cause. Throwing out modules early also helps to improve performance by cutting down the design; there's no point in further transforming stuff we're going to throw away, anyway.

On the other hand, we can't really just throw bad parts of the design away. We at least need some way to see what went wrong, so that we can debug it.

Our basic strategy for dealing with this, in vl-simplify at least, is to imagine two designs, good and bad. Initially, we put all of the design elements into the good design, and the bad design is empty. We always only try to transform the good design, and afterward we can move any design elements that had errors into the bad design.

Moving things into the bad design is tricky because design elements do not exist in isolation. When, for instance, some module M has an error, we would ideally like to remove not only M but also all modules that transitively depend on M. Moreover, we also want to make sure that any modules that are killed off in this transitive way get extended with some kind of warning that explains why the module is being removed.

Because this is so complicated, we bundle up the process into a function, vl-design-propagate-errors, which is intended to move any design elements that (transitively) have errors from good to bad.

Subtopics

Vl-blamealist
A record of which submodules are to blame for transitive failures to translate modules.
Vl-design-propagate-errors
Top-level function for propagating-errors. We identify any faulty design elements in a good design and move them into a bad design.
Vl-blame-alist-to-reportcard
Construct a vl-reportcard of fatal warnings for a vl-blamealist-p.
Vl-blame-alist
Build an alist describing which modules are really to blame for their dependents being thrown away.
Vl-design-zombies
Collect the names of design elements with fatal warnings.
Vl-blamealist-count