※ 引述《hschiang (hschiang)》之銘言：
: 不好意思再問一個問題
: 題目上說 property violate 時要印counter example
: 可是格式看不太懂
: 是要把所有會讓_reachStates&monitor為真的input + state都列出來吧
我重新看了一下題目說明文件
似乎沒特別提到要印出state
以ref program來說.也只有印出input而已
因為給定一個transition是deterministic的design
決定了input應該也同時決定了state的變化(從initial state開始)
: 可是
: ref program 執行Traffic.dofile 的結果
: 卻是連續輸出43個1
: 0:1
: 1:1
: .
: .
: .
: 42:1
: 好像和題目上寫的
: 0: 1'b0 4'b0000
: 1: 1'b0 4'b0001
: 2: 1'b1 4'b1010
: 不太一樣
: 是我哪裡理解有問題嗎?
至於格式問題.是的確實不太一致(差別在bit-width資訊上)
你要採用哪種皆可(但應該reference的格式對實作比較方便)
順便一提.印出的順序是照ntk裡存input,inout的順序
由於這個說明檔是從去年的檔案改的
當初沒注意到這個部份而做更改造成你的困擾不好意思
而有更改的原因主要是去年把BDD做在(假)word-level上
而今年則都在aig上操作
要拿到相應的資訊應該比較麻煩.所以就沒特別印出bit-width的資訊
以上.希望有解決你的疑惑