Representation of (* foo = 3, bar *) style attributes.
Verilog-2005 and SystemVerilog-2012 allow many constructs, (e.g., module instances, wire declarations, assignments, subexpressions, and so on) to be annotated with attributes.
Each individual attribute can either be a single key with no
We represent attributes as alists mapping names to their values.
We use ordinary ACL2 strings to represent the keys. These strings
are typically honsed to improve memory sharing. Each explicit value
is represented by an ordinary vl-expr-p, and keys with no
values are bound to
(defun vl-atts-p (x) (declare (xargs :guard t)) (let ((__function__ 'vl-atts-p)) (declare (ignorable __function__)) (if (atom x) (eq x nil) (and (consp (car x)) (stringp (caar x)) (vl-maybe-expr-p (cdar x)) (vl-atts-p (cdr x))))))
Verilog-2005 doesn't say anything about the types of attribute
expressions. SystemVerilog-2012 says (Section 5.12) that the type
of an attribute with no value is
(* foo = a + b *)
Since attributes live in their own namespace, it isn't clear what
Well, no matter. Attributes are not used for much and if their sizes and types aren't well specified, that's not necessarily any kind of problem. We generally expect to be able to ignore attributes and do not expect to need to size them or determine their types.
Note that both Verilog-2005 and SystemVerilog-2012 prohibit the nesting of attributes. That is, expressions like the following are not allowed:
(* foo = a + (* bar *) b *)
VL's parser enforces this restriction and will not allow expressions to have nested attributes; see vl-parse-0+-attribute-instances. However, we make no such restriction internally—our vl-expr-p structures can have attributes nested to any arbitrary depth.
When the same attribute name is given repeatedly, both
Verilog-2005 and SystemVerilog-2012 agree that the last occurrences
of the attribute should be used. That is, the value of
(* foo = 1, foo = 5 *) assign w = a + b;
VL's parser properly handles this case. It issues warnings when
duplicate attributes are used, and always produces
Internally we make no such restriction. We treat
Certain VL transformations may occasionally add attributes
throughout modules. For instance, the make-implicit-wires
transformation will add
We once tried to record the different kinds of attributes that VL
used here, but that list became quickly out of date as we forgot to
maintain it, so we no longer try to do this. As a general rule,
attributes added by VL should be prefixed with