> 9. Note that example a would not work in simulation. In simulation, idx would be initialized to one value, which it would keep throughout the simulation. The corresponding bit of data1 and data2 would match, but the other bits would not. Actually, this is a feature, not a bug. I believe Dmitry's intent was that specifying it in this way ensures the formal proof will cover the general case, while reducing the burden on simulation. Each simulation will check the property for one (non-determinstic) bit; if a set of properties like this needs to exist on a large bus, this may allow much better simulation efficiency while effectively doing some random testing. Maybe we should explain this in more detail in the text? -- This message has been scanned for viruses and dangerous content by MailScanner, and is believed to be clean.Received on Thu Sep 27 10:54:59 2007
This archive was generated by hypermail 2.1.8 : Thu Sep 27 2007 - 10:55:06 PDT