声明
位向量表达式（或项）由位向量常数、位向量变量以及下列函数构成。在STP中，所有变量必须在使用前声明。声明一个长度为32的位向量变量的例子是：x : BITVECTOR(32);。声明数组的例子如下：
x_arr : ARRAY BITVECTOR(32) OF BITVECTOR(5000);
功能和术语
长度为0的位向量变量（或术语）是不允许的。位向量常数可以用二进制或十六进制格式表示。最右边的位称为最低有效位（LSB），最左边的位称为最高有效位（MSB）。LSB的索引是0，而n位常数的MSB的索引是n-1。这个约定自然地扩展到所有位向量表达式。以下是一些以二进制和十六进制表示的位向量常数的例子：
0bin0000111101010000
0hex0f50
STP中的位向量实现支持非常多的函数和谓词。这些函数分为字级函数、位级函数和算术函数。
字级函数
| 名称 | 符号 | 示例 |
|---|---|---|
| 连接 | @ | t1@t2@…@tm |
| 提取 | [i:j] | x[31:26] |
| 左移 | << | 0bin0011 << 3 = 0bi n0011000 |
| 右移 | >> | x[24:17] >> 5, 另一个例子: 0bin1000 >> 3 = 0bin0001 |
| 符号扩展 | BVSX(bv,n) | BVSX(0bin100, 5) = 0bin11100 |
| 数组读取 | [index] | x_arr[t1] |
| 数组写入 | WITH | x_arr WITH [index] := value |
注释：
- 对于提取项，例如 t[i:j]，n > i >= j > 0，其中 n 是 t 的长度。
- 对于左移项，t << k 表示将 k 个 0 追加到 t 的右端。t << k 的长度为 n * +* k。
- 对于右移项，t >> k 表示通过 k 个 0 跟随t[n-1,k]得到的位向量，其长度为 t >> k 为 n。
例子
- 连接
ASSERT x@y = 0b1101@0b11; // 连接 x 和 y，假设 x = 1101 和 y = 11
位级函数
| 名称 | 符号 | 示例 |
|---|---|---|
| 位与 | & | t1 & t2 & … & tm |
| 位或 | | | t1 | t2 | … | tm |
| 位非 | ~ | ~t1 |
| 位异或 | BVXOR | BVXOR(t1, t2) |
| 位与非 | BVNAND | BVNAND(t1, t2) |
| 位或非 | BVNOR | BVNOR(t1, t2) |
| 位同或 | BVXNOR | BVXNOR(t1, t2) |
注意： 所有位运算函数的参数必须具有相同的长度。
算术函数
| 名称 | 符号 | 示例 |
|---|---|---|
| 位向量加法 | BVPLUS | BVPLUS(n, t1, t2, …, tm) |
| 位向量乘法 | BVMULT | BVMULT(n, t1, t2) |
| 位向量减法 | BVSUB | BVSUB(n, t1, t2) |
| 位向量一元负 | BVUMINUS | BVUMINUS(t1) |
| 位向量除法 | BVDIV | BVDIV(n, t1, t2) |
| 有符号位向量除法 | SBDIV | SBDIV(n, t1, t2) |
| 位向量模数 | BVMOD | BVMOD(n, t1, t2) |
| 有符号位向量模数 | SBVMOD | SBVMOD(n, t1, t2) |
注释：
- 输出位的数量必须被指定（一元负数除外）。
- 所有输入必须具有相同的长度。
BVUMINUS(t)是BVPLUS(n, ~t, 0bin1)的简写，其中 n 是 t 的长度。BVSUB(n, t1, t2)是BVPLUS(n, t1, BVUMINUS(t2))的简写。
STP 还支持条件表达式，例如 IF cond THEN t1 ELSE t2 ENDIF，其中 cond 是布尔表达式，t1 和 t2 可以是位向量表达式。这样可以模拟多路选择器。一个例子是：
x, y : BITVECTOR(1);
QUERY(x = (IF 0bin0 = x THEN y ELSE BVUMINUS(y) ENDIF));
谓词
| 名称 | 符号 | 示例 |
|---|---|---|
| 等于 | = | t1=t2 |
| 小于 | BVLT | BVLT(t1, t2) |
| 大于 | BVGT | BVGT(t1, t2) |
| 小于或等于 | BVLE | BVLE(t1, t2) |
| 大于或等于 | BVGE | BVGE(t1, t2) |
| 有符号小于 | SBVLT | SBVLT(t1, t2) |
| 有符号大于 | SBVGT | SBVGT(t1, t2) |
| 有符号小于或等于 | SBVLE | SBVLE(t1, t2) |
| 有符号大于或等于 | SBVGE | SBVGE(t1, t2) |
注意：
- STP 要求像 x = y 这样的原子公式中，x 和 y 必须是长度相同的表达式。
- STP接受原子公式的布尔组合。
注释
以%开头的是注释。
例子
Example1
x : BITVECTOR(5); //声明了一个名为 x 的位向量变量，它的长度是5位。
y : BITVECTOR(4); //明了一个名为 y 的位向量变量，它的长度是4位
QUERY( //查询表达式，STP将尝试验证括号内的表达式是否总是为真
BVPLUS(9, x@0bin0000, (0bin000@(~y)@0bin11))[8:4]
=
BVPLUS(5, x, 0bin000@~(y[3:2]))
);
