感謝回答。
我有另一個有關於property checking的問題。
在做property checking的時後，我用reference code作測試，以counterBit2為例，
如果我設定property是!(00)，會output 0:11，其中0當然就是因為一開始的state是
00，因此property fail，但後面的11似乎可以用任何input組合取代。範例的
porperty我也遇到類似的問題，就是最後一組input assignment感覺用什麼都可以(？)
，因為這時候已經reach到!p的state了？
在simulation部分，由於DFF的值會在"這一個"cycle計算好，然後在"下一個"cycle
才更新，如果property fail出現在第n次的simulation，應該是表示前面n-1個input
所造成的，這樣的話，第n次simulation給的值應該也就不重要了(？)。一樣用
counterBit2所給的do file為例，其中p2，感覺給兩個input就會reach到property fail
的state(10)，可是reference code得到的counterexample會有三組input，而且
simulation時也需三次simulation才會觀察到property fail，但似乎最後一組其實是
什麼都可以(？)
※ 引述《ric2k1 (Ric)》之銘言：
: ※ 引述《kaie819 (kaie)》之銘言：
: : 有關於作業四目前遇到了幾個問題
: : 1. 我想要建立DFF fanin cone的BDD，看CirGate的資料結構，可以藉由CirGate[0]得到
: : fanin gate，可是實際這樣用卻得到的是自己這個DFF(？)，如果要得到fanin cone，必須
: : 要用CirGate[0][0]，這樣做出來感覺是對的，但不知道是否合理？(二維？)
: 你確定你的 gate 是 DFF 嗎? 看來有可能是 PO gate 哦?
: I wrote the following test code, and the output looks fine.
: for( unsigned i = 0, n = _dffList.size(); i < n; ++i ) {
: cout << i << ": " << endl;
: cout << _dffList[i]->getTypeStr() << endl;
: cout << (*_dffList[i])[0]->getTypeStr() << endl;
: }
: ======= for alu2.v =======
: 0:
: DFF
: AND
: 1:
: DFF
: AND
: ....<略>
: 7:
: DFF
: AND
: : 2. 作業題目有關於PTR的部份TR和TRI順序好像跟程式不一致
: : 題目是PTR TR TRI; 程式是PTR TRI TR
: 啊... 寫反了。
: 改題目好了，比較單純。
: 就是改成 PTR [triName][trName]
: : 3. 有關於BddNode exist()的功能，不知道大家有沒有問題，我用了不會作existential
: : quantification...(e.g., _tr.exit(2);)，這個功能應該不需要自己implement吧？
: : 不知道有沒有人可以幫我解答一下~
: Yes, the prototype for exist() is:
: BddNode exist(unsigned l) const;
: That means, _tr.exist(2) will return a existentially quantified BDD,
: but itself won't get changed (i.e. This is a constant method).
: So you should use something like "a = b.exist(2)".
: Of course, "_tr = _tr.exist(2)" works fine too,
: if that's what you intened to do.