Hi Erik, Yes, I was thinking along the lines that if this example was included, that there should be some note that the property was written this way only for reducing the formal proof complexity, and that users' should not expect the constraint to generate the correct simulation data. Tom Seligman, Erik wrote On 09/27/07 10:54 AM,: > >>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? -- ------------------ Thomas J. Thatcher Sun Microsystems 408-616-5589 ------------------ -- This message has been scanned for viruses and dangerous content by MailScanner, and is believed to be clean.Received on Thu Sep 27 14:30:25 2007
This archive was generated by hypermail 2.1.8 : Thu Sep 27 2007 - 14:30:33 PDT