AIGER檔案格式(翻譯)
AIGER
1. 介紹
AIGER是AIG()And-Inverter Graphs)的檔案格式的代稱，是瑞士境內阿爾卑斯山的一座山峰。AIGER格式CAV2007模型檢測競賽提供了一種簡潔明瞭的檔案格式。
AIGER檔案格式含有ASCII格式和二進位制格式兩個版本。當一個應用沒有使用AIGER庫時，可以生成ASCII格式的AIG檔案。
二進位制格式更加簡潔，格式更嚴謹，是基準測試和競賽所採取的格式。生成二進位制格式AIG檔案有兩種方法，第一種是用AIGER庫直接生成，第二種是使用aigtoaig工具將ASCII格式轉換成二進位制格式(反過來也行，因此也將此工具用來驗證二進位制格式AIG檔案的正確性)。
在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和額外的低電平復位訊號作為輸入，實現了上述振盪電路
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。