		Search-engine friendly clone of the ACL2 documentation.

Expressions

vl-ops-table

Table binding valid operators to their vl-opinfo structures.

The constant *vl-ops-table* defines the valid operators in our expression representation. It is preferred not to access this table directly, but rather to use vl-op-p and vl-op-arity.

Here is how we represent the various Verilog operators:

Basic Unary Operators (arity 1)

+ becomes :vl-unary-plus
- becomes :vl-unary-minus
! becomes :vl-unary-lognot
~ becomes :vl-unary-bitnot
& becomes :vl-unary-bitand
~& becomes :vl-unary-nand
| becomes :vl-unary-bitor
~| becomes :vl-unary-nor
^ becomes :vl-unary-xor
^~ or ~^ becomes :vl-unary-xnor
++a becomes :vl-unary-preinc
a++ becomes :vl-unary-postinc
--a becomes :vl-unary-predec
a-- becomes :vl-unary-postdec

Basic Binary Operators (arity 2)

+ becomes :vl-binary-plus
- becomes :vl-binary-minus
* becomes :vl-binary-times
/ becomes :vl-binary-div
% becomes :vl-binary-rem
== becomes :vl-binary-eq
!= becomes :vl-binary-neq
=== becomes :vl-binary-ceq
!== becomes :vl-binary-cne
&& becomes :vl-binary-logand
|| becomes :vl-binary-logor
** becomes :vl-binary-power
< becomes :vl-binary-lt
<= becomes :vl-binary-lte
> becomes :vl-binary-gt
>= becomes :vl-binary-gte
& becomes :vl-binary-bitand
| becomes :vl-binary-bitor
^ becomes :vl-binary-xor
^~ or ~^ becomes :vl-binary-xnor
>> becomes :vl-binary-shr
<< becomes :vl-binary-shl
>>> becomes :vl-binary-ashr
<<< becomes :vl-binary-ashl

Assignments within Expressions (SystemVerilog)

(a = b) becomes :vl-binary-assign
(a += b) becomes :vl-binary-plusassign
(a -= b) becomes :vl-binary-minusassign
(a *= b) becomes :vl-binary-timesassign
(a /= b) becomes :vl-binary-divassign
(a %= b) becomes :vl-binary-remassign
(a &= b) becomes :vl-binary-andassign
(a |= b) becomes :vl-binary-orassign
(a ^= b) becomes :vl-binary-xorassign
(a <<= b) becomes :vl-binary-shlassign
(a >>= b) becomes :vl-binary-shrassign
(a <<<= b) becomes :vl-binary-ashlassign
(a >>>= b) becomes :vl-binary-ashrassign

Basic Ternary Operators (arity 3)

a ? b : c becomes :vl-qmark (conditional operator)
a : b : c becomes :vl-mintypmax (min/typ/max delay operator)

Selection Operators

foo[1] initially becomes :vl-index. Later these are changed to :vl-bitselect if they are determined to be bitselects (i.e., applied to a simple vector type).
foo[3 : 1] becomes :vl-select-colon (arity 3), similarly changed to vl-partselect-colon if applied to a simple vector.
foo[3 +: 1] becomes :vl-select-pluscolon (arity 3), similarly changed to vl-partselect-pluscolon if applied to a simple vector.
foo[3 -: 1] becomes :vl-select-minuscolon (arity 3), similarly changed to vl-partselect-minuscolon if applied to a simple vector.

Note that upon parsing, there are no :vl-bitselect or :vl-partselect-* operators; these must be introduced by the resolve-indexing transform.

Concatenation and Replication Operators

{1, 2, 3, ...} becomes :vl-concat (arity nil)
{ 3 { 2, 1 } } becomes :vl-multiconcat (arity 2)

Streaming Concatenations

For SystemVerilog streaming concatenations we add new variable-arity operators:

{<< [size] { arg1 arg2 ... }}
  -->
(:vl-stream-left [size] arg1 arg2 ...)

{>> [size] { arg1 arg2 ... }}
  -->
(:vl-stream-right [size] arg1 arg2 ...)

For the special with expressions, we add four new operators:

foo with [1] becomes :vl-with-index (arity 2)
foo with [3:1] becomes :vl-with-colon (arity 3)
foo with [3+:1] becomes :vl-with-pluscolon (arity 3)
foo with [3-:1] becomes :vl-with-minuscolon (arity 3)

Function Calls

foo(1,2,3) becomes :vl-funcall (arity nil)
$foo(1,2,3) becomes :vl-syscall (arity nil)

Hierarchical Identifiers

Note: see vl-hidpiece-p for some additional discussion about hierarchical identifiers.

