AIGER 1.9

目录

• AIGER 1.9
  • 1. 简介
  • 2. 复位逻辑
  • 3. 多重性质(multiple properties)
  • 3.不变式约束
  • 4. Liveness性质和公平约束
  • 5.API
  • 6. Witness格式

AIGER 1.9

1. 简介

为了方便迁移，1.9版本的AIGER格式在句法上和之前的版本是向下兼容的，同时包括了随后的2.0版本AIGER格式的一些新特性。由于使用了新的二进制编码，2.0版本的AIGER格式将不会向下兼容。
1.9版本AIGER格式大体上有如下5个新的语义特性：

• 复位逻辑 reset logic
• 多重性质multiple properties
• 不变式约束 invariant constraints
• 公正性质 justice properties
• 公平约束 fairness constraints
  以下分小节讨论这些特性，并介绍对老版本的句法扩展，API的改变，以及新的witness格式。

2. 复位逻辑

AIGER格式应该可以用作综合过程(synthesis)中的一种中间语言，允许出现大量被标记为未初始化的锁存器，因此在新版本中添加了复位逻辑。在新版本中，一个锁存器要么被初始化为0(兼容老版本，新版本中为默认选项)，要么被初始化为1，要么被标记为未初始化。
语法上，定义锁存器时，新版本在原版本的基础上，在下一状态文字后添加一可选的文字用来指示初始状态，可选文字可以是0、1或者表示锁存器本身的文字。前面的0和1用来进行常数初始化，后者用来定义未初始化的锁存器。
在没有句法变化的情况下，这能够确保未来能够实现更一般化的复位逻辑。
当前版本只能支持常数初始化和未初始化的锁存器。

3. 多重性质(multiple properties)

如何同时定义和检测一个模型中的多种性质？实际上，一个模型通常具有多种性质，而且一个模型的不变式性质能够帮助更快的检测其他性质。
之前版本只允许定义一个性质，现在可以定义多个性质。最大的改变在于witness格式(见后文)。
AIG文件的header行也做了一些改变。之前版本的header行的格式是aig M I L O A，现在在原有的基础上再增加了4个数字B C J F。其中，B代表坏态性质("bad state" properties)的个数；C J F分别代表不变式约束(invariant constraints)的个数、公正性质(justice properties)的个数、公平约束(fairness constraints)的个数。坏态性质("bad state" property)是关于不变式的简单安全性质的否定。其余三个的解释在下文。
新的文件头是老版本文件头的扩展。新版本文件头可以将后缀0全部省略掉。例如，下面的一位计数器(one-bit counter)，含有一个使能输入文字2，坏态性质是用于输出的锁存器文字4，该锁存器初始化为0，它的下一状态文字是10。该计数器的逻辑为如果输入为1,则将锁存器进行反转；否则锁存器不改变。这个逻辑是通过XOR异或门实现的。

aag 5 1 1 0 3 1
2
4 10 0
4		bad state, not output
6 5 3
8 4 2
10 9 7

和老版本一样，一个坏态性质b是一个简单的安全性质AG g的否定，即b=!g，g代表“好”的状态。如果b是可满足的，则系统能够到达一个坏态。
二进制格式中，输入部分(文字2)和锁存器定义的第一个文字(文字4)都可以省略。与门和老版本一样也是使用二进制编码。
老版本header行中没有坏态定义部分，而新版本中有(上述header行中的最后一个数字1)。坏态性质必须作为输出被列举出来。因此上述AIG文件如果要转换为老版本，只要改变header行就可以，如下：

aag 5 1 1 1 3

3.不变式约束

对于第二节的例子，我们想检测该系统在没有启用输入的情况下，是否可能到达一个坏态(也就是"锁存器为1")。

aag 5 1 1 0 3 1 1
2
4 10 0
4		bad state, not output
3		invariant constraint
6 5 3
8 4 2
10 9 7

这个不变式约束应该从第一个状态开始保持成立，直到(包括)到达一个坏态。在线性时序逻辑(LTL)中，一个对于这样的坏态的witness是满足公式(cU(cland b))的一条路径，其中c是不变式约束的合取，b是一个坏态性质，U是时序逻辑时态连接词。
坏态的witness一般是一条有限路径，因此能够在不经转化的前提下被安全性质检测算法发现。
记所要证明的坏态性质的否定为(g=ar{b})(好态)，则证明问题可以转换为证明LTL公式(ar{c} R (c ightarrow g))在所有的初始化路径上都成立，这个证明的解释是：当性质c不再满足时，性质g开始满足。

4. Liveness性质和公平约束

将LTL转换为通用(Bddot{u}chi)自动机(类似于LTL2SMV工具的功能)，转换结果是：一个LTL性质对应于一个公平约束集合。这样的一个公平约束集合称为公正"justice"性质。一个公正性质对应的witness是一条无限的初始路径，该公正性质(公平约束集合)中的每个公平约束都能满足无限次。

5.API

新版本AIGER格式在不改变原有方程的作用和意义的前提下扩展了aiger.h中的API，新特性对应的方程如下：

void aiger_add_reset (aiger *, unsigned lit, unsigned reset);
void aiger_add_bad (aiger *, unsigned lit, const char *);
void aiger_add_constraint (aiger *, unsigned lit, const char *);
void aiger_add_justice (aiger *, unsigned size, unsigned *, const char *);
void aiger_add_fairness (aiger *, unsigned lit, const char *);

6. Witness格式

一个witness文件以0，1或者2开始。0表示所验证的性质不能满足，也就是说没有可达的坏态。2表示性质可满足性未知。1表示找到一个witness。