AIGER
1. 介紹
AIGER是AIG()And-Inverter Graphs)的文件格式的代稱，是瑞士境內阿爾卑斯山的一座山峰。AIGER格式CAV2007模型檢測競賽提供了一種簡潔明了的文件格式。
AIGER文件格式含有ASCII格式和二進制格式兩個版本。當一個應用沒有使用AIGER庫時，可以生成ASCII格式的AIG文件。
二進制格式更加簡潔，格式更嚴謹，是基准測試和競賽所采取的格式。生成二進制格式AIG文件有兩種方法，第一種是用AIGER庫直接生成，第二種是使用aigtoaig工具將ASCII格式轉換成二進制格式(反過來也行，因此也將此工具用來驗證二進制格式AIG文件的正確性)。
在http://fmv.jku.at/aiger/ 任意下載一個版本aiger-1.9.1.tar.gz, 在其中的examples目錄下可以找到示例文件。
ASCII格式的AIG文件第一行由字符串
aag開始，aag是ASCII AIG的縮寫；然后是以空格分隔5個非負整數，分別由M, I, L, O, A表示。
其中
M= 最大變量下標 maximum variable indexI= 輸入個數 number of inputsL= 鎖存器個數 number of latchesO= 輸出個數 number of outputsA= 與門個數 number of AND gates
沒有輸入且沒有輸出的空電路AIG文件只包含如下的一行(
header是注釋)：
aag 0 0 0 0 0 header
包含如下兩行的AIG文件代表常量
FALSE,其中header(第一行)中的1代表輸出的個數為1，第二行代表唯一的輸出literal.
aag 0 0 0 1 0 header
0 output
如下AIG文件代表常量
TRUE
aag 0 0 0 1 0 header
1 output
下述文件是一個
buffer， 第一行中，其中第一個數1為最大變量下標(maximal variable index)，第二個數1代表輸入個數；第二行是一個輸入literal(一個變量通過乘以2可以轉換為文字literal，即如果輸入為2的倍數且大於0，則它為一個literal)。在 第一種情況下，最后一行指定的輸出和輸入相同；在第二種情況下輸出和輸入相反，因為輸出的文字3帶有符號位(3的二進制表示的最低有效位為1，代表相反)
aag 1 1 0 1 0 header
2 input
2 output
下列文件是一個
inverter
aag 1 1 0 1 0 header
2 input
3 output
如下AIG文件表示一個與門(
AND gate)。其中，第一行中的第一個數為3，代表最大變量下標(下標從0開始，即有0,1,2,3)；代表與門的文字為6，下標(從上至下來)為3；與門個數為1(第一行最后的數字)
aag 3 2 0 1 1
2 input 0
4 input 1
6 output 0
6 2 4 AND gate 0 1&2
或門可以表示為
aag 3 2 0 1 1
2 input 0
4 input 1
7 output 0 !(!1&!2)
6 3 5 AND gate 0 !1&!2
一個完整的組合電路。其中，symbol行是可選的(用來表示輸入、鎖存器、輸出的符號)
aag 7 2 0 2 3 header line
2 input 0 1st addend bit 'x'
4 input 1 2nd addend bit 'y'
6 output 0 sum bit 's'
12 output 1 carry 'c'
6 13 15 AND gate 0 x ^ y
12 2 4 AND gate 1 x & y
14 3 5 AND gate 2 !x & !y
i0 x symbol
i1 y symbol
o0 s symbol
o1 c symbol
c comment header
half adder comment
時序電路使用鎖存器(
latches)作為狀態變量，下述AIG文件是一個振盪轉換電路，只含有一個鎖存器和兩個輸出，沒有輸入；該系統包含兩個相反的狀態。
aag 1 0 1 2 0
2 3 latch 0 with next state literal
2 output 0
3 output 1
鎖存器通常被初始化為0。下面使用了“使能信號”
enable和額外的低電平復位信號作為輸入，實現了上述振盪電路（小提示：看AND/與門的組成結構時，從最下面一個AND/與門往上看）
aag 7 2 1 2 4
2 input 0 'enable'
4 input 1 'reset'
6 8 latch 0 Q next(Q)
6 output 0 Q
7 output 1 !Q
8 4 10 AND gate 0 reset & (enable ^ Q)
10 13 15 AND gate 1 enable ^ Q
12 2 6 AND gate 2 enable & Q
14 3 7 AND gate 3 !enable & !Q
文字的順序和與門的定義是無關的。二進制格式對順序增加了更多的限制，也不允許出現未使用的文字。
2.設計選擇
- 能對組合電路進行建模
- 能描述結構化的SAT問題
- 能對時序電路進行建模
- 能描述模型檢測問題
- 操作符僅限於比特級別
- 操作符集合盡可能簡單
- 具有簡潔且標准化的二進制格式
- 應用程序能夠方便地生成ASCII格式的AIG文件
- 應用程序能夠方便讀取二進制格式的AIG文件
- 具有符號表和注釋
- 讀取文件時能夠按序舍棄符號表和注釋
- 能夠允許一些簡單的拓展
3. ASCII格式
- ASCII格式的AIG文件在第一行(
header行)具有一個格式標識符aag(是ASCII AIG的簡寫)，且文件的擴展名為.aag。
AIGER庫能夠讀取使用GNU GZIP壓縮的包含AIG文件的壓縮文件(壓縮包需要具有.gz的擴展名) header行后面緊接着的是I個輸入，每行一個輸入，均為非否定的文字(literal)，用正偶數來表示。- 接下來是定義
L個鎖存器，每行一個。每一個鎖存器定義都由兩個正整數表示，第一個正整數是偶數，表示該鎖存器當前狀態；第二個用來指示該鎖存器的下個狀態。 - 然后是
O個輸出文字(output literals)，每行一個。輸出文字的內容是任意的。 - 之后是
A個與門的定義，每行一個。每一個與門包含3個正整數，相鄰整數用一個空格分開。第一個整數是偶數，表示與門的左值(left-hand side, LHS,結果)；其余兩個整數表示與門的右值(right-hand side, RHS，輸入) - 為了保持結構良好，
I個輸入文字需要彼此不相同，L個鎖存器的當前狀態文字也互不相同，以及A個與門的左值LHS文字互不相同，因此恰好需要I+L+A個文字。 - 其他沒定義的文字，除了兩個常量
0和1外，均不能用來作為輸出文字，也不能作為下個狀態文字，也不能作為與門的右值RHS文字。 - 與門的定義必須不能循環依賴，即某與門的左值LHS文字不能和同一與門的右值RHS文字相同(在去掉符號位的情況下)。這種依賴關系的傳遞非自反閉包必須是無環的。
- ASCII格式的AIG文件需要先檢查無定義的文字和循環依賴，而格式約束較多的二進制格式則不需要進行檢查。AIGER庫中的
aignm和aigtoaig均可以用來檢查AIG文件的格式是否正確。 - 最后一點，ASCII格式的AIG文件中定義的文字個數不一定要和最大變量下標
M相等，因為有些文字可能不需要用到。
4. 符號表(Symbols table)
在定義了與門之后，可以選擇定義一個符號表(Symbols table)。一個符號是一個可打印字符(除去換行符)所組成的字符串。符號只能被賦予輸入、鎖存器和輸出，且每個輸入、鎖存器和輸出只能被分別賦予一個符號。一個符號占據一行。符號類型指示符由i,l,o加上一個位置(在輸入、鎖存器、輸出中的位置，例如該符號指示第一個輸入，則其位置為0)組成，符號名稱是一個字符串，符號表中的一項則由符號類型指示符合符號名稱構成，結構如下：
[ilo]<pos> <string>
符號表和注釋放置在各種定義之后，所以應用程序讀取AIG文件則只需讀取定義后就停止讀取。
5. 注釋(comment)
可選的注釋內容放置在文件最后。注釋部分有一個注釋頭(comment header)，該注釋頭由一個單獨的字符c開始，最后是一個換行符。注釋頭下面的每一行都是注釋。如果有注釋，則文件的最后一個字符必須為換行符。
6. 二進制格式的優勢
二進制格式比ASCII格式更加嚴格。文字必須按照特定的順序排列。順序限制和數字的二進制補碼表示能夠使得二進制格式文件更加易於閱讀且更加簡潔。實驗表明，這些限制和額外的增量編碼能夠構造更小的文件。某模型的二進制格式文件通常比經過GZIP壓縮的ASCII格式的文件更小。壓縮二進制格式能夠得到更小容量的文件。
7.二進制格式的定義
在語義上，二進制格式是ASCII格式的一個子集，只在語法上有些不同。將一個二進制格式文件轉換為一個ASCII格式文件，再轉換回二進制格式，會得到與轉換之前相同的二進制格式文件，即便二進制格式會重新編碼文字(reencode literals)。
如果定義了輸入文字，則所有鎖存器的當前狀態文字可以省略。
與門的定義是二進制編碼的。
符號表和注釋部分的定義和ASCII格式文件相同。
二進制格式文件(.aig文件)的header是使用ASCII格式。示例如下：
aig M I L O A
常量、變量和文字的處理方式和ASCII格式的AIG文件一樣。
二進制文件在輸入變量、鎖存器、與門的變量下標和定義位置上做出了限制。
首先定義輸入變量的下標，接着是定義鎖存器的pseudo-primary input(偽初始輸入)的下標，
最后是定義與門的左值(LHS)文字的下標
input variable indices 1, 2, ... , I
latch variable indices I+1, I+2, ... , (I+L)
AND variable indices I+L+1, I+L+2, ... , (I+L+A) == M
與上面對應的無符號文字分別是
input literals 2, 4, ... , 2*I
latch literals 2*I+2, 2*I+4, ... , 2*(I+L)
AND literals 2*(I+L)+2, 2*(I+L)+4, ... , 2*(I+L+A) == 2*M
所有文字必須被定義，因此必須嚴格滿足等式M=I+L+A。有了這條限制，我們可以省略鎖存器的當前狀態文字。
因此，在header行之后，緊接着是L個下一狀態文字，每行一個，分別代表一個鎖存器。
然后是O個輸出文字，也是每行一個。
在二進制格式中，與門的排列是有序的，遵循父子關系。與門的左值文字比較小的排列在前面。
一個與門的右值文字都要比它的左值文字要小。
我們可以將一個與門的右值文字排序，將較大的文字排在前面。例如下面的與門定義：
lhs rhs0 rhs1
其中lhs是偶數，並且lhs>rhs0>=rhs1。
為了防止組合邏輯自循環(combinational self loops)，變量下標被設置成兩兩不同
因為所有與門的左值(LHS)文字是連續的(偶數)，所以在二進制格式的文件中，我們不需要保存LHS。
根據上述描述，我們可以只用delta0和delta1表示一個與門(binary delta encoding,二進制增量編碼)，其中：
delta0 = lhs-rhs0, delta1 = rhs0-rhs1
這兩者都不會是負數，且數值比較小，當使用簡單的小端編碼時會有優勢。
定義完與門之后，便是可選的符號表和注釋部分(和ASCII格式一樣)
8.二進制增量編碼
假設w0,...,wi都是7位比特的文字，w1,..wi均不為0，且無符號整數x能夠表示為
x = w0 + 2^7*w1 + 2^14*w2 + 2^(7*i)*wi
則x在AIGER格式中可以用二進制編碼為i個字節序列b0,b1,b2,...,bi：
b0,b1,b2,...,bi = 1w0, 1w1, 1w2, ..., 0wi
序列中每個字節的最高有效位(MSB)用來指示該字節是否為此序列的最后一個字節。示例如下：
unsigned integer byte sequence of encoding (in hexadecimal)
x b0 b1 b2 b3
0 00
1 01
2^7-1 = 127 7f
2^7 = 128 80 01
2^8 + 2 = 258 82 02
2^14 - 1 = 16383 ff 7f
2^14 + 3 = 16387 83 80 01
2^28 - 1 ff ff ff 7f
2^28 + 7 87 80 80 80 01
這種編碼最多可以減少4倍的字節數，特別是文件中的含有大量數值較小的整數時。
這種對任意精度無符號整數的二進制編碼與平台無關，因此是64位機器完全支持。
以下C代碼可以用來表明這種編碼-解碼方法非常方便，但該方法無法運行，其中存在棧溢出和文件錯誤。
unsigned char
getnoneofch (FILE * file)
{
int ch = getc (file);
if (ch != EOF)
return ch;
fprintf (stderr, "*** decode: unexpected EOF\n");
exit (1);
}
unsigned
decode (FILE * file)
{
unsigned x = 0, i = 0;
unsigned char ch;
while ((ch = getnoneofch (file)) & 0x80)
x |= (ch & 0x7f) << (7 * i++);
return x | (ch << (7 * i));
}
void
encode (FILE * file, unsigned x)
{
unsigned char ch;
while (x & ~0x7f)
{
ch = (x & 0x7f) | 0x80;
putc (ch, file);
x >>= 7;
}
ch = x;
putc (ch, file);
}
不檢查讀取的字符是否為EOF可能會導致無限循環。在AIG文件的二進制格式中，讀取上述的二進制編碼序列需要一次性讀完，如果沒有讀完序列就遇到了EOF，則會發生解析錯誤。解決方法是檢查getc返回的字符，若是EOF，則終止解析。
9. 性質檢測(property checking)
AIGER格式可以方便地用於各種類型的性質檢測。
我們可以強制一個不包含鎖存器、且只含一個輸出的組合邏輯電路輸出為1，這是對SAT問題的編碼。
驗證時序邏輯電路上的安全性質的模型檢測問題也可以進行同樣的編碼。
若是為了驗證liveness，我們可以將每個輸出解釋為公平約束。
一種能夠找出給定公平約束所對應的一個可達公平循環(reachable fair cycle)的算法可以用來對LTL性質進行模型檢測。
接下來我們計划使AIG文件能夠支持PSL性質的描述。
當前僅允許電路輸出作為原子特性。
可以通過引用符號表中所定義的符號名來引用輸出文字。
10. Vectors, Stimulus, Traces, Solutions and Witnesses
此節給出了性質檢測問題中的traces和solutions的語義和語法。
具體而言，此節只考慮結構化SAT求解問題和壞態檢測問題。
本質上，一個有效的solution是一個輸入向量(vector)組成的列表(list)。輸入向量包含三種值0,1,x。該solution是一個有效的witness，當且僅當將x用0或者1實例化之后，AIG文件的二值模擬能夠輸出至少一個1(假設AIG文件是從全為0的初始狀態出發的)。
對於結構化SAT求解問題，AIG文件中不包含鎖存器，這種情況下只需一個輸出就足夠了。
原則上，在部分二值輸入已賦值的情況下，可以用三值邏輯來模擬AIG文件。
三值邏輯中使用到了0,1,x，三值邏輯的邏輯操作如下：
a !a & 0 1 x
0 1 0 0 0 0
1 0 1 0 1 x
x x x 0 x x
一個大小為n的值向量(vector of values)是一個具有n個三值常量的列表，使用長度為n的ASCII碼字符串表示，每個字符可以為0， 1或者x。
給定一個AIG文件的，其類型表示為M I L O A。它對應的一個輸入向量大小為I，輸出向量大小為O，狀態向量大小為L。
AIG文件的一個stimulus是一個輸入向量的列表。一個stimulus對應的文件是一個多行ASCII字符串，每一行字符串用一個換行符分隔，文件末尾使用一個換行符結束。
一個transition一次包含當前狀態、輸入、輸出和下一個狀態向量。一個transition是與給定的AIG邏輯一致的，如果模擬的結果是當前狀態向量在三值邏輯中的輸入向量產生給定的輸出和下一個狀態。在ASCII表示的transition中，四個向量的字符串用空格字符隔開，兩個字符串之間正好是一個空格。這意味着“L=0”組合電路的transition的開始和結束都是一個空格；沒有輸入的組合電路以兩個空格開始。
一條trace由一個transition列表構成。若一條trace中的所有transition是連續的，且所有transition(除第一個外)的當前狀態向量是和之前的transition的下一狀態向量相同，則稱該trace是連續的。若一條trace中的第一個transiton的當前狀態向量只包含0，則稱這條trace已被初始化。trace文件中一個transition占據一行，使用換行符分隔和標識文件結束。
因此，simulator將AIG和匹配AIG類型的stimulus作為輸入，並生成一個初始化的連續trace。一個隨機simulator將使用隨機輸入向量，不需要stimulus。
x值不應解釋為don't care。例如，如果將文字l賦值為值x，則l & !l在三值模擬中會產生x，而不是0。這個三值邏輯標准的語義允許在對輸入進行全局三值分配的情況下對電路進行線性時間模擬。模擬二值邏輯中的部分賦值，也就是檢查輸出是否固定到某個值，是一個NP完全問題。另一方面，三值模擬是純粹的句法，優化AIG不需要保留三值模擬語義。
由於三值模擬的句法性質，我們可以定義grounded stimulus的概念，也就是不包含x值的stimulus。一個stimulus是另一個stimulus的實例，如果前者與后者(在后者包含x的對應位置以外)都相同。前者可以是(0、1或x)這三個值中的任何一個。
一個witness指的是系統可以產生一個壞態bad state。
一個SAT求解問題的solution是一個文件，該文件包含一行驗證結果(a result line)和一個可選的stimulus部分。驗證結果若是一個0則指示該AIG文件無法輸出1；無效的驗證結果行或空文件被解釋為未知(無法驗證)；結果若是為1，則產生一個壞態的witness。