		Search-engine friendly clone of the ACL2 documentation.

Unparameterization

Vl-unparam-signature

An unparam signature describes a module/parameter combo that needs to be created.

This is a product type introduced by defprod.

Fields

modname — stringp
newname — stringp
final-params — vl-paramdecllist: paramdecls with constant, overridden values
final-ports — vl-portlist: interfaceports with final interface names

Note on the final-params: These are relative to the scope of some instantiating module. That doesn't matter for value parameters, because they must all be resolved to literal expressions anyway. Type parameters should be resolved such that the usertype names are vestigial and the relevant definition for each usertype is stored in the res field.

Subtopics

Vl-unparam-signature-fix: Fixing function for vl-unparam-signature structures.
Vl-unparam-signature-equiv: Basic equivalence relation for vl-unparam-signature structures.
Make-vl-unparam-signature: Basic constructor macro for vl-unparam-signature structures.
Vl-unparam-signature->final-params: Get the final-params field from a vl-unparam-signature.
Vl-unparam-signature->final-ports: Get the final-ports field from a vl-unparam-signature.
Vl-unparam-signature->newname: Get the newname field from a vl-unparam-signature.
Vl-unparam-signature->modname: Get the modname field from a vl-unparam-signature.
Change-vl-unparam-signature: Modifying constructor for vl-unparam-signature structures.
Vl-unparam-signature-p: Recognizer for vl-unparam-signature structures.