****************************
CVC Input Language Reference
****************************

.. highlight:: lisp

This page contains a description for the input language that STP expects
by default.

Declarations
============

Bitvector expressions (or terms) are constructed out of bitvector
constants, bitvector variables and the functions listed below. In STP
all variables have to declared before the point of use. An example
declaration of a bitvector variable of length 32 is as follows:
``x : BITVECTOR(32);``. An example of an array declaration is as
follows:

::

    x_arr : ARRAY BITVECTOR(32) OF BITVECTOR(5000);

Functions and Terms
===================

Bitvector variables (or terms) of length 0 are not allowed. Bitvector
constants can be represented in binary or hexadecimal format. The
rightmost bit is called the least significant bit (LSB), and the
leftmost bit is the most significant bit (MSB). The index of the LSB is
0, and the index of the MSB is *n*-1 for an *n*-bit constant. This
convention naturally extends to all bitvector expressions. Following
are some examples of bitvector constants in binary and hexadecimal:

::

    0bin0000111101010000
    0hex0f50

The Bitvector implementation in STP supports a very large number of
functions and predicates. The functions are categorized into word-level
functions, bitwise functions, and arithmetic functions.

Word-level functions
~~~~~~~~~~~~~~~~~~~~

+-----------------------+-----------------------+-----------------------+
| Name                  | Symbol                | Example               |
+=======================+=======================+=======================+
| Concatenation         | ``@``                 | ``t1@t2@...@tm``      |
+-----------------------+-----------------------+-----------------------+
| Extraction            | ``[i:j]``             | ``x[31:26]``          |
+-----------------------+-----------------------+-----------------------+
| left shift            | ``<<``                | ``0bin0011 << 3 = 0bi |
|                       |                       | n0011000``            |
+-----------------------+-----------------------+-----------------------+
| right shift           | ``>>``                | ``x[24:17] >> 5``,    |
|                       |                       | another example:      |
|                       |                       | ``0bin1000 >> 3 = 0bi |
|                       |                       | n0001``               |
+-----------------------+-----------------------+-----------------------+
| sign extension        | ``BVSX(bv,n)``        | ``BVSX(0bin100, 5) =  |
|                       |                       | 0bin11100``           |
+-----------------------+-----------------------+-----------------------+
| Array READ            | ``[index]``           | ``x_arr[t1]``         |
+-----------------------+-----------------------+-----------------------+
| Array WRITE           | ``WITH``              | ``x_arr WITH [index]  |
|                       |                       | := value``            |
+-----------------------+-----------------------+-----------------------+

Notes:

- For extraction terms, say ``t[i:j]``, *n* > *i* >= *j* >= 0, where
  *n* is the length of *t*.

- For left shift terms, ``t << k`` is equal to *k* 0’s appended to *t*. The length
  of ``t << k`` is *n*+*k*.

- For right shift terms, say ``t >> k``, the term is equal to the bitvector
  obtained by *k* 0’s followed by ``t[n-1:k]``. The length of ``t >> k`` is *n*.


Bitwise functions
~~~~~~~~~~~~~~~~~

+--------------+------------+------------------------+
| Name         | Symbol     | Example                |
+==============+============+========================+
| Bitwise AND  | ``&``      | ``t1 & t2 & ... & tm`` |
+--------------+------------+------------------------+
| Bitwise OR   | ``|``      | ``t1 | t2 | ... | tm`` |
+--------------+------------+------------------------+
| Bitwise NOT  | ``~``      | ``~t1``                |
+--------------+------------+------------------------+
| Bitwise XOR  | ``BVXOR``  | ``BVXOR(t1,t2)``       |
+--------------+------------+------------------------+
| Bitwise NAND | ``BVNAND`` | ``BVNAND(t1,t2)``      |
+--------------+------------+------------------------+
| Bitwise NOR  | ``BVNOR``  | ``BVNOR(t1,t2)``       |
+--------------+------------+------------------------+
| Bitwise XNOR | ``BVXNOR`` | ``BVXNOR(t1,t2)``      |
+--------------+------------+------------------------+

NOTE: It is required that all the arguments of bitwise functions have
the same length

Arithmetic functions
~~~~~~~~~~~~~~~~~~~~

+-----------------------+-----------------------+-----------------------+
| Name                  | Symbol                | Example               |
+=======================+=======================+=======================+
| Bitvector Add         | ``BVPLUS``            | ``BVPLUS(n,t1,t2,..., |
|                       |                       | tm)``                 |
+-----------------------+-----------------------+-----------------------+
| Bitvector Multiply    | ``BVMULT``            | ``BVMULT(n,t1,t2)``   |
+-----------------------+-----------------------+-----------------------+
| Bitvector Subtract    | ``BVSUB``             | ``BVSUB(n,t1,t2)``    |
+-----------------------+-----------------------+-----------------------+
| Bitvector Unary Minus | ``BVUMINUS``          | ``BVUMINUS(t1)``      |
+-----------------------+-----------------------+-----------------------+
| Bitvector Divide      | ``BVDIV``             | ``BVDIV(n,t1,t2)``,   |
|                       |                       | where ``t1`` is the   |
|                       |                       | dividend and ``t2``   |
|                       |                       | is the divisor        |
+-----------------------+-----------------------+-----------------------+
| Signed Bitvector      | ``SBVDIV``            | ``SBVDIV(n,t1,t2)``,  |
| Divide                |                       | where ``t1`` is the   |
|                       |                       | dividend and ``t2``   |
|                       |                       | is the divisor        |
+-----------------------+-----------------------+-----------------------+
| Bitvector Modulo      | ``BVMOD``             | ``BVMOD(n,t1,t2)``,   |
|                       |                       | where ``t1`` is the   |
|                       |                       | dividend and ``t2``   |
|                       |                       | is the divisor        |
+-----------------------+-----------------------+-----------------------+
| Signed Bitvector      | ``SBVMOD``            | ``SBVMOD(n,t1,t2)``,  |
| Modulo                |                       | where ``t1`` is the   |
|                       |                       | dividend and ``t2``   |
|                       |                       | is the divisor        |
+-----------------------+-----------------------+-----------------------+

