		Search-engine friendly clone of the ACL2 documentation.

Expressions-and-datatypes

Vl-atts

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 value (e.g., baz above), or can have the form key = value. The keys are always identifiers, and the values (if provided) are expressions. Both Verilog-2005 and SystemVerilog-2012 agree that an attribute with no explicit value is to be treated as having value 1.

Representation

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 nil instead.

Function: vl-atts-p

(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))))))

Size/Types of Attribute Values

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 bit, and that otherwise its type is the (presumably self-determined) type of the expression. But this is not really an adequate spec. Consider for instance an attribute like:

(* foo = a + b *)

Since attributes live in their own namespace, it isn't clear what a and b refer to here. For instance, are they wires in this module, or perhaps global values that are known by the Verilog tool. It doesn't seem at all clear what the type or size of such an expression is supposed to be.

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.

Nesting Attributes

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.

Redundant and Conflicting Attributes

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 below should be 5:

(* 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 vl-atts-p structures that are free from duplicate keys, and where the entry for each attribute corresponds to the last occurrence of it; see vl-parse-0+-attribute-instances.

Internally we make no such restriction. We treat vl-atts-p structures as ordinary alists.

Internal Use of Attributes by VL

Certain VL transformations may occasionally add attributes throughout modules. For instance, the make-implicit-wires transformation will add VL_IMPLICIT attributes to the wire declarations that added implicitly.

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 VL_. In practice, we may sometimes forget to follow this rule.

Subtopics

Vl-atts-p: Recognizer for vl-atts.
Vl-atts-equiv: Basic equivalence relation for vl-atts structures.
Vl-atts-fix: (vl-atts-fix x) is an fty alist fixing function that follows the fix-keys strategy.