What it shows
A full mask is split into tiles, and each tile carries a stored check with some margin to spare. When a designer makes one small edit, the tiles near it may change. The usual answer is to simulate them again.
This method asks a cheaper question first. It bounds how much the edit can change each nearby tile. If that bound fits inside the margin the tile’s stored check already had, the tile is proved still valid and is not recomputed.
The published record says, word for word (an excerpt)
A tile whose inputs did move is proved still valid when a certified bound on the edit's influence fits inside the margin its stored certificate was already carrying, with 0 violations over 9,175,040 pointwise comparisons.
Why it matters
Re-checking a full chip after every small change repeats work. A proof that some nearby tiles are still valid lets a tool skip re-simulating them, for single edits. How many it skips depends on the edit. On one published workload of small, even changes to the exposure dose, it cleared only 8 of 640 tiles. Close to the point where a pattern stops printing reliably, it ran at 0.88x the speed of simply recomputing, so there it costs time instead of saving it.
Why now: lithography is entering a new machine generation; ASML calls its first High-NA EUV system "the first in a new generation of machines". Each new generation brings new masks to check, and every edit to them has to be checked again.
Who should care
- Mask-synthesis and physical-verification software makers. Incremental re-checking with a proof attached, for one edit at a time.
- Mask-data preparation teams. Fewer full re-simulations after small corrections, inside the stated limit.
The limits, in the record’s words
The published record says, word for word (an excerpt)
SINGLE-edit re-certification only. Chained multi-edit soundness is NOT established.
The published record says, word for word (an excerpt)
Do not call the incremental path generally sound.
In plain words: over a chain of four edits, 9 of 64 tile results came out worse than recomputing from scratch, by up to 4.3267 nanometres, and the test set for single edits could not see it.
Everything here is measured in our own simulator, not on a printed wafer.
Open source for this step
Tools and datasets we publish for the print step of building a multi-chip package. They are the checkers around this work, not a copy of the result itself.
- cert-atlas: A labelled set of forged lithography certificates, scored on wrong accepts and wrong rejects alike, so a checker that accepts everything or rejects everything cannot score well.
- lcert-verify: A checker for our lithography certificates that needs only Python's standard library.
- lcert-verify-web: The same verifier in the browser: zero dependencies, nothing uploaded.
- equiv-receipt: A small file that records why two versions of a circuit compute the same thing, which anyone can re-check without our tools.
- prereg (pre-registration primitive): Write your acceptance criteria down, hash them, then measure — a tiny pre-registration primitive.
- certified-mcp: Lets an AI agent ask our certificate checker for a yes-or-no answer, instead of judging a certificate itself.
- cert-verifier: Drop a lithography certificate bundle and verify it in your browser.