		Search-engine friendly clone of the ACL2 documentation.

Vl-paramdecl

Representation of a single parameter or localparam declaration.

This is a product type introduced by defprod.

name — stringp: Name of the parameter being declared.
localp — booleanp: True for localparam declarations, nil for parameter declarations. The difference is apparently that localparams such as TWICE_WIDTH below cannot be overridden from outside the module, except insofar as that they depend upon non-local parameters. (These localparam declarations are a way to introduce named constants without polluting the `define namespace.)
type — vl-paramtype: Indicates the type and default value of the parameter, and also distinguishes between implicit/explicit value parameters and type parameters.
atts — vl-atts: Any attributes associated with this declaration.
loc — vl-location: Where the declaration was found in the source code.

Some examples of parameter declarations include:

module mymod (a, b, ...) ;
  parameter WIDTH = 3;
  localparam TWICE_WIDTH = 2 * WIDTH;
  ...
endmodule

Vl-paramtype: Representation of the kind and default for a parameter declaration.
Vl-paramdecl-p: Recognizer for vl-paramdecl structures.
Vl-paramdecl-fix: Fixing function for vl-paramdecl structures.
Vl-paramdecl-equiv: Basic equivalence relation for vl-paramdecl structures.
Make-vl-paramdecl: Basic constructor macro for vl-paramdecl structures.
Change-vl-paramdecl: Modifying constructor for vl-paramdecl structures.
Vl-paramdecl->name: Get the name field from a vl-paramdecl.
Vl-paramdecl->localp: Get the localp field from a vl-paramdecl.
Vl-paramdecl->type: Get the type field from a vl-paramdecl.
Vl-paramdecl->loc: Get the loc field from a vl-paramdecl.
Vl-paramdecl->atts: Get the atts field from a vl-paramdecl.