Numeric Drills: State and Depth

On this page

Part 9 of 10, lesson 12 of 15Interview PrepAll levels

Why it matters

Panels use arithmetic to test whether abstractions are priced or wished for. Each drill states the rule, works it by hand, and checks it in a calculator written as a function, so the failing variant calls the same function with a wrong input. Numbers on the running designs come from counted runs; the rest are labelled illustrative or derived.

Job of this lesson: make six calculations automatic: space, bound, overflow depth, induction k, memory bits, counter bits.

1. State-space size

Three 8-bit registers, a 4-bit counter, a 2-bit state machine and a 16 by 8 memory give 24 plus 4 plus 2 plus 128, which is 158 bits. Two to the 158 is about 3.7 times 10 to the 47: at a billion states per second, enumeration outlives the project by thirty orders of magnitude. The conclusion the panel wants: tools work symbolically on the cone of the property, never by enumeration. The sizes are illustrative.

example.py

def space_bits(regs8, counter, fsm, mem_words, mem_width):
    return regs8 * 8 + counter + fsm + mem_words * mem_width

bits = space_bits(3, 4, 2, 16, 8)
assert bits == 158, bits
states = 2 ** bits
assert abs(states - 3.7e47) / states < 0.02, states
# The failing variant: the same call without the memory understates the space by 128 bits.
try:
    assert space_bits(3, 4, 2, 0, 8) == 158
    raise SystemExit("sized the machine without its memory")
except AssertionError:
    pass
print("PASS: 158 bits, about 3.7e47 states, enumeration is not the method")

2. BMC bound for a pipeline

A 6-stage pipeline answers in 6 cycles, reset lasts 2, and the bug needs 4 back-to-back requests (the trigger length). Minimum depth is reset 2, plus trigger 4, plus latency 6, plus 1 check step: 13. The rule is the same everywhere: depth at least reset plus trigger length plus worst-case latency plus 1. The figures are illustrative.

example.py

def min_depth(reset, trigger, latency, check=1):
    return reset + trigger + latency + check

assert min_depth(2, 4, 6) == 13, min_depth(2, 4, 6)
# The failing variant: the same call without the check step quotes a bound one short.
try:
    assert min_depth(2, 4, 6, check=0) == 13
    raise SystemExit("quoted a bound without its check step")
except AssertionError:
    pass
print("PASS: minimum depth 13, rule is reset plus trigger plus latency plus 1")

3. Depth to see a FIFO overflow

One reset step, then N pushes to fill and one more to overflow (trigger N + 1), no latency, one check step: 1 plus N + 1 plus 0 plus 1 gives N + 3. Measured: 7 on the 4-entry FIFO, 8 on the occupancy counter at 5 entries, 15 at 12 entries, each with the depth one lower passing. The rule then gives 19 for 16 entries and 1027 for 1024, derived and not run, which is why the proof uses a small parameter or induction instead of brute depth. A wrap needs about two laps of the pointers, 2N + 2 steps (34 for 16, 2050 for 1024): also derived, not run.

example.py

def depths(entries):
    overflow = 1 + (entries + 1) + 0 + 1      # reset, fill plus overflow push, latency, check
    wrap = 2 * entries + 2                    # derived: two laps of the pointers
    return overflow, wrap

assert depths(4)[0] == 7, depths(4)          # measured on sync_fifo: bmc 6 passes, bmc 7 fails
assert depths(5)[0] == 8 and depths(12)[0] == 15   # measured on the occupancy counter
assert depths(16) == (19, 34), depths(16)
assert depths(1024) == (1027, 2050), depths(1024)
# The failing variant: a 15-entry FIFO is not a 16-entry one.
try:
    assert depths(15)[0] == 19
    raise SystemExit("accepted the overflow depth of the wrong FIFO size")
except AssertionError:
    pass
print("PASS: overflow depth is entries plus 3 (19 for 16, 1027 for 1024); wrap figures are derived")

4. Induction k for the decade counter

The property 'count is not 15' is true but not inductive: the unreachable chain 10 to 14 satisfies it and leads to 15. With the enable free, no k up to 20 closes it (shown in the decade counter case of the methodology section: Splitting Properties and Parameters). Force the enable high by an assumption and the chain is five states long, so the step needs a window of six good states to see the violation coming: k of 6. Runs: with the enable forced high and no helper, depth 5 leaves the step unproven and depth 6 proves it. With the helper 'count at most 9' the property closes at k of 1, and the whole set at 2.

