RE: mantis 4144

OK, I'll see what I can do before the next round of voting. The LRM is not supposed to be a user's guide, and we could get into a deep hole trying to explain how constraint probabilities work.
________________________________________
From: owner-sv-xc@eda.org [owner-sv-xc@eda.org] on behalf of Kaiming Ho [kaiming.ho@iis.fraunhofer.de]
Sent: Wednesday, July 11, 2012 12:24 AM
To: Rich, Dave; sv-xc@eda.org
Subject: mantis 4144

Hello Dave:

   I've looked at your proposed change to 18.5.10 in mantis 4144.
The example illustrates subtleties in the way the constraint solver
works which are still misunderstood by many people. Including a
table of valid solutions, and their probability of occurrence in the
LRM would be educational. One finds this approach in training slides
or papers outlining SV 'gotchas'.

   Please consider adding the following after the first paragraph.

| The following table illustrates the valid solutions of {s,d} which
| satisfy the constraint, and the probability of occurrence of each
| s d prob
| 1 0x00000000 1/(1+2^32)
| 0 0x00000000 1/(1+2^32)
| 0 0x00000001 1/(1+2^32)
| 0 0x00000002 1/(1+2^32)
| 0 ...
| 0 0xfffffffe 1/(1+2^32)
| 0 0xffffffff 1/(1+2^32)

   In place of the entire second paragraph, I'd like to suggest something
like:

| In this case, the order constraint instructs the solver to solve for s
| before solving for d. Adding this order constraint does not change
| the set of valid solutions, but alters their probability of
| occurrence.
| s d prob
| 1 0x00000000 1/2
| 0 0x00000000 1/2 * 1/2^32
| 0 0x00000001 1/2 * 1/2^32
| 0 0x00000002 1/2 * 1/2^32
| 0 ...
| 0 0xfffffffe 1/2 * 1/2^32
| 0 0xffffffff 1/2 * 1/2^32
|
| Note that the probability that d==0 without the order constraint
| is 2/(1+2^32), and is 1/2*(1+2^32) with the order constraint.

regards,
kaiming
Received on Fri Jul 13 14:23:37 2012