ASIC puzzle · bounded model checking

Unrolling Time

A SAT solver has no concept of a clock. So how does a circuit full of feedback loops become a formula it can solve? You stop treating time as time and start treating it as an array index.

The problem

A toy circuit with two loops in it

Four cells and two flip-flops. It shifts a serial input I through two stages, and raises S when it sees the pattern 1 then 0. Each flop has the enable-hold mux you've already met — the one that feeds a flop's own output back into its input so it can freeze.

Two feedback paths, drawn in amber. Each flip-flop's output returns to its own mux, so q0 → mux a → q0 is a cycle of length two, and so is q1 → mux b → q1. This graph cannot be topologically sorted, which is exactly the thing that looks fatal.

Written as equations, the circuit is four lines:

m_a = en ? I  : q0      ← q0 depends on itself
m_b = en ? q0 : q1      ← q1 depends on itself
nq0 = NOT q0
S   = q1 AND nq0

The move

The loop becomes a line

Make N copies of the circuit, one per clock cycle, and wire each copy's flop outputs into the next copy's flop inputs. Every net stops being one variable and becomes N variables: q0@0, q0@1, q0@2, and so on.

Unrolling doesn't remove the feedback — it stretches it along the time axis, where it stops being a loop. The same edge that closed a cycle now runs from frame t to frame t+1 and never comes back.

Why the cycle vanishes

The self-referential equation q0 = ITE(en, I, q0) becomes:

q0@(t+1) = ITE(en@t, I@t, q0@t)

q0 still appears on both sides — but at different time indices. Every constraint points strictly from frame t to frame t+1, so the dependency graph of the unrolled formula flows one way and is acyclic.

One flop, four frames

What `q0@t` actually refers to

Keeping two things apart is the whole answer here. The mux and the flip-flop are separate cells driving separate nets:

m_a — the mux output, which is also the flop's D input
q0 — the flop output, its Q

At any one instant these hold different values. The flip-flop's entire job is to relate them across time — and in the unrolled formula that relation is a single equality:

In the unrolled formula the flip-flop computes nothing — it renames. q0@(t+1) and m_a@t are the same value under two names, one frame apart. All the actual logic lives in the mux.

So, to your question directly: yes. The mux's A0 input at frame t is — going back one step — the mux's own output at frame t−1:

m_a@t   = ITE(en@t, I@t, q0@t)     mux, within frame t
q0@t    = m_a@(t-1)                flop, across the frame boundary
─────────────────────────────────────────────────────
m_a@t   = ITE(en@t, I@t, m_a@(t-1))  substituted

The loop is genuinely there. What makes it well defined rather than circular is that the two mentions of the same net carry different frame indices — so nothing depends on itself.

Where `en` comes in

en@t is the mux's select, and like I@t it is a free variable in every frame — the solver picks it independently each cycle, which is what lets it choose when to load and when to hold.

t	q0@t	en@t	I@t	m_a@t = ITE(en, I, q0)	q0@(t+1)
0	0	1	1	1 — loads I@0	1
1	1	0	0	1 — holds, ignores I@1	1
2	1	1	0	0 — loads I@2	0
3	0	1	1	1 — loads I@3	1

Row 1 is the one worth staring at. I@1 = 0, yet q0 stays at 1 into frame 2 — because en@1 = 0 routed the flop's own value back round instead. That is the hold, and it is the reason the cycle exists in the circuit at all.

The second flop is the same thing with a different source

m_b@t = ITE(en@t, q0@t, q1@t) — identical shape, except its "load" input is q0@t rather than I@t. That one substitution is what turns two independent registers into a shift chain: on a load cycle, q1 takes whatever q0 held, while q0 takes the new bit from outside.

The formula

Four frames, three kinds of constraint

Time runs left to right; nothing points backwards. Inputs are free variables in every frame — those are what you are solving for. Only the last frame's output is constrained.

Three kinds of constraint, and that's the entire encoding:

1 · Initial state

q0@0 == 0        q1@0 == 0        the post-reset state

2 · Combinational, repeated in every frame

m_a@t == ITE(en@t, I@t,  q0@t)
m_b@t == ITE(en@t, q0@t, q1@t)
nq0@t == NOT q0@t
S@t   == q1@t AND nq0@t

3 · Transition, between consecutive frames

q0@(t+1) == m_a@t
q1@(t+1) == m_b@t

The reframing that does the work

