		Search-engine friendly clone of the ACL2 documentation.

Expressions

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.

This is not really an adequate spec. Consider for instance an attribute like:

(* foo = a + b *)

Attributes live in their own namespace and are generally not very well-specified. 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. For VL's part, our sizing code simply ignores attributes and does not try to determine their sizes and types at all.

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.

Internally we make no such restriction. 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

VL transformations occasionally add attributes throughout modules. As a couple of examples:

The VL_HANDS_OFF attribute is used to say that a module is somehow special and should not be modified by transformations.
VL may add VL_ORIG_EXPR annotations to remember the "original" versions of expressions, before any rewriting or other simplification has taken place; these annotations can be useful in error messages.

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 ACL2::fty alist fixing function that follows the fix-keys strategy.