※ 引述《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的资讯
以上.希望有解决你的疑惑