作者yan12125 (姥姥)
看板EE_DSnP
標題[問題] Updating by SAT???
時間Sat Jan 12 17:52:23 2013
跑cirfraig的時候，ref最後面都會有一行Updating by SAT... Total #FEC Group = 0
我原本以為是把SAT的pattern蒐集起來，再simulate一遍，但結果跟我想的不一樣？譬如
說：
(my.aag)
aag 9 2 0 2 2
2
4
6
8
6 3 5
8 7 2
(my.pattern)
11
(執行結果)
fraig> cirr my.aag
fraig> cirsim -f my.pattern
Total #FEC Group = 1
1 patterns simulated.
fraig> cirg 1
==================================================
= PI(1), line 2 =
= FECs: =
= Value: 0000_0000_0000_0000_0000_0000_0000_0001 =
==================================================
fraig> cirfraig
Proving (3, !4)...SAT!!
Updating by SAT... Total #FEC Group = 0
fraig> cirg 1
==================================================
= PI(1), line 2 =
= FECs: =
= Value: 0000_0001_0001_1000_0100_1101_0010_0000 =
==================================================
fraig> q -f
fraig之後cirg 1的value應該是從SatSolver::getValue()得到的吧？但是getValue()
一次只能拿到一個bit吧？不知新的simulation pattern是用什麼神奇的方法得到的？
或是我其他地方理解有誤？
--
昔我愛泉石 長揖離公卿 結屋青山下 咫尺蓬與瀛
至人不可見 世塵忽相攖 業風吹浩劫 蝸角爭浮名
偶逢大呂公 如有夙世盟 相從語寥廓 俯仰萬慮輕
--
※ 發信站: 批踢踢實業坊(ptt.cc)
◆ From: 140.112.241.234
推 ric2k1:反正其他的 bits 也沒有要用，隨便塞一些值應該沒有關係吧! 01/12 22:04
→ yan12125:亂塞的？(驚) 01/12 22:38
推 ric2k1:對啊，fraig 在 sim 的時候其他的 bits 應該是什麼值都 01/12 22:57
→ ric2k1:無所謂吧! 反正是 parallel sim. 01/12 22:58
→ ric2k1:我是指 input patterns 啦! 01/12 22:58
→ yan12125:原來如此～ 01/12 23:06