※ 引述《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
不過也不是很強就是了...