我丟一個我自己寫的aag file：
aag 4 2 0 2 2
2
4
6
8
6 2 4
8 2 5
模擬的pattern：(00跟10各重複32次)
00
....
00
10
....
10
第一輪模擬完AIG 3和AIG 4都是0000_0000_0000_0000_0000_0000_0000_0000，
cirp -fec應該像這樣：
[0] 0 3 4
第二輪模擬AIG 3=0000_0000_0000_0000_0000_0000_0000_0000，
AIG 4=1111_1111_1111_1111_1111_1111_1111_1111
這時./ref/fraig給出cirp -fec的結果是：
[0] 0 3 !4
第一輪模擬後3跟4在同一組，只要之後任何模擬的結果不一樣，兩個gate就要分成
兩組吧？

因為 00...000 與 11...111 是 inverse FEC，所以還是會被放在同一組，只是加上 ! 變成 !4

我的想法是：如果兩個gate equiv. ，則所有的input都會使結果相同，而如果是inverse equiv. ，則所有的input都會結果完全相反，因此對於已知的兩個gate，如果存在兩組input分別使結果完全相同與完全相反，則這兩個gate既不是equiv. 也不是inverse equiv. ，那就沒有必要繼續留在functionally equivalent "candidate" pairs裡吧？

你這麼說的確有道理，ref prog 的確沒有把這個因素考慮進去我等一下有空來改一下。

推！

不過我又想了一下，在正常的 parrallel pattern 模擬底下兩個 gates 要前一次 32 個 patterns 是 eq, 下一次 32 個patterns 是 inv-eq 的機率幾乎是 0, 為了這樣去改變我收集FEC pairs 的機制似乎不太划算，所以我就不改了。我們在測的時候會注意不要讓這樣的情形發生。

XD 我亂數產生10000個gate的電路+65行的pattern file10幾次就出現了似乎32k+1個pattern時比較容易出現

不懂... 不過基本上這不會影響 FRAIG 的正確性。也許在某些case 會讓 cirp -FEC 不夠精確，但我想 sim 的重點還是要快而且夠就好，誤判的情形就交給 SAT，整體來說應該是比較好簡單的說，如果前面 32n 個 parallel patterns讓兩個 gates的反應一樣，但下 32 個亂數的 parallel patterns 卻讓

嗯 了解

這兩個 gates 的反應正好反向，這樣的電路真的是太奇怪了，都給 SAT 去解 SAT(f == g) // 因為反向應該會一下子就解出來了，所以也不會有什麼 overhead但為了要檢查這種情形，以我目前的 implement 來說卻要多記/多傳一些東西，我覺得是不值得的。

感謝老師！問個小問題，讓我獲益良多其實就算中間被誤判歸類為inverse FEC，最後還是會被分開simulation pattern數量增加結果就一樣了