Bound Refinement

Definition

In the context of hardware-accelerated constrained random test generation, bound refinement is the per-iteration operation that, after a value has been chosen for one variable $x_i$, recomputes the feasible interval $B_{x_j}$ of every still-unassigned variable $x_j$ (with $j > i$). The refinement uses the overlapping constraint set (OCS) of the strip that was selected for $x_i$ to eliminate from each remaining variable's range those values that cannot be combined with the just-assigned value while still satisfying the joint constraints.

The conceptual picture given in the methodology is that each variable's initial range is the union of strips — contiguous intervals in the variable's projection of the feasible polygon — and choosing a particular strip for $x_i$ restricts the other variables to the intersection of the polygon with the plane $x_i = \bar{x}i$. The new interval $B'{x_j}$ therefore satisfies $B'{x_j} \subseteq B{x_j}$, and the strip set for $x_j$ shrinks accordingly (for example, choosing a value $x_0$ for variable $x$ may reduce variable $y$'s boundary to strips $S_{y_1}, S_{y_2}, S_{y_3}$).

Where it is invoked

Bound refinement is invoked from the main generation loop GenerateSolution(CT, VT):

3.7: For each variables x_j in NGV (j > i) do
    3.7.1: RefineBound(X_i, OCS(S_{x_i}^k), x_i^linear, x_i^NGV).
    3.7.2: Update TWt_{x_j} by ReCompToW(x_i^linear, x_i^NGV, SetOfStrip(x_j), TWt_{x_j}).

After RefineBound narrows a variable's interval, ReCompToW recomputes the variable's total strip weight $TWt_{x_j}$ over the new (smaller) strip set, so that subsequent strip selection for $x_j$ is correctly weighted.

Purpose and correctness role

Bound refinement is what makes the sequential variable-by-variable procedure sound: as soon as a value is fixed for one variable, the intervals of the others are tightened to the cross-section of the feasible polygon at that value, so that no infeasible point is ever generated. Two complementary properties are established about the algorithm that relies on bound refinement:

Soundness (Theorem 4.1): if a valid valuation is chosen for the $k$-th variable, then a satisfying assignment for the $(k+1)$-th variable still exists, because the refined bound $B'{x{k+1}}$ is non-empty and is a subset of the previously feasible $B_{x_{k+1}}$.
Completeness (Theorem 4.2): every valid $n$-tuple $\bar{x} = (\bar{x}0, \ldots, \bar{x}{n-1})$ is generated with non-zero probability. The argument shows that fixing $\bar{x}k$ for variable $k$ cannot exclude $\bar{x}{k+1}$ from the refined bound $B_{x_{k+1}}$, since $\bar{x}$ itself satisfies all the constraints $a_{i1}x_k + a_{i2}x_{k+1} , \theta , a_{i3}$ in the $X_k X_{k+1}$-plane (including the OCS constraints $C_p, C_q$ of the strip containing $\bar{x}_k$).

Relation to other building blocks

Bound refinement sits between three other hardware/synthesis blocks of the methodology:

Strip and OCS pre-processing (software phase) — supplies, for every variable, the list of strips and the overlapping constraint set of each strip.
GenRandNum — generates a uniform random integer inside a given bound $[x^{\min}, x^{\max}]$ using a $k$-bit LFSR and a bit-flip fallback when the raw random number exceeds the interval width.
ReCompToW — recomputes the total strip weight $TWt_x$ after refinement, so that the next GenRandNum call correctly picks a strip in proportion to its weight.

Without bound refinement, the random strip selection and random value selection in steps 1 and 2 of the inner loop would pick values outside the feasible region; with it, every candidate $n$-tuple is automatically constraint-satisfying.