In the simulator, q_next = D is an assignment, executed in time order. In the formula, q@(t+1) == D@t is an equation that simply has to hold. There is no storage in the formula, and no execution — just N sets of equations that are all true at once.

The grid

Every net becomes a row, every cycle a column

With en held at 1 the transitions collapse to q0@(t+1) = I@t and q1@(t+1) = q0@t, so you can write out what each variable equals symbolically:

	frame 1	frame 2	frame 3
q0	I@0	I@1	I@2
q1	0	I@0	I@1
S = q1 & !q0	0	I@0 & !I@1	I@1 & !I@2

Each column is one copy of the circuit. Each row is one net across time. Nothing in this grid refers to itself — every cell is written purely in terms of cells to its left.

The payoff

Solving runs backwards, which searching cannot

Same equations, opposite direction. Because all four frames hold simultaneously, the constraint on frame 3 propagates back through frames 2 and 1 — no enumeration involved.

Read the last row of the grid and the derivation is two steps:

S@3 = I@1 & !I@2, and we require it to be 1
therefore I@1 = 1 and I@2 = 0; I@0 is unconstrained

The solver did no searching. It propagated one constraint backwards through three frames and read off the answer — which is exactly why this scales to input spaces you could never enumerate. A single serial pin over 100 cycles is 2¹⁰⁰ possible waveforms; constraint propagation never visits them.

The equivalence

Why this is the same thing the simulator does

The formula is the relation; the simulator is one way of using it. Like y = f(x) — you can evaluate it forwards or solve it for x. Nothing about the circuit changed.

The equivalence is provable by induction on the frame index:

Base. The initial constraint pins q@0 to the reset state — identical to what the simulator starts from.
Step. Suppose the model's state at frame t equals the simulator's state at cycle t. Given that state and the frame's inputs, the combinational constraints have exactly one solution — so every internal net variable in frame t equals what the simulator computes.
Therefore the transition constraint fixes frame t+1's state to the same value the simulator's sampling phase produces.

So for any fixed input sequence, the formula has exactly one satisfying assignment: the simulator's trace. Which gives the result you actually want —

What SAT means here

The formula plus the goal is satisfiable if and only if there exists an input sequence whose simulation reaches that goal. A model returned by the solver is a valid stimulus, and you can replay it through the simulator to confirm.

The ingredient that makes it work

The "exactly one solution" in the induction step isn't free. It holds because the combinational subgraph is a DAG: evaluate it in topological order and each constraint net == f(inputs) pins exactly one value.

If there were a combinational loop

A cycle among combinational cells could leave the constraints with zero solutions, or several — and the correspondence with the simulator would break. That is the same property _topo() relies on, and the same one it raises an error about.

Which means: the acyclicity check that makes your simulator evaluable is also what makes the SAT encoding faithful. One property, two payoffs — and if extraction merges two nets that should be separate, both fail at once, loudly.

Scale

What this costs on the real netlist

The warm-up has 84 nets, 63 combinational cells and 16 flops. Unrolled:

Cycles	Net variables	Free input vars	Cell constraints
10	840	40	630
20	1,680	80	1,260
64	5,376	256	4,032

Everything is linear in N. No blow-up — a 64-cycle unroll of this design is a few thousand variables, which z3 handles instantly. The cost of looking further into the future is a proportional cost, not an exponential one.

The one real subtlety: choosing N

UNSAT at N means "not achievable within N cycles" — not "impossible." Bounded model checking is only ever a statement about the bound you chose.

So you iterate, raising N until you get SAT or run out of patience. Pick the starting value from structure rather than guessing: the depth of the longest shift chain, plus reset, plus the settle cycle. The flop count and cone() give you that.

Translating the cell library

The expression trees in celllib.py map one-to-one onto z3's constructors, so the bridge is about a dozen lines and no decomposition into primitive gates is needed — z3 converts to CNF internally.

# celllib expression        z3
("and", a, b)      →  z3.And(a, b)
("or",  a, b)      →  z3.Or(a, b)
("not", a)         →  z3.Not(a)
("xor", a, b)      →  z3.Xor(a, b)
("mux", s, i1, i0) →  z3.If(s, i1, i0)
("var", pin)       →  ref(net_of(pin), t)
("const", v)       →  z3.BoolVal(v)

That is the entire reason for keeping compound cells like a21boi as expression trees rather than collapsing them to a label or flattening them into gates: the tree was already the shape the solver wants.