Re: [問題] Counter Example

看板 Giee_Soc_V
時間
留言 1則留言,1人參與討論
推噓 1推 0噓 0→
: 不好意思再問一個問題 : 題目上說 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的資訊 以上.希望有解決你的疑惑 --
1Fhschiang:懂了,謝謝助教 04/21 06:37
看更多 keyboardle 的文章,或回到 GIEE_SoC_V 看板