• 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
            • Vl-expr-expand-function-calls
            • Vl-expand-function-call
            • Vl-module-expand-functions
            • Vl-modulelist-expand-functions
            • Vl-check-bad-funcalls
            • Vl-funtemplate
              • Vl-funtemplate-p
              • Vl-funtemplate-fix
              • Vl-funtemplate-equiv
              • Make-vl-funtemplate
              • Vl-funtemplate->locals
              • Vl-funtemplate->inputs
              • Vl-funtemplate->assigns
              • Change-vl-funtemplate
              • Vl-funtemplate->out
              • Vl-funtemplate->name
            • Vl-funbody-to-assignments
            • Vl-assignlist->rhses
            • Vl-fundecl-expand-params
            • Vl-fun-stmt-okp
            • Vl-fundecllist-expand-params
            • Vl-remove-fake-function-vardecls
            • Vl-design-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
          • 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
  • Expand-functions

Vl-funtemplate

Function expansion templates, the intermediate representation of functions we use while inlining function calls.

This is a product type introduced by defprod.

Fields
name — stringp
inputs — vl-vardecllist
locals — vl-vardecllist
out — vl-vardecl
assigns — vl-assignlist

For each of the module's functions, we generate a template that will allow us to expand calls of the function. Each template has the same name as the function, but all of its inputs and var declarations have been turned into net declarations (the inputs and locals, respectively), and we have added a net declaration for the function's return value (out). The function's body is converted into assigns, an ordinary vl-assignlist-p, and we assume that these assignments are well-formed in the sense of vl-fun-assignorder-okp.

Why do we bother introducing these templates at all? One nice thing about them is that there is a certain amount of "static" processing that needs to be done on each function declaration (e.g., we need to do well-formedness checking and extract its body into assignments) and it is somewhat efficient to do this processing once, in the creation of templates, rather than each time we want to expand a call of the function.

But a more important reason is that it allows us to support functions that call other functions in a straightforward way. BOZO: previously we claimed that ``in vl-flatten-funtemplates we use our ordinary function-expansion code to expand any function calls within function templates, so that when we expand functions throughout the rest of the module we only need one pass.'' but that function no longer exists and Jared does not remember whether we changed how this worked.

Subtopics

Vl-funtemplate-p
Recognizer for vl-funtemplate structures.
Vl-funtemplate-fix
Fixing function for vl-funtemplate structures.
Vl-funtemplate-equiv
Basic equivalence relation for vl-funtemplate structures.
Make-vl-funtemplate
Basic constructor macro for vl-funtemplate structures.
Vl-funtemplate->locals
Get the locals field from a vl-funtemplate.
Vl-funtemplate->inputs
Get the inputs field from a vl-funtemplate.
Vl-funtemplate->assigns
Get the assigns field from a vl-funtemplate.
Change-vl-funtemplate
Modifying constructor for vl-funtemplate structures.
Vl-funtemplate->out
Get the out field from a vl-funtemplate.
Vl-funtemplate->name
Get the name field from a vl-funtemplate.