Vl-id
Representation for simple identifiers.
This is a product type introduced by defprod.
Fields
- name — stringp
- This identifier's name. Our structure only requires that this is an
ACL2 string; in practice the name can include any character
besides whitespace and should be non-empty. Note that for escaped
identifiers like \foo , the \ and trailing space are not
included in the name; see vl-read-escaped-identifier.
vl-id-p objects are used to represent identifiers used in
expressions which might be the names of wires, ports, parameters, registers,
and so on.
A wonderful feature of our representation vl-id-p atoms are guaranteed
to not be part of any hierarchical identifier, nor are they the names of
functions or system functions. See the discussion in vl-hidpiece-p for
more information.
Like vl-constint-ps, we automatically create these structures with
hons. This seems quite nice, since the same names may be used many
times throughout all the expressions in a design.
Subtopics
- Vl-id-fix
- Fixing function for vl-id structures.
- Vl-id-p
- Recognizer for vl-id structures.
- Vl-id-equiv
- Basic equivalence relation for vl-id structures.
- Make-vl-id
- Basic constructor macro for vl-id structures.
- Change-vl-id
- Modifying constructor for vl-id structures.
- Vl-id->name
- Get the name field from a vl-id.
