作者ckmarkoh (阿傑)
看板EE_DSnP
標題Re: [討論] 將FEC pairs用SAT證明
時間Fri Jan 14 14:28:26 2011
每發現一個SAT equivalence 進行化減以後
就要更新一次存FEC pair的資料結構
例如現在有 A B C D是FEC pair, 而C在B的fanin裡面
A和B已證明相等 把B和A merge以後 保留A 那麼C也會被刪掉
如果沒有更新FEC pair 的話
iterator會指到已經被刪除的gate
還有 如果是B和C merge的話 一定要保留C
否則就會形成loop
不過 在做SAT之前 需要找出B和C各別的子電路
所以應該是可以發現C是在B的fanin裡面
--
※ 發信站: 批踢踢實業坊(ptt.cc)
◆ From: 140.112.4.170
1F：→ BBSealion:第一個情況 刪B時 可以不要把C刪掉吧 merge只刪掉自己 01/14 15:23
2F：→ BBSealion:他的fin是沒用了沒錯 但要刪你就要沿路砍回去到pi為止 01/14 15:23
3F：→ BBSealion:我是沒有做這個麻煩事啦XD 至於不砍的話SAT確實會浪費 01/14 15:23
4F：→ BBSealion:時間做他 但起碼不會Crash或loop 01/14 15:23
5F：推 BBSealion:我是盡量把找和砍分開做 找到先通通回報出來 最後一起砍 01/14 15:30
6F：→ BBSealion:不過現在變成跑很慢 我還在想這樣的overhead多大... 01/14 15:31
7F：→ ckmarkoh:因為我的gate都有存fanout 所以該砍的就要砍乾淨 01/14 15:36
8F：→ ckmarkoh:即使沒有存fanout, 如果這個gate的fanout被砍了 01/14 15:40
9F：→ ckmarkoh:就成了floating gate了吧? 是否會有memory leak的問題? 01/14 15:41
10F：→ ckmarkoh:更正 如果還有pointer指到這個gate是不會有memory leak的 01/14 15:44
11F：推 BBSealion:喔 我也有存fanout 所以以這例子 我會把C中的fanout拿掉 01/14 16:37
12F：→ BBSealion:一個 也就是到B的這個 如果C還有其他fanout才會維持正常 01/14 16:37
13F：→ BBSealion:等C都確定沒有fanout才該拿掉他 不過我沒做最後這步 01/14 16:38
14F：→ BBSealion:變floating會出問題嗎？ 本來就會有floating吧 不然為何 01/14 16:39
15F：→ BBSealion:要 report floating呢 都砍完了XD 01/14 16:39
16F：推 BBSealion:剛想到比較麻煩的是大家的一致性 我下篇題了一下這問題 01/14 16:43
17F：推 ric2k1:我是覺得先 check B or C 應該都不至於會發生問題， 01/15 00:43
18F：→ ric2k1:我也有存 fanouts, 我也是先找到一定數目的 UNSAT 之後再 01/15 00:44
19F：→ ric2k1:做 merge. 只是 merge 之後要重新 collect 一些 circuit 01/15 00:45
20F：→ ric2k1:information, 像是 DFS, FEC pairs, floating cells, 等等 01/15 00:46
21F：→ ric2k1:後面這些 info 重新收集應該會比隨時去 maintain 來得容易 01/15 00:47
22F：→ ric2k1:且有效率。 01/15 00:48