Notes:

- The number of output bits must be specified (expect for unary minus).

- All inputs must be of the same length.

- ``BVUMINUS(t)`` is a short-hand for ``BVPLUS(n,~t,0bin1)``, where *n* is the
  length of *t*.

- ``BVSUB(n,t1,t2))`` is a short-hand for ``BVPLUS(n,t1,BVUMINUS(t2))``.

STP also supports conditional terms, e.g., ``IF cond THEN t1 ELSE t2 ENDIF``,
where *cond* is a boolean term, and *t*\ 1 and *t*\ 2 can be bitvector terms. This
allows us to simulate multiplexors. An example is:

::

    x, y : BITVECTOR(1);
    QUERY(x = (IF 0bin0 = x THEN y ELSE BVUMINUS(y) ENDIF));

Predicates
==========

Following are the predicates supported by STP:

+---------------------------------+-----------+------------------+
| Name                            | Symbol    | Example          |
+=================================+===========+==================+
| Equality                        | ``=``     | ``t1=t2``        |
+---------------------------------+-----------+------------------+
| Less Than                       | ``BVLT``  | ``BVLT(t1,t2)``  |
+---------------------------------+-----------+------------------+
| Greater Than                    | ``BVGT``  | ``BVGT(t1,t2)``  |
+---------------------------------+-----------+------------------+
| Less Than Or Equal To           | ``BVLE``  | ``BVLE(t1,t2)``  |
+---------------------------------+-----------+------------------+
| Greater Than Or Equal To        | ``BVGE``  | ``BVGE(t1,t2)``  |
+---------------------------------+-----------+------------------+
| Signed Less Than                | ``SBVLT`` | ``SBVLT(t1,t2)`` |
+---------------------------------+-----------+------------------+
| Signed Greater Than             | ``SBVGT`` | ``SBVGT(t1,t2)`` |
+---------------------------------+-----------+------------------+
| Signed Less Than Or Equal To    | ``SBVLE`` | ``SBVLE(t1,t2)`` |
+---------------------------------+-----------+------------------+
| Signed Greater Than Or Equal To | ``SBVGE`` | ``SBVGE(t1,t2)`` |
+---------------------------------+-----------+------------------+

Note: STP requires that in atomic formulas such as ``x = y``, ``x`` and
``y`` are expressions of the same length. STP accepts boolean
combination of atomic formulas.

Comments
========

Any line whose first character is ``%`` is a comment.

Some Examples
=============

Example 1 illustrates the use of arithmetic, word-level and bitwise NOT
operations:

::

    x : BITVECTOR(5);
    y : BITVECTOR(4);
    QUERY(
      BVPLUS(9, x@0bin0000, (0bin000@(~y)@0bin11))[8:4]
      =
      BVPLUS(5, x, 0bin000@~(y[3:2]))
    );

Example 2 illustrates the use of arithmetic, word-level and multiplexor
terms:

::

    bv : BITVECTOR(10);
    a  : BOOLEAN;
    
    QUERY(
      (0bin01100000[5:3] = (0bin1111001@bv[0:0])[4:2])
      AND
      (
        0bin1@(IF a THEN 0bin0 ELSE 0bin1 ENDIF)
        =
        (IF a THEN 0bin110 ELSE 0bin011 ENDIF)[1:0]
      )
    );

Example 3 illustrates the use of bitwise operations:

::

    x, y, z, t, q : BITVECTOR(1024);

    ASSERT(x = ~x);
    ASSERT(x & y & t & z & q = x);
    ASSERT(x | y = t);
    ASSERT(BVXOR(x, ~x) = t);
    QUERY(FALSE);

Example 4 illustrates the use of predicates and all the arithmetic
operations:

::

    x, y : BITVECTOR(8);
    ASSERT(x = 0hex05);
    ASSERT(y = 0bin00000101);
    QUERY(
      (BVMULT(8,x,y) = BVMULT(8,y,x))
      AND
      NOT(BVLT(x,y))
      AND
      BVLE(BVSUB(8,x,y), BVPLUS(8, x, BVUMINUS(x)))
      AND
      (x = BVSUB(8, BVUMINUS(x), BVPLUS(8, x,0hex01)))
    );

Example 5 illustrates the use of shift functions

::

    x, y : BITVECTOR(8);
    z, t : BITVECTOR(12);

    ASSERT(x = 0hexff);
    ASSERT(z = 0hexff0);
    QUERY(z = x << 4);

For invalid inputs, the ``COUNTEREXAMPLE`` command can be used to generate
appropriate counterexamples. The generated counter example is
essentially a bitwise assignment to the variables in the input.