[問題] Updating by SAT???

作者: yan12125 (姥姥)   2013-01-12 17:52:23
跑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是用什麼神奇的方法得到的?
或是我其他地方理解有誤?
作者: ric2k1 (Ric)   2013-01-12 22:04:00
反正其他的 bits 也沒有要用,隨便塞一些值應該沒有關係吧!
作者: yan12125 (姥姥)   2013-01-12 22:38:00
亂塞的?(驚)
作者: ric2k1 (Ric)   2013-01-12 22:57:00
對啊,fraig 在 sim 的時候其他的 bits 應該是什麼值都無所謂吧! 反正是 parallel sim.我是指 input patterns 啦!
作者: yan12125 (姥姥)   2013-01-12 23:06:00
原來如此~

Links booklink

Contact Us: admin [ a t ] ucptt.com