標題

Re: [問題] Counter Example

作者 keyboardle
看板 GIEE_SoC_V
時間 04-21
※ 引述《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的資訊 以上.希望有解決你的疑惑 -- ※ 發信站: 批踢踢實業坊(ptt.cc) ◆ From: 114.45.233.73
1Fhschiang:懂了,謝謝助教 04/21 06:37

討論串

標題 作者 日期 留言數量
[問題] Counter Example hschiang 2013-04-20T23:30:53 0
>> Re: [問題] Counter Example keyboardle 2013-04-21T05:30:46 1