• 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
        • Getting-started
        • Utilities
        • Printer
        • Kit
        • Mlib
          • Scopestack
          • Hid-tools
          • Filtering-by-name
          • Vl-interface-mocktype
          • Stripping-functions
            • Vl-function-specialization-map-strip
            • Vl-portdecl-or-blockitem-list-strip
            • Vl-maybe-delayoreventcontrol-strip
            • Vl-portdecl-or-blockitem-strip
            • Vl-fundecl-strip
            • Vl-function-specialization-strip
            • Vl-taskdecl-strip
            • Vl-repeateventcontrol-strip
            • Vl-delayoreventcontrol-strip
            • Vl-sequence-strip
            • Vl-property-strip
            • Vl-paramtype-strip
            • Vl-modinst-strip
            • Vl-maybe-gatedelay-strip
            • Vl-gateinst-strip
            • Vl-assign-strip
            • Vl-vardecl-strip
            • Vl-propspec-strip
            • Vl-propport-strip
            • Vl-portdecl-strip
            • Vl-paramdecl-strip
            • Vl-maybe-exprdist-strip
            • Vl-letdecl-strip
            • Vl-initial-strip
            • Vl-blockitem-strip
            • Vl-arguments-strip
            • Vl-always-strip
            • Vl-alias-strip
            • Vl-vardecllist-strip
            • Vl-typedeflist-strip
            • Vl-repetition-strip
            • Vl-propportlist-strip
            • Vl-portdecllist-strip
            • Vl-plainarglist-strip
            • Vl-paramdecllist-strip
            • Vl-namedarglist-strip
            • Vl-modinstlist-strip
            • Vl-maybe-rhs-strip
            • Vl-gateinstlist-strip
            • Vl-gatedelay-strip
            • Vl-final-strip
            • Vl-exprdistlist-strip
            • Vl-eventcontrol-strip
            • Vl-distitem-strip
            • Vl-delaycontrol-strip
            • Vl-blockitemlist-strip
            • Vl-typedef-strip
            • Vl-rhs-strip
            • Vl-plainarg-strip
            • Vl-namedarg-strip
            • Vl-importlist-strip
            • Vl-import-strip
            • Vl-exprdist-strip
            • Vl-distlist-strip
            • Vl-assignlist-strip
            • Vl-expr-strip
          • Genblob
          • Expr-tools
          • Extract-vl-types
          • Hierarchy
          • Range-tools
          • Finding-by-name
          • Stmt-tools
          • Modnamespace
          • Flat-warnings
          • Reordering-by-name
          • Datatype-tools
          • Syscalls
          • Allexprs
          • Lvalues
          • Port-tools
        • Transforms
      • X86isa
      • Svl
      • Rtl
    • Software-verification
    • Math
    • Testing-utilities
  • Mlib

Stripping-functions

Functions for throwing away attributes, widths, locations, etc., so that expressions and module elements can be compared using equal.

In many basic kinds of vl-lint checks and well-formedness checking, it is useful to be able to compare module elements using equal. But equal can report that elements are different because of, e.g., their location information, widths and other annotations on expressions, and other kinds of semantically irrelevant attributes.

These stripping functions attempt to strip away these kind of semantically irrelevant components of module elements, so that they can be compared with equal. For instance, we replace all locations with *vl-fakeloc*, replace all attributes with nil, etc.

Exactly what we throw away depends on the kind of module element. In some cases this may not be exactly what you want. See the individual functions for details.

Subtopics

Vl-function-specialization-map-strip
Vl-portdecl-or-blockitem-list-strip
Vl-maybe-delayoreventcontrol-strip
Vl-portdecl-or-blockitem-strip
Vl-fundecl-strip
Vl-function-specialization-strip
Vl-taskdecl-strip
Vl-repeateventcontrol-strip
Vl-delayoreventcontrol-strip
Vl-sequence-strip
Vl-property-strip
Vl-paramtype-strip
Vl-modinst-strip
Vl-maybe-gatedelay-strip
Vl-gateinst-strip
Vl-assign-strip
Vl-vardecl-strip
Vl-propspec-strip
Vl-propport-strip
Vl-portdecl-strip
Vl-paramdecl-strip
Vl-maybe-exprdist-strip
Vl-letdecl-strip
Vl-initial-strip
Vl-blockitem-strip
Vl-arguments-strip
Vl-always-strip
Vl-alias-strip
Vl-vardecllist-strip
Vl-typedeflist-strip
Vl-repetition-strip
Vl-propportlist-strip
Vl-portdecllist-strip
Vl-plainarglist-strip
Vl-paramdecllist-strip
Vl-namedarglist-strip
Vl-modinstlist-strip
Vl-maybe-rhs-strip
Vl-gateinstlist-strip
Vl-gatedelay-strip
Vl-final-strip
Vl-exprdistlist-strip
Vl-eventcontrol-strip
Vl-distitem-strip
Vl-delaycontrol-strip
Vl-blockitemlist-strip
Vl-typedef-strip
Vl-rhs-strip
Vl-plainarg-strip
Vl-namedarg-strip
Vl-importlist-strip
Vl-import-strip
Vl-exprdist-strip
Vl-distlist-strip
Vl-assignlist-strip
Vl-expr-strip
Strip an expression, removing attributes and code locations.