• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
        • Warnings
        • Primitives
        • Use-set
        • Syntax
        • Getting-started
        • Utilities
        • Loader
        • Transforms
          • Expression-sizing
          • Occform
          • Oprewrite
          • Expand-functions
          • Delayredux
          • Unparameterization
          • Caseelim
          • Split
          • Selresolve
          • Weirdint-elim
          • Vl-delta
          • Replicate-insts
          • Rangeresolve
          • Propagate
          • Clean-selects
          • Clean-params
          • Blankargs
          • Inline-mods
          • Expr-simp
          • Trunc
          • Always-top
          • Gatesplit
          • Gate-elim
          • Expression-optimization
          • Elim-supplies
          • Wildelim
          • Drop-blankports
          • Clean-warnings
          • Addinstnames
          • Custom-transform-hooks
          • Annotate
            • Make-implicit-wires
            • Resolve-indexing
            • Origexprs
              • Vl-namedparamvaluelist-origexprs
              • Vl-paramvaluelist-origexprs
              • Vl-plainarglist-origexprs
              • Vl-namedarglist-origexprs
              • Vl-gateinstlist-origexprs
              • Vl-modinstlist-origexprs
              • Vl-initiallist-origexprs
              • Vl-modulelist-origexprs
              • Vl-evatomlist-origexprs
              • Vl-assignlist-origexprs
              • Vl-alwayslist-origexprs
              • Vl-rangelist-origexprs
              • Vl-expr-origexprs
              • Vl-pp-origexpr
              • Vl-maybe-delayoreventcontrol-origexprs
              • Vl-repeateventcontrol-origexprs
              • Vl-delayoreventcontrol-origexprs
              • Vl-namedparamvalue-origexprs
              • Vl-module-origexprs
              • Vl-maybe-paramvalue-origexprs
              • Vl-maybe-gatedelay-origexprs
              • Vl-eventcontrol-origexprs
              • Vl-paramvalue-origexprs
              • Vl-paramargs-origexprs
              • Vl-nonatom->original-operator
              • Vl-modinst-origexprs
              • Vl-maybe-range-origexprs
              • Vl-gateinst-origexprs
              • Vl-gatedelay-origexprs
              • Vl-delaycontrol-origexprs
              • Vl-arguments-origexprs
              • Vl-plainarg-origexprs
              • Vl-namedarg-origexprs
              • Vl-maybe-expr-origexprs
              • Vl-initial-origexprs
              • Vl-assign-origexprs
              • Vl-range-origexprs
              • Vl-evatom-origexprs
              • Vl-design-origexprs
              • Vl-always-origexprs
            • Argresolve
            • Portdecl-sign
            • Designwires
            • Udp-elim
            • Vl-annotate-design
          • Latchcode
          • Elim-unused-vars
          • Problem-modules
        • Lint
        • Mlib
        • Server
        • Kit
        • Printer
        • Esim-vl
        • Well-formedness
      • Sv
      • Fgl
      • Vwsim
      • Vl
      • X86isa
      • Svl
      • Rtl
    • Software-verification
    • Math
    • Testing-utilities
  • Annotate

Origexprs

Add VL_ORIG_EXPR annotations to some expressions.

In this transformation, we annotate many expressions with their VL_ORIG_EXPR attribute (see vl-atts-p). The idea is to associate each expression with its "original version," as it was read from the source file, before any simplification has taken place.

Why do we want to do this? Transformations like oprewrite can, for instance, simplify expressions such as a == b into &(a ~^ b), and these reduced expressions may not correspond to anything the logic designer actually wrote in the source file. So, if we want to print an error message or warning about this expression, we would prefer to write it as a == b instead. By saving the original version of the expression as an attribute, we can easily remember where the expression came from.

The core function, vl-expr-origexprs, is rather cute. As we encounter each expression, say x, we just cons together a new expression with the same fields, except that we add an VL_ORIG_EXPR attribute whose value is x itself. This is really quite fast, and we do not need to do any pretty-printing ahead of time.

In error messages, we typically use this attribute implicitly, by calling vl-pps-origexpr.

Subtopics

