推 wmin0:謝謝教授的回答!! 12/30 00:47
: 聽完課還是有點問題 所以又來PO版了 囧"
No problem.
:
: 一 關於 Fraig Proof
:
: 我還是不了解有了 FEC pairs 之後要找多深去 proof 是不是 FEC
: 要一個一個 fanin level 去試
: 還是只是從那個 gate 到 fanin 整串 ...
是的，從 FEC gates (f, g) 到 PIs 整個 cone of gates 都要轉成 CNF，
然後再把 (f, g) 兜出一個 XOR 的 CNF 丟給 sat 去解。
: 如果是這樣
: 那嵌在中間的 FEC 就算了?
所以說最好從靠 PI 端的 FEC 開始證，
否則中間的 FEC 就沒有意義了。
:
:
: 二 還是 Fraig Proof
:
: 當 sat 的時候似乎要拿現在這個結果再去 simulate
: 範圍呢? 所有的 FEC pair or current FEC pair ...
:
current pair 都被證明 sat (i.e. different) 了，
所以應該是 simulate 整個電路吧 (all FEC pairs).
: 應該要 collect 夠多的 sat 才去 simulate 吧
: 否則似乎有點浪費?
是啊! 可以 collect 到足以湊成一個 parallel pattern.
:
: 三 關於 Fraig Merge
:
: 看 ref 的 output 似乎只 merge 最上面那個 Gate
: 有需要 recursive 的向下處理 fanout 變成 float 的 Gate嗎
可以不用，事後用 cirsweep 去掃掉就好了。
:
:
: 四 關於 CirPrint -FEC
:
: ref 似乎只有對 FEC pair 裡面 sort
: 整個 FEC pair list 也要不要 sort ?
: 純粹是 diff 上的需求...
這要每個 group 裏頭的 ID 按照順序排就好了。
(see commnad "CIRPrint")
:
:
: 五 關於 CirGate
:
: simulate value
: 先塞的會出現在最右邊
: 人從左邊讀過去感覺怪怪的 囧"
: 呃 這不重要 ...
因為右邊是 LSB...
:
:
: 六 心得 ...
:
: 合理懷疑老師前面在 parse gate 的時候就偷用了 hash ...
: 昨天發現 sim13.aag 餵不下去
: 在找有沒有 redefine error 的時候卡住 ...
: 改成 hash 版本快超多 ...
我沒有哦!
有很多方法可以快速地找到 parsing 的資訊，
像是用空間換去時間，array/index 等等.
其實像 aag 這種簡單 format 的 parsing 通常都不會想到要用 hash.
:
: HW6 明明沒 hash 這玩意兒啊啊 QQ
:
: --
:
: 後面部分不要理我 囧"
:
: 先感謝前面回答 Orz
:
: --
: ※ 發信站: 批踢踢實業坊(ptt.cc)
: ◆ From: 140.112.249.64
: ※ 編輯: wmin0 來自: 140.112.249.64 (12/29 17:08)
: → djshen:redefine看totGateList[gateId]有沒有東西就可以吧? 12/29 17:54
沒錯。
: → djshen:三 我覺得應該是留給sweep做? 12/29 17:55
Yes.
: → wmin0:沒用hash的話全搜是n^2 到5 6萬的時候就差很多... 12/29 18:07
: → djshen:應該是讀的時候就在totGateList裡面找 random access算快吧 12/29 18:09
: → wmin0:噢噢 原來一樓說的是map啊@@ 因為我只用vector存而已囧" 12/29 18:09
: → djshen:是array沒錯啊@@ 12/29 18:10
: → djshen:如果gateId對應到array裡面的位置就可以直接拿 12/29 18:11
: → djshen:如果沒有redefine就new一個gate在那個位置 我是這樣啦@@ 12/29 18:12
: → wmin0:恩恩 不過我當時沒想到這樣做@@" 呆呆地報搜 12/29 18:13
: → wmin0:用 hash 的話記憶體也不用噴這麼多掉XD 12/29 18:13
: → djshen:如果hash的value是gateID那就跟array一樣了@@ 12/29 18:16
沒錯。
不過 vector potentially 是會比 hash 吃多一點記憶體，
尤其是當你有需多 "空號" AIG gates 的時候。
但我覺得除非很誇張 (像是 M = 1,000,000, A = 1,000)，
否則我覺得用 vector 就好了。
--
※ 發信站: 批踢踢實業坊(ptt.cc)
◆ From: 114.36.58.251