※ 引述《goodword (佳话)》之铭言：
: 大家好~
: 和 TR 奋斗了两天...
: rtl 也已经改到相当简单 (只有3楼)
: 一开始还是再建时 还是跑不出来
: 但我又再做了一些简化 让总 dff = 18 个
: 然后我有观察在 tri &= (yi == δi(X,I)); 时 tri 总node的变化
: 在第10个iteration时 total tri node = 39427 (可看作只有10个dff)
: 在第15个iteration时 total tri node = 189972
: 而我的design 有18个dff 最后total tri node = 1519496
: exist 完后的 tr node = 10874
: 这真的要跑满久的...
: 上面这个简单的case 大概要跑2分钟
: 所以我想 像这样的design 可能最多只能有20多个dff
: 因为 tri node 大致是以指数增加
: 所以太多的 dff 我认为建不太起来了
: 一点点心得给大家参考
感谢分享。
BDD-based verification 只能用在 #dff 小于 20 的电路是有点夸张，
如果真的是这样的话 80 ~ 90 年代用 BDD 在作研究的人可能都要切腹了 XD
我绝不是说大家的程式写得不好，
事实上是如果只用最阳春的算法 (就是上课教的基本款啦)，
的确很可能就只能做到这样。
不过像是以前我们 (Verplex) 的 tool 甚至是现在许多的 verification tools，
BDD 还是有它可以发挥的空间的。
大家应该可以想像我们是花了很多的力气在 tune BDD 的 performance 以及 capacity，
课堂上有提到的像是 "early quantification"，"conjunctive/disjunctive partitions"
"restrict", 等等，都会视情况运用上去。
TRI 事实上我们是没有在建的，因为它通常会大很多，
而且在做 reachability 的时候用不到，
不过当我们要真正建 counter-example 的时候我们会再针对目前的 X & Y 值
用 BDD 找出一组 PI assignment。
有兴趣的人也可以 try 一下一套非常成熟的 BDD package (CUDD):
http://vlsi.colorado.edu/~fabio/CUDD/
Download 下来后他有一个程式 "nanotrav" 可以做 state traversal
不过也不是很强就是了...