foo.bar becomes :vl-hid-dot (arity 2)
foo[3][4].bar becomes a :vl-hid-dot whose from argument is a tree of :vl-index operators.

Casting

The SystemVerilog-2012 casting operator, e.g., int'(2.0), is represented with a binary operator, :vl-binary-cast. The first argument is the desired type (e.g., int), and the second argument is the expression to cast to this type (e.g., 2.0). See Section 6.24 from the SystemVerilog-2012 Standard.

Inside Expressions

The SystemVerilog inside expression gets dealt with via three operators. To illustrate consider:

foo inside { bar, [a:b], baz }

This will get represented as a top-level :vl-inside operator applied to two arguments: foo and the right-hand side. The right-hand side is a single :vl-valuerangelist operator, applied to all of the members of the range list. The individual arguments are ordinary expressions (in the case of bar and baz), with value ranges like [a:b] represented by the special :vl-valuerange applied to the two arguments.

Definition: *vl-ops-table*

(defconst *vl-ops-table*
 (list$
  (cons :vl-unary-plus (make-vl-opinfo :arity 1 :text "+"))
  (cons :vl-unary-minus (make-vl-opinfo :arity 1 :text "-"))
  (cons :vl-unary-lognot (make-vl-opinfo :arity 1 :text "!"))
  (cons :vl-unary-bitnot (make-vl-opinfo :arity 1 :text "~"))
  (cons :vl-unary-bitand (make-vl-opinfo :arity 1 :text "&"))
  (cons :vl-unary-nand (make-vl-opinfo :arity 1 :text "~&"))
  (cons :vl-unary-bitor (make-vl-opinfo :arity 1 :text "|"))
  (cons :vl-unary-nor (make-vl-opinfo :arity 1 :text "~|"))
  (cons :vl-unary-xor (make-vl-opinfo :arity 1 :text "^"))
  (cons :vl-unary-xnor (make-vl-opinfo :arity 1 :text "~^"))
  (cons :vl-unary-preinc (make-vl-opinfo :arity 1 :text "++"))
  (cons :vl-unary-predec (make-vl-opinfo :arity 1 :text "--"))
  (cons :vl-unary-postinc (make-vl-opinfo :arity 1 :text "++"))
  (cons :vl-unary-postdec (make-vl-opinfo :arity 1 :text "--"))
  (cons :vl-binary-plus (make-vl-opinfo :arity 2 :text "+"))
  (cons :vl-binary-minus (make-vl-opinfo :arity 2 :text "-"))
  (cons :vl-binary-times (make-vl-opinfo :arity 2 :text "*"))
  (cons :vl-binary-div (make-vl-opinfo :arity 2 :text "/"))
  (cons :vl-binary-rem (make-vl-opinfo :arity 2 :text "%"))
  (cons :vl-binary-eq (make-vl-opinfo :arity 2 :text "=="))
  (cons :vl-binary-neq (make-vl-opinfo :arity 2 :text "!="))
  (cons :vl-binary-ceq (make-vl-opinfo :arity 2 :text "==="))
  (cons :vl-binary-cne (make-vl-opinfo :arity 2 :text "!=="))
  (cons :vl-binary-wildeq (make-vl-opinfo :arity 2 :text "==?"))
  (cons :vl-binary-wildneq (make-vl-opinfo :arity 2 :text "!=?"))
  (cons :vl-binary-logand (make-vl-opinfo :arity 2 :text "&&"))
  (cons :vl-binary-logor (make-vl-opinfo :arity 2 :text "||"))
  (cons :vl-binary-power (make-vl-opinfo :arity 2 :text "**"))
  (cons :vl-binary-lt (make-vl-opinfo :arity 2 :text "<"))
  (cons :vl-binary-lte (make-vl-opinfo :arity 2 :text "<="))
  (cons :vl-binary-gt (make-vl-opinfo :arity 2 :text ">"))
  (cons :vl-binary-gte (make-vl-opinfo :arity 2 :text ">="))
  (cons :vl-binary-bitand (make-vl-opinfo :arity 2 :text "&"))
  (cons :vl-binary-bitor (make-vl-opinfo :arity 2 :text "|"))
  (cons :vl-binary-xor (make-vl-opinfo :arity 2 :text "^"))
  (cons :vl-binary-xnor (make-vl-opinfo :arity 2 :text "~^"))
  (cons :vl-binary-shr (make-vl-opinfo :arity 2 :text ">>"))
  (cons :vl-binary-shl (make-vl-opinfo :arity 2 :text "<<"))
  (cons :vl-binary-ashr (make-vl-opinfo :arity 2 :text ">>>"))
  (cons :vl-binary-ashl (make-vl-opinfo :arity 2 :text "<<<"))
  (cons :vl-binary-assign (make-vl-opinfo :arity 2 :text "="))
  (cons :vl-binary-plusassign (make-vl-opinfo :arity 2 :text "+="))
  (cons :vl-binary-minusassign (make-vl-opinfo :arity 2 :text "-="))
  (cons :vl-binary-timesassign (make-vl-opinfo :arity 2 :text "*="))
  (cons :vl-binary-divassign (make-vl-opinfo :arity 2 :text "/="))
  (cons :vl-binary-remassign (make-vl-opinfo :arity 2 :text "%="))
  (cons :vl-binary-andassign (make-vl-opinfo :arity 2 :text "&="))
  (cons :vl-binary-orassign (make-vl-opinfo :arity 2 :text "|="))
  (cons :vl-binary-xorassign (make-vl-opinfo :arity 2 :text "^="))
  (cons :vl-binary-shlassign (make-vl-opinfo :arity 2 :text "<<="))
  (cons :vl-binary-shrassign (make-vl-opinfo :arity 2 :text ">>="))
  (cons
       :vl-binary-ashlassign (make-vl-opinfo :arity 2 :text "<<<="))
  (cons
       :vl-binary-ashrassign (make-vl-opinfo :arity 2 :text ">>>="))
  (cons :vl-implies (make-vl-opinfo :arity 2 :text "->"))
  (cons :vl-equiv (make-vl-opinfo :arity 2 :text "<->"))
  (cons :vl-qmark (make-vl-opinfo :arity 3 :text nil))
  (cons :vl-mintypmax (make-vl-opinfo :arity 3 :text nil))
  (cons :vl-index (make-vl-opinfo :arity 2 :text nil))
  (cons :vl-bitselect (make-vl-opinfo :arity 2 :text nil))
  (cons :vl-select-colon (make-vl-opinfo :arity 3 :text nil))
  (cons :vl-select-pluscolon (make-vl-opinfo :arity 3 :text nil))
  (cons :vl-select-minuscolon (make-vl-opinfo :arity 3 :text nil))
  (cons :vl-partselect-colon (make-vl-opinfo :arity 3 :text nil))
  (cons
       :vl-partselect-pluscolon (make-vl-opinfo :arity 3 :text nil))
  (cons
      :vl-partselect-minuscolon (make-vl-opinfo :arity 3 :text nil))
  (cons :vl-concat (make-vl-opinfo :arity nil :text nil))
  (cons :vl-multiconcat (make-vl-opinfo :arity 2 :text nil))
  (cons :vl-stream-left (make-vl-opinfo :arity nil :text nil))
  (cons :vl-stream-right (make-vl-opinfo :arity nil :text nil))
  (cons :vl-stream-left-sized (make-vl-opinfo :arity nil :text nil))
  (cons
       :vl-stream-right-sized (make-vl-opinfo :arity nil :text nil))
  (cons :vl-with-index (make-vl-opinfo :arity 2 :text nil))
  (cons :vl-with-colon (make-vl-opinfo :arity 3 :text nil))
  (cons :vl-with-pluscolon (make-vl-opinfo :arity 3 :text nil))
  (cons :vl-with-minuscolon (make-vl-opinfo :arity 3 :text nil))
  (cons :vl-funcall (make-vl-opinfo :arity nil :text nil))
  (cons :vl-syscall (make-vl-opinfo :arity nil :text nil))
  (cons :vl-hid-dot (make-vl-opinfo :arity 2 :text "."))
  (cons :vl-scope (make-vl-opinfo :arity 2 :text "::"))
  (cons :vl-tagged (make-vl-opinfo :arity nil
                                   :text "tagged"))
  (cons :vl-binary-cast (make-vl-opinfo :arity 2 :text "'"))
  (cons
       :vl-pattern-positional (make-vl-opinfo :arity nil :text nil))
  (cons :vl-pattern-multi (make-vl-opinfo :arity 2 :text nil))
  (cons :vl-pattern-keyvalue (make-vl-opinfo :arity nil :text nil))
  (cons :vl-keyvalue (make-vl-opinfo :arity 2 :text nil))
  (cons :vl-pattern-type (make-vl-opinfo :arity 2 :text nil))
  (cons :vl-inside (make-vl-opinfo :arity 2
                                   :text "inside"))
  (cons :vl-valuerangelist (make-vl-opinfo :arity nil :text nil))
  (cons :vl-valuerange (make-vl-opinfo :arity 2 :text nil))))

Subtopics

Vl-opinfo-p