mod10_counter.sv

// formal: prove 5 expect unproven slang top mod10_counter define HELPER=0
`define FORMAL
// mod10_counter: 4-bit decade counter, counts 0..9 and wraps to 0.
module mod10_counter #(parameter BUG = 0, parameter HELPER = 1) (
  input  wire       clk,
  input  wire       rst,
  input  wire       en,
  output reg  [3:0] count,
  output wire       tc
);
  wire [3:0] last = (BUG == 1) ? 4'd10 : 4'd9;
  assign tc = en && (count == last);
  always @(posedge clk) begin
    if (rst)      count <= 4'd0;
    else if (en)  count <= (count == last) ? 4'd0 : count + 4'd1;
  end
`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  always @(*) assume (en);
  always @(*) if (!init) a_not15: assert (count != 4'd15);
  generate if (HELPER) begin : g_helper
    always @(*) if (!init) a_range: assert (count <= 4'd9);
  end endgenerate
  always @(*) if (!init) a_tc: assert (tc == (en && count == 4'd9));
  always @(posedge clk) if (!init && !$past(rst)) begin
    a_step: assert (!$past(en) || count == (($past(count) == 4'd9) ? 4'd0 : $past(count) + 4'd1));
    a_hold: assert ($past(en) || count == $past(count));
  end
  reg wrapped;
  always @(posedge clk) begin
    if (rst) wrapped <= 1'b0;
    else if (tc) wrapped <= 1'b1;
  end
  always @(*) if (!init) begin
    c_nine: cover (count == 4'd9);
    c_tc:   cover (tc);
    c_wrap: cover (wrapped && count == 4'd3);
  end
`endif
endmodule

mod10_counter.sv

// formal: prove 6 expect pass slang top mod10_counter define HELPER=0
`define FORMAL
// mod10_counter: 4-bit decade counter, counts 0..9 and wraps to 0.
module mod10_counter #(parameter BUG = 0, parameter HELPER = 1) (
  input  wire       clk,
  input  wire       rst,
  input  wire       en,
  output reg  [3:0] count,
  output wire       tc
);
  wire [3:0] last = (BUG == 1) ? 4'd10 : 4'd9;
  assign tc = en && (count == last);
  always @(posedge clk) begin
    if (rst)      count <= 4'd0;
    else if (en)  count <= (count == last) ? 4'd0 : count + 4'd1;
  end
`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  always @(*) assume (en);
  always @(*) if (!init) a_not15: assert (count != 4'd15);
  generate if (HELPER) begin : g_helper
    always @(*) if (!init) a_range: assert (count <= 4'd9);
  end endgenerate
  always @(*) if (!init) a_tc: assert (tc == (en && count == 4'd9));
  always @(posedge clk) if (!init && !$past(rst)) begin
    a_step: assert (!$past(en) || count == (($past(count) == 4'd9) ? 4'd0 : $past(count) + 4'd1));
    a_hold: assert ($past(en) || count == $past(count));
  end
  reg wrapped;
  always @(posedge clk) begin
    if (rst) wrapped <= 1'b0;
    else if (tc) wrapped <= 1'b1;
  end
  always @(*) if (!init) begin
    c_nine: cover (count == 4'd9);
    c_tc:   cover (tc);
    c_wrap: cover (wrapped && count == 4'd3);
  end
`endif
endmodule

mod10_counter.sv

// formal: prove 6 expect unproven slang top mod10_counter define HELPER=0
`define FORMAL
// mod10_counter: 4-bit decade counter, counts 0..9 and wraps to 0.
module mod10_counter #(parameter BUG = 0, parameter HELPER = 1) (
  input  wire       clk,
  input  wire       rst,
  input  wire       en,
  output reg  [3:0] count,
  output wire       tc
);
  wire [3:0] last = (BUG == 1) ? 4'd10 : 4'd9;
  assign tc = en && (count == last);
  always @(posedge clk) begin
    if (rst)      count <= 4'd0;
    else if (en)  count <= (count == last) ? 4'd0 : count + 4'd1;
  end
`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  always @(*) if (!init) a_not15: assert (count != 4'd15);
  generate if (HELPER) begin : g_helper
    always @(*) if (!init) a_range: assert (count <= 4'd9);
  end endgenerate
  always @(*) if (!init) a_tc: assert (tc == (en && count == 4'd9));
  always @(posedge clk) if (!init && !$past(rst)) begin
    a_step: assert (!$past(en) || count == (($past(count) == 4'd9) ? 4'd0 : $past(count) + 4'd1));
    a_hold: assert ($past(en) || count == $past(count));
  end
  reg wrapped;
  always @(posedge clk) begin
    if (rst) wrapped <= 1'b0;
    else if (tc) wrapped <= 1'b1;
  end
  always @(*) if (!init) begin
    c_nine: cover (count == 4'd9);
    c_tc:   cover (tc);
    c_wrap: cover (wrapped && count == 4'd3);
  end
`endif
endmodule

example.py

def min_k(chain_length):
    # chain_length unreachable states satisfy the property and lead to the violation
    return chain_length + 1

assert min_k(len([10, 11, 12, 13, 14])) == 6, "matches the runs: prove 5 unproven, prove 6 proved"
# The failing variant: a four-state chain would close one step earlier, not at 6.
try:
    assert min_k(4) == 6
    raise SystemExit("claimed k of 6 for a four-state chain")
except AssertionError:
    pass
print("PASS: minimum k is 6 with the enable forced high and no helper")

5. State bits after memory abstraction

A 256 by 32 memory is 8192 bits. The tracked-entry abstraction keeps an 8-bit symbolic address, a 32-bit shadow value and a valid bit: 41 bits, about 200 times fewer. It is sound only when the property concerns one address at a time and control ignores data, with the address constrained to the legal map.

example.py

import math

def tracked_bits(entries, width):
    return math.ceil(math.log2(entries)) + width + 1    # address, shadow value, valid bit

full = 256 * 32
assert full == 8192, full
assert tracked_bits(256, 32) == 41, tracked_bits(256, 32)
assert full // tracked_bits(256, 32) >= 199
# The failing variant: the same call for a 128-entry memory gives a different bit count.
try:
    assert tracked_bits(128, 32) == 41
    raise SystemExit("accepted the bit count of a different memory size")
except AssertionError:
    pass
print("PASS: 8192 bits abstracted to 41, about a 200 times reduction")

6. Counter abstraction

A 32-bit timeout counter waiting a million cycles needs a bound near a million: 1 plus 1,000,000 plus 1 plus 1 is 1,000,003 steps. A saturating counter at threshold 2 keeps 2 bits and needs 1 plus 2 plus 1 plus 1, which is 5, justified by proving the surrounding logic identical below the threshold or by proving the real counter by induction. The panel listens for the justification, not the trick. The figures are illustrative.

example.py

def bound(reset, trigger, latency, check=1):
    return reset + trigger + latency + check

real_wait, threshold = 1_000_000, 2
real = bound(1, real_wait, 1)
abstract = bound(1, threshold, 1)
assert real == 1_000_003, real
assert abstract == 5 and abstract < 10, abstract
assert 2 ** 2 > threshold, "2 bits hold the saturating count"
assert 2 ** 32 > real_wait, "the real 32-bit counter does span the wait"
# The failing variants: keeping the million-cycle bound, or giving the counter one bit.
try:
    assert bound(1, real_wait, 1) < 10
    raise SystemExit("kept the million-cycle bound after abstracting")
except AssertionError:
    pass
try:
    assert 2 ** 1 > threshold
    raise SystemExit("one bit cannot hold a threshold of 2")
except AssertionError:
    pass
print("PASS: 32-bit million-cycle wait becomes 2 bits and depth 5")

Check yourself The bound reaches the bug but the proof still spins. What did the depth buy?

A counterexample search, not a proof: depth buys bug-finding up to N and a justified interim status, while convergence needs reduction or invariants.

Navigate

Why it matters

1. State-space size

2. BMC bound for a pipeline

3. Depth to see a FIFO overflow

4. Induction k for the decade counter

5. State bits after memory abstraction

6. Counter abstraction

Related topics

Numeric Drills: State and Depth

Why it matters

1. State-space size

2. BMC bound for a pipeline

3. Depth to see a FIFO overflow

4. Induction k for the decade counter

5. State bits after memory abstraction

6. Counter abstraction

Related topics

Why it matters

1. State-space size

2. BMC bound for a pipeline

3. Depth to see a FIFO overflow

4. Induction k for the decade counter

5. State bits after memory abstraction

6. Counter abstraction

Related topics

Up next

Why it matters

1. State-space size

2. BMC bound for a pipeline

3. Depth to see a FIFO overflow

4. Induction k for the decade counter

5. State bits after memory abstraction

6. Counter abstraction

Related topics

Up next