[问题] 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