Bidirectional Solving

Implication is a filter, not an if-statement

The constraint a -> b reads like procedural code ("if a then make b true") but means something different: it removes every tuple where a is true and b is false . Logically it is !a || b. Crucially, the surviving tuples include ones where a is false — and if making b true is impossible or rare, the solver will prefer tuples where a is false . The implication has constrained its own antecedent. That is bidirectionality: every constraint shapes every variable it mentions, in both directions.

class backward;
  rand bit [3:0] a;
  rand bit [3:0] b;
  constraint c {
    (a == 5) -> (b == 100);   // b is 4 bits: b==100 is IMPOSSIBLE
  }
endclass
// Procedural reading: "a can be anything; if it lands on 5, set b=100."
// Solver reality: tuples with a==5 require b==100, which no 4-bit b
// satisfies -> ALL a==5 tuples are removed.
// Result: a is NEVER 5. The implication constrained a backwards.

This backward pressure is the single most-tested solver behavior in interviews, usually via the joint-distribution question worked out below.

The classic: (x==0) -> (y==0) joint distribution

One rand bit x, one rand bit y, single constraint (x==0) -> (y==0). Question: what is the probability of each (x, y) combination? Enumerate the four tuples and filter:

JOINT DISTRIBUTION OF  (x==0) -> (y==0)    [== !(x==0) || (y==0)]

   x  y | implication check          | legal? | probability
  ------+-----------------------------+--------+------------
   0  0 | antecedent T, consequent T  |  yes   |   1/3
   0  1 | antecedent T, consequent F  |  NO    |    0
   1  0 | antecedent F  (vacuous)     |  yes   |   1/3
   1  1 | antecedent F  (vacuous)     |  yes   |   1/3

  Marginals:  P(x=0) = 1/3        P(y=0) = 2/3
              P(x=1) = 2/3        P(y=1) = 1/3

  Procedural intuition said: "x is a fair coin (1/2), and y only
  gets forced when x==0."  WRONG: x is biased to 1, because x==0
  survives in only one tuple while x==1 survives in two.

The marginal P(x=0) = 1/3 — not 1/2 — is the punchline. The implication reduced the number of tuples in which x==0 can appear, so the uniform-over-tuples rule shifts probability toward x==1. No dist, no ordering — just set filtering.

module prove_it;
  class xy;
    rand bit x, y;
    constraint c { (x == 0) -> (y == 0); }
  endclass
  initial begin
    xy o = new();
    int n00, n10, n11;
    repeat (30000) begin
      void'(o.randomize());
      case ({o.x, o.y})
        2'b00: n00++;
        2'b10: n10++;
        2'b11: n11++;
        default: $fatal(1, "illegal tuple 01 generated!");
      endcase
    end
    $display("00:%0d 10:%0d 11:%0d", n00, n10, n11);
    // expect roughly 10000 / 10000 / 10000  (1/3 each)
  end
endmodule

Restoring the procedural intent with solve...before

If you wanted the procedural behavior — x a fair coin, y reacting — solve x before y delivers it. Ordering splits the solve into stages: first pick x uniformly over the values of x that admit at least one legal completion, then pick y uniformly among values legal given that x. The solution set is unchanged — tuple (0,1) is still illegal — but the probability mass moves.

class xy_ordered;
  rand bit x, y;
  constraint c   { (x == 0) -> (y == 0); }
  constraint ord { solve x before y; }
endclass

SAME CONSTRAINT, WITH vs WITHOUT ORDERING

  no ordering (uniform tuples)      solve x before y (staged)
  ----------------------------      --------------------------
  P(0,0) = 1/3                      stage 1: x in {0,1}, both
  P(1,0) = 1/3                               viable -> 1/2 each
  P(1,1) = 1/3                      stage 2: x=0 -> y must be 0
                                             x=1 -> y in {0,1}, 1/2 each
  P(x=0) = 1/3                      P(0,0) = 1/2
  P(x=1) = 2/3                      P(1,0) = 1/4
                                    P(1,1) = 1/4
                                    P(x=0) = 1/2   <- fair coin restored

  Legal tuples IDENTICAL in both columns.
  Only the WEIGHTS changed. Ordering never adds or
  removes solutions — it re-distributes probability.

Memorize both columns of that table. "1/3-1/3-1/3 without ordering, 1/2-1/4-1/4 with solve-before" is a complete senior-level answer to the most common solver interview question asked today.

Interview angle

What interviewers probe

• "(x==0)->(y==0): what is P(x=0)?" — expected: 1/3. Enumerate the three legal tuples; uniform over tuples biases x toward 1.

• "How do you make x a fair coin again?" — expected: solve x before y; staged solve gives 1/2, 1/4, 1/4.

• "Does solve-before change which values are legal?" — expected: never; it re-weights, the solution set is identical.

• "Constraint (a==5)->(b==100) with 4-bit b — what values can a take?" — expected: anything except 5; impossible consequents eliminate their antecedents backwards.

• "Is a -> b the same as if (a) b inside constraints?" — expected: the if/else constraint form and -> are equivalent filters; neither is procedural.

Strong candidates volunteer the equivalence a -> b == !a || b early — it signals you see constraints as Boolean algebra over the tuple space, which makes every backward-pressure question trivial.

Key takeaways

• a -> b is the filter !a || b — it removes (a true, b false) tuples and pressures a toward false when b is hard.

• (x==0)->(y==0) yields P(x=0)=1/3 under default uniform-tuple semantics — not 1/2.

• solve x before y restores procedural intuition: x picked first among viable values, then y given x.

• Ordering re-weights probability only; the legal solution set is bit-for-bit identical.

• Impossible consequents eliminate their antecedent values entirely — backward constraint propagation.

Common pitfalls

• Reading -> as a procedural if — predicting fair-coin marginals that the solver does not produce.

• Using solve-before hoping to FIX an unsatisfiable set — ordering never adds solutions; contradiction stays contradiction.

• Writing (a==5)->(b==100) style constraints with unreachable consequents — silently bans a==5 and nobody notices.

• Chaining implications both directions (a->b and b->a) without realizing you built an equality filter.

• Forgetting that if/else inside constraints is also declarative — both branches shape the space, no execution order.