感谢回答。
我有另一个有关于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.