Configuration pins and tied-off inputs shrink the input space. Both sides must apply the same tie-offs before comparison, or constants compare as divergences.
A proved tie-off propagates into the cone and simplifies it. The proof then covers the smaller space exactly.
Tie-off | Space | Proof covers |
|---|---|---|
No ties, 3 inputs | 8 vectors. | All 8 vectors. |
One pin tied, 2 free | 4 vectors. | The 4 vectors with the tie applied. |
Two pins tied, 1 free | 2 vectors. | Both values of the free pin. |
Some vectors cannot occur: a one-hot bus never shows two bits set, and a mode pin never toggles in mission logic. Treating them as comparable creates false failures.
Each unreachable case needs a stated constraint on both sides. Without it the solver flags a vector the design never sees.
Unreachable case | Constraint | If omitted |
|---|---|---|
Two-hot on a one-hot bus | At most one bit set. | A false divergence on two-hot vectors. |
Illegal mode code | Mode stays within valid codes. | A false divergence on unused codes. |
Reset-active plus enable | Enable is low during reset. | A false divergence on the overlap. |
On three inputs every vector can be enumerated directly. The program below replays the RTL against the mutated block from the previous lesson over all eight vectors.
import sys
def gold(a, b, c):
return (a & b) | ((1 ^ a) & c)
def mutated(a, b, c):
return (a & b) | (a & c)
bad = []
agree = 0
for a in (0, 1):
for b in (0, 1):
for c in (0, 1):
g = gold(a, b, c)
m = mutated(a, b, c)
if g == m:
agree += 1
else:
bad.append((a, b, c, g, m))
if not len(bad) == 3:
print("FAIL: want 3 differing vectors, got " + str(len(bad)))
sys.exit(1)
if not agree == 5:
print("FAIL: want 5 agreeing vectors, got " + str(agree))
sys.exit(1)
if not (gold(0, 0, 1) == 1 and mutated(0, 0, 1) == 0):
print("FAIL: vector 001 must give RTL 1 and mutated 0")
sys.exit(1)
if (0, 0, 1, 1, 0) not in bad or (0, 1, 1, 1, 0) not in bad or (1, 0, 1, 0, 1) not in bad:
print("FAIL: differing set must be 001, 011 and 101")
sys.exit(1)
print("PASS: 8 vectors give 5 agreements and 3 differences at 001, 011 and 101")The program visits each vector once through nested loops over 2 by 2 by 2. Its checks pin the agreement count, the difference count, and all three differing vectors.
input space doubles per free input: 2^1 = 2, 2^2 = 4, 2^3 = 8, 2^4 = 16
3 inputs enumerate as nested loops: 2 x 2 x 2 = 8 vectors
brute force visits every vector once, so no case is skippedFour. Two free inputs give 2^2, which is 4 vectors with the tie applied.
All three have c=1 with a and b not both 1. At c=1 the RTL gives b when a=1 and 1 when a=0, while the mutated block gives b OR c when a=1 and 0 when a=0, so they agree only at a=1 and b=1.