• 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
        • Transforms
          • Unparameterization
            • Vl-unparameterize-flow
              • Vl-genblob-resolve
            • Vl-unparam-inst
            • Vl-unparam-add-to-ledger
            • Vl-scopeinfo-resolve-params
            • Vl-scope-finalize-params
            • Vl-create-unparameterized-interface
            • Vl-create-unparameterized-module
            • Vl-unparam-actualkeys
            • Vl-make-paramdecloverrides
            • Vl-unparam-class
            • Vl-unparam-instlist
            • Vl-create-unparameterized-class
            • Vl-add-lost-interface-warnings
            • Vl-add-lost-module-warnings
            • Vl-unparam-classlist
            • Vl-interfacelist->orignames
            • Vl-user-signature
            • Vl-interfaceport-default-signature
            • Vl-modulelist->orignames
            • Vl-plainarglist-update-ifports
            • Vl-portlist-interface-signatures
            • Vl-user-signatures
            • Vl-plainarg-update-ifports
            • Vl-unparam-inst->instkey
            • Vl-toplevel-signatures
            • Vl-unparam-basename
            • Vl-genblob-resolve-rejoin-scopeitems
            • Vl-gencase-some-match
            • Vl-gencase-match
            • Vl-package-elaborate
            • Vl-unparam-signature
            • Vl-unparam-ledger
            • Vl-packagelist-elaborate
            • Vl-design-elaborate
            • Vl-unparam-actualkey
            • Vl-make-paramdecloverrides-named
            • Vl-unparameterize-main
            • Vl-recover-modules-lost-from-elaboration
            • Vl-finish-unparameterized-interface
            • Vl-paramdecl-set-default
            • Vl-genblob-rejoin-scopeitems
            • Vl-finish-unparameterized-interfaces
            • Vl-unparam-instkey
            • Vl-finish-unparameterized-module
            • Vl-finish-unparameterized-class
            • Vl-finish-unparameterized-modules
            • Vl-finish-unparameterized-classes
            • Vl-genblob-split-scopeitems
            • Vl-user-paramsettings-for-top-names
            • Vl-string/int-alist-to-namedargs
            • Vl-add-lost-interface-warning
            • Vl-unparam-basename-exprstring
            • Vl-add-lost-module-warning
            • Vl-paramdecllist-remove-defaults
            • Vl-ifport-alist
            • Vl-paramdecl-remove-default
            • Vl-ifportexpr->name
            • Vl-paramdecllist-all-localp
            • Vl-unparam-instkeymap
            • Vl-unparam-donelist
            • Vl-unparam-instkeylist
          • Elaborate
          • Addnames
          • Annotate
          • Clean-warnings
          • Eliminitial
          • Custom-transform-hooks
          • Problem-modules
      • X86isa
      • Svl
      • Rtl
    • Software-verification
    • Math
    • Testing-utilities
  • Unparameterization

Vl-unparameterize-flow

How the heck does unparameterization/elaboration work?

Basic Idea

Our algorithm processes a list of signatures that specify what modules we want to create with what parameters.

We start from the top-level modules. Any module that is never instantiated is assumed to be a top-level module, and we'll use its default parameters (if it has parameters). The initial signature list has the top level modules, associated with their default parameters.

Recursively, to create a module with a set of parameters, we apply vl-genblob-resolve, which substitutes the parameter values everywhere they're needed, and then examines the module instances. For each module instance that has parameters, we add to our list of signatures the needed module, and replace that instance with a parameter-free instance of that module. (The function that does this on each instance is vl-unparam-inst.)

When we're done with the current module, we recur on the list of signatures we accumulated; when we're done with those, we've completely unparameterized the module and all of its dependencies. This is what vl-unparameterize-main does.

Tricky Parts

Scoping

When we unparameterize a module instance like

module supermod ; 
  ...
  foo #(.size(64), .kind(foo_t)) myinst (...) ;
endmodule

The actual parameter arguments (64, foo_t) need to be resolved in the scope of supermod. But then, we are going to create a signature for specializing foo that binds size to 64, kind to foo_t. What scope are these bindings relative to? Our answer is: they need to be independent of scope.

To accomplish this, for value parameters (e.g. size) we insist that the each value gets resolved to a literal (e.g., 64, "foo", etc.), and such literals are of course independent of scope. If we can't resolve a parameter, e.g., you write .size(a+b) and we don't know what a/b are, then we are just going to fail to unparameterize this.

For type parameters the situation is harder. We can't simply replace a named type like foo_t with its definition (recursively), because various rules in SystemVerilog prohibit that, especially pertaining to signedness.

(Digression: e.g., consider the type foo_t:

typedef logic signed [3:0] [5:0] signedarr_t;
typedef signedarr_t [7:0] foo_t;

You can't define foo_t without a subsidiary typedef, because there's no way to directly express a multidimensional array of which some inner dimension is signed.)

So what to do? Our approach is to annotate the named type (see vl-usertype) with its definition as the res field of the vl-usertype; any usertypes referenced in the res field also are similarly annotated with their definitions, recursively. This is similar to expressing it as one monolithically defined type, but we can tell which parts are named, which lets us be faithful to the awkward semantics. However, the names are basically vestigial -- we don't generally know what scope they're from, so it doesn't make sense to look them up anywhere!

In summary: the actual values for type parameters in our signatures are scope agnostic in the sense that we know we can't trust their names, and in the sense that we don't need their names to know anything about them, because we have these res fields to use instead.

Sharing Isomorphically Parameterized Modules

If a module is instantiated twice with the same parameters, we don't want to create two different unparameterized versions of that module. However, we need to be careful not to share a definition for two modules whose parameters look the same, but are actually different. E.g., a module with a type parameter may be instantiated twice with two types that have the same name, but refer to different definitions because they occur in different scopes.

To keep track of this, we create a key for each module instantiation. Two module instantiations should produce the same key only if they are instantiations of the same module, all value parameters resolve to the same values, and all type parameters are the same up to and including the scope in which any usertypes are defined. To track which scope is which, we use vl-scopestack->hashkey, which reduces a scopestack to a hierarchy of names.

Indirect Parameterization Via Interface Ports

If an interface is instantiated with a set of parameters and then passed to a module instance, that instance differs from a similar instance that is passed an interface instantiated with different parameters, even if the parameters two the two instances are the same (or there aren't any parameters).

Subtopics

Vl-genblob-resolve
Substitutes the parameter values given by ledger throughout the given object.