The second half of interview arithmetic prices the engine's work and the assumptions' damage: how much the cone saves, how long a lasso must be, how big the unrolled problem grows, how much input space the assumptions removed. It closes with the two gate calculations: the mutation score and the bound justification.
Job of this lesson: make six more calculations automatic, ending with the two numbers that gate a signoff. Every figure here is illustrative unless it names a running design.
Four independent channels of 100 flops share 20 flops. A property on channel 0 sees 120 flops of 420: the state-space ratio is 2 to the 300, about 2.0 times 10 to the 90. Report the cone size per property; a shrunken cone is a disconnected property.
def cone(channel, shared, channels):
seen = channel + shared
total = channels * channel + shared
return seen, total
seen, total = cone(100, 20, 4)
assert (seen, total) == (120, 420), (seen, total)
ratio_log10 = (total - seen) * 0.30103
assert abs(ratio_log10 - 90.3) < 0.5, ratio_log10
# The failing variant: a design with one channel has a cone equal to the whole machine, so no saving.
try:
s1, t1 = cone(100, 20, 1)
assert (t1 - s1) * 0.30103 > 90
raise SystemExit("priced a saving for a single-channel design")
except AssertionError:
pass
print("PASS: cone of 120 of 420 flops, ratio 2 to the 300")A 3-bit counter plus a 2-bit state machine is 5 bits: at most 32 states, so any infinite counterexample repeats a state within 33 steps, and a search of that length must see the loop. The bounded-latency substitute uses window equals worst latency plus assumed stall bound, for example 4 plus 3 is 7.
def lasso_depth(bits):
return 2 ** bits + 1
def window(latency, stall):
return latency + stall
assert lasso_depth(3 + 2) == 33, lasso_depth(5)
assert window(4, 3) == 7, window(4, 3)
# The failing variants: a 4-bit machine needs a shorter search; a window without the stall bound is shorter.
try:
assert lasso_depth(4) == 33
raise SystemExit("used the lasso depth of a smaller machine")
except AssertionError:
pass
try:
assert window(4, 0) == 7
raise SystemExit("priced the window without the stall bound")
except AssertionError:
pass
print("PASS: 32 states need depth 33 for the loop; latency window is 7")Fifty thousand gates at depth 30 give about 4.5 million clauses, taking three clauses per gate per step; two thousand flops add sixty thousand flop-link equalities. Depth 300 gives about 45 million. These are illustrative rules of thumb for sizing, not the capacity of any tool.
def clauses(gates, depth, per_gate=3):
return gates * per_gate * depth
assert clauses(50_000, 30) == 4_500_000, clauses(50_000, 30)
assert 2_000 * 30 == 60_000, "flop links"
assert clauses(50_000, 300) == 45_000_000
# The failing variant: one unrolling step instead of thirty understates the size by 30 times.
try:
assert clauses(50_000, 1) == 4_500_000
raise SystemExit("priced one unrolling for thirty depths")
except AssertionError:
pass
print("PASS: depth 30 is about 4.5 million clauses; depth 300 about 45 million")A 4-bit opcode restricted below 12 and excluding 5 keeps 11 of 16 values; word alignment keeps a quarter of the addresses. Combined, 11 over 64 of the space remains, about 17.2 per cent, so 82.8 per cent is excluded. A bug triggering only on opcode 5 or an unaligned address is invisible: each excluded class needs its verification home named.
def remaining(opcodes_kept, opcodes_all, address_fraction):
return (opcodes_kept / opcodes_all) * address_fraction
left = remaining(11, 16, 1 / 4)
assert abs(left - 11 / 64) < 1e-12, left
excluded = 1 - left
assert abs(excluded - 53 / 64) < 1e-12, excluded
assert round(excluded * 100, 1) == 82.8, excluded
# The failing variant: the same call without the alignment rule understates the exclusion.
try:
assert abs(remaining(11, 16, 1) - left) < 1e-12
raise SystemExit("priced the opcode rule but dropped alignment")
except AssertionError:
pass
print("PASS: 11/64 remains, 82.8 percent excluded by two rules")Nineteen injected bugs across the property classes, seventeen killed at their stated steps: the score is 17 over 19, about 0.895. The gate for required properties is 1.0: every required property kills its mutant, or it is strengthened until it does. Two survivors are two properties that cannot protect the design, named and scheduled, not averaged away.
def signoff_ok(killed, total, gate=1.0):
return killed / total >= gate
score = 17 / 19
assert abs(score - 0.8947) < 1e-3, score
assert signoff_ok(19, 19), "all mutants killed passes the gate"
assert 19 - 17 == 2, "two survivors"
# The failing variant: the same call with 17 of 19 must not pass the gate.
try:
assert signoff_ok(17, 19)
raise SystemExit("gated signoff on a score below 1.0 for required properties")
except AssertionError:
pass
print("PASS: mutation score 17/19, gate is 1.0 on required properties")The 4-entry FIFO overflow bug fails at step 6, so it needs depth 7. By the rule: reset 1, plus a trigger of five pushes (four to fill and one to overflow), plus latency 0, plus 1 check step: 7. The ledger entry reads bounded to 7 with the rule beside it; depth 6 passes and proves nothing, which the paired runs in the whiteboard lesson show directly.
def bound(reset, trigger, latency, check=1):
return reset + trigger + latency + check
justified = bound(1, 5, 0)
assert justified == 7, justified
bug_step = 6
assert justified == bug_step + 1, "the bound reaches one step past the bug"
# The failing variant: a trigger of four pushes (no overflow push) gives the bound that misses the bug.
try:
assert bound(1, 4, 0) > bug_step
raise SystemExit("filed depth 6 as justification for a step-6 bug")
except AssertionError:
pass
print("PASS: justified bound is 7, one past the step-6 bug")The exact one if it converges in budget, because it carries no justification risk; the 41-bit one when the machine demands it, with the argument and the map constraint beside the result.