作者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
1F：推 ric2k1:反正其他的 bits 也没有要用，随便塞一些值应该没有关系吧! 01/12 22:04
2F：→ yan12125:乱塞的？(惊) 01/12 22:38
3F：推 ric2k1:对啊，fraig 在 sim 的时候其他的 bits 应该是什麽值都 01/12 22:57
4F：→ ric2k1:无所谓吧! 反正是 parallel sim. 01/12 22:58
5F：→ ric2k1:我是指 input patterns 啦! 01/12 22:58
6F：→ yan12125:原来如此～ 01/12 23:06