Vl-namedparamvaluelist-origexprs
Add VL_ORIG_EXPR annotations throughout a vl-namedparamvaluelist-p
Vl-paramvaluelist-origexprs
Add VL_ORIG_EXPR annotations throughout a vl-paramvaluelist-p
Vl-plainarglist-origexprs
Add VL_ORIG_EXPR annotations throughout a vl-plainarglist-p
Vl-namedarglist-origexprs
Add VL_ORIG_EXPR annotations throughout a vl-namedarglist-p
Vl-gateinstlist-origexprs
Add VL_ORIG_EXPR annotations throughout a vl-gateinstlist-p
Vl-modinstlist-origexprs
Add VL_ORIG_EXPR annotations throughout a vl-modinstlist-p
Vl-initiallist-origexprs
Add VL_ORIG_EXPR annotations throughout a vl-initiallist-p
Vl-modulelist-origexprs
Add VL_ORIG_EXPR annotations throughout a vl-modulelist-p
Vl-evatomlist-origexprs
Add VL_ORIG_EXPR annotations throughout a vl-evatomlist-p
Vl-assignlist-origexprs
Add VL_ORIG_EXPR annotations throughout a vl-assignlist-p
Vl-alwayslist-origexprs
Add VL_ORIG_EXPR annotations throughout a vl-alwayslist-p
Vl-rangelist-origexprs
Add VL_ORIG_EXPR annotations throughout a vl-rangelist-p
Vl-expr-origexprs
Recursively annotate an expression with VL_ORIG_EXPR attributes.
Vl-pp-origexpr
Pretty-print the "original," un-transformed version of an expression.
Vl-maybe-delayoreventcontrol-origexprs
Add VL_ORIG_EXPR annotations throughout a vl-maybe-delayoreventcontrol-p
Vl-repeateventcontrol-origexprs
Add VL_ORIG_EXPR annotations throughout a vl-repeateventcontrol-p
Vl-delayoreventcontrol-origexprs
Add VL_ORIG_EXPR annotations throughout a vl-delayoreventcontrol-p
Vl-namedparamvalue-origexprs
Add VL_ORIG_EXPR annotations throughout a vl-namedparamvalue-p
Vl-module-origexprs
Add VL_ORIG_EXPR annotations throughout a vl-module-p
Vl-maybe-paramvalue-origexprs
Add VL_ORIG_EXPR annotations throughout a vl-maybe-paramvalue-p
Vl-maybe-gatedelay-origexprs
Add VL_ORIG_EXPR annotations throughout a vl-maybe-gatedelay-p
Vl-eventcontrol-origexprs
Add VL_ORIG_EXPR annotations throughout a vl-eventcontrol-p
Vl-paramvalue-origexprs
Add VL_ORIG_EXPR annotations throughout a vl-paramvalue-p
Vl-paramargs-origexprs
Add VL_ORIG_EXPR annotations throughout a vl-paramargs-p
Vl-nonatom->original-operator
Get the original operator from a non-atomic expression.
Vl-modinst-origexprs
Add VL_ORIG_EXPR annotations throughout a vl-modinst-p
Vl-maybe-range-origexprs
Add VL_ORIG_EXPR annotations throughout a vl-maybe-range-p
Vl-gateinst-origexprs
Add VL_ORIG_EXPR annotations throughout a vl-gateinst-p
Vl-gatedelay-origexprs
Add VL_ORIG_EXPR annotations throughout a vl-gatedelay-p
Vl-delaycontrol-origexprs
Add VL_ORIG_EXPR annotations throughout a vl-delaycontrol-p
Vl-arguments-origexprs
Add VL_ORIG_EXPR annotations throughout a vl-arguments-p
Vl-plainarg-origexprs
Add VL_ORIG_EXPR annotations throughout a vl-plainarg-p
Vl-namedarg-origexprs
Add VL_ORIG_EXPR annotations throughout a vl-namedarg-p
Vl-maybe-expr-origexprs
Add VL_ORIG_EXPR annotations throughout a vl-maybe-expr-p
Vl-initial-origexprs
Add VL_ORIG_EXPR annotations throughout a vl-initial-p
Vl-assign-origexprs
Add VL_ORIG_EXPR annotations throughout a vl-assign-p
Vl-range-origexprs
Add VL_ORIG_EXPR annotations throughout a vl-range-p
Vl-evatom-origexprs
Add VL_ORIG_EXPR annotations throughout a vl-evatom-p
Vl-design-origexprs
Top-level origexprs transform.
Vl-always-origexprs
Add VL_ORIG_EXPR annotations throughout a vl-always-p