作者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