作者ric2k1 (Ric)
看板EE_DSnP
标题Re: [请益] 在sat merge
时间Tue Jan 17 02:39:21 2012
: 请问一下
: 做sat的时候如果把gate merge掉了
: 那麽原本建立的var id之间的关系要如何处理呢
: 例如const0要merge aig 4
: aig 4被砍掉之後是用assumeProperty来处理aig 4的var id吗?
电路上就用与 strash 相同的方法来 merge 两个 gates,
被 merge 的 gate 我是只有 delete 掉它本身，没有去管它的 transitive fanins,
所以有可能会造成 floating cells, 反正 fraig 完再呼叫 cirsweep 就好了。
至於是不是证完一个 FEC pair UNSAT 就马上 merge，
我是没有啦! 因为改了 netlist 之後就改 FEC groups, 以及 DFS list,
这样有点得不偿失。
不过完全不 merge (等到证完再 merge) 其实也不好，
就找个 balance 罗!
另外就是在 SAT 方面，
当两个 gates 被证明是相等的时候，
SAT engine 会 learn 起来这件事情，
所以除非你 reset solver, 否则後来的 assumpSolve 都会有这样的资讯。
这叫做 "incremental SAT"，如果你没有用的话保证你会证很慢，
因为前面证的後面没有用到，那相当於证明的 cone 越来越大...
p.s. 其实 SAT 证明过程还有 learn 到很多东西，他都有记下来。
: --
:
※ 发信站: 批踢踢实业坊(ptt.cc)
: ◆ From: 111.249.189.38
: → victoret:个人是没有重新接...反正一样的就是一样。 01/16 13:11
: → victoret:我是说 SAT 里的东西...不过不知道重新接会不会比较快？ 01/16 13:12
: → victoret:因为目前还没重接拆...sim12 崩溃...但是也不确定接了速 01/16 13:12
: → victoret:度上有没有帮助 @@ 01/16 13:13
: 推 ntueesuevan:sim12崩溃+1 01/16 15:49
: → wmin0:我的做法是每次把solver reset 重接... 01/16 18:55
: 推 victoret:请问要重接一定要 reset 吗？还是有什麽指令可以直接重设 01/16 21:34
: → victoret:某个 gate 的 fanin？ 01/16 21:34
: → wmin0:召唤教授... 01/16 21:45
每次 solver reset 的话之前 learn 的东西就都不见了，
通常是不好...
--
※ 发信站: 批踢踢实业坊(ptt.cc)
◆ From: 114.36.61.155
1F：→ djshen:sat.h里面写 for incremental proof, use assumeSolve 01/17 02:50
2F：→ djshen:可是他又clear 所以assumpSolve才是incremental proof? 01/17 02:51
3F：→ ric2k1:clear() 只有清掉 assumption 而已，之前的 proof mode 01/17 03:08
4F：→ ric2k1:以及 learned info 都不会被清掉。 01/17 03:08
5F：→ djshen:我眼花了 根本就没有assumeSolve= = 打错字无误 01/17 03:16
6F：→ djshen:sat 68行 01/17 03:16