The Proof-Carrying Platform for the Multi-Die Era.

Package-coupling and mask-printing results to license or buy, for chip-package design teams and makers of extraction, signoff and lithography software, as chips move to multi-die packages.

Founder: Nick Harris · nick@chipletos.com

Read the results Try the Verifier Talk to us about your layout

6.1×Smaller coupling error than pair-by-pair sums; FastCap-graded median of 24 simulated layoutsAgainst our own pair-by-pair solver, a different solver class: 15.6× on 11 layouts, 12.1× on 43.
≥ 10.467%Proved error floor of pair-by-pair extraction: it overstates the worst coupling by at least this on every layout of one modelled via family

01PlatformSheet 01 / 07

From mask to package, in three checks

A multi-chip product is printed, bought in pieces and then packaged. Below is what we have shown for each step, in simulation.

Print
A mask tile, the pattern our simulator prints from it, and the range computed around that pattern.
Check how a chip pattern will print, against our own detailed simulation, before paying to make it.
A near-constant-size sign-off record for a photomask (VerifyCore Labs)
The problemA fast check can approve a mask that the slow, accurate simulation would reject, and the error shows up late.
ChipletOSFor every pixel of the simulated image, at the stated grid, we compute a range that contains our detailed simulation’s value, assuming standard floating-point rules and an accurate maths library.
One internal step’s numerical error is left out of that range.
Trust
A chip design kept private, and the kind of short certificate we propose a checker could verify.
Why testing alone cannot rule out a leak in a modelled timing channel.
The problemA company buying chiplets from two suppliers cannot ask either one for its design, which is a trade secret, yet it still has to trust what it buys.
ChipletOSOur proposed approach is to hand over a checkable certificate instead of the design; Theorems & Bounds shows why, in a modelled timing channel, testing alone can miss a rare leak.
Package
Two vertical connections through glass, the interference between them, and the quantity being checked.
A predictor of how a package’s connections interfere, graded by an outside solver.
The problemNeighbouring vertical connections interfere. A quick estimate adds the coupling up one pair at a time; here, a pairwise baseline we built. A sample shows it is wrong.
ChipletOSWe grade a predictor, and that shortcut, against FastCap, an independent solver, and prove a floor on the shortcut’s error inside a simplified model (see Theorems & Bounds).

02ResultsSheet 02 / 07

What we have shown

Graded on capacitance by FastCap, an outside solver, our model of coupling in simulated chip packages had a smaller median per-layout error than a simple add-up-the-pairs shortcut. Each result has its own page.

Packaging
6.1×Shortcut’s error over ours, median of per-layout ratios, simulated layouts
A coupling predictor, graded by an outside solver
Our model of coupling between a package’s vertical connections, graded against FastCap, an outside solver.
Read the result
Printing
13.3 millionPixel checks, none outside the computed range
A printing check whose range held our simulation on every test mask
For each pixel of our simulated print, a computed range contained the detailed simulation on every test mask tried.
Read the result
Packaging
about 40%At the ends of one simplified via, in simulation
The capacitance at a via’s ends, simulated
Our own three-dimensional solver computed, in simulation, the capacitance flat models leave out at a via’s ends, and one flat solver now adds it back.
Read the result
Printing
0 violationsPointwise checks, single edits, simulated
Small mask edits, re-checked without starting over
After one small mask edit, a computed bound shows some nearby tiles are still valid without re-simulating them.
Read the result
Packaging
< 1Gain of the wiring models, seeded trials
Wiring models built to rule out invented energy
Wiring models whose gain, in exact arithmetic, never exceeds one, so they cannot invent energy.
Read the result

More results

Every result with its own page is in Research.

Why now

Chip makers are moving from one large chip to packages that combine several smaller ones; Intel describes the industry as moving into “the heterogeneous era that uses multiple ‘chiplets’ in a package”, and has announced glass substrates for such packages, planned for the latter part of this decade. More of what decides whether a product works now sits in the package. Source: Intel newsroom: glass substrates for next-generation advanced packaging.

Who it is for

Chip-package and interposer design teams, and makers of extraction, signoff and lithography software, who could license or buy a result.

Who we are

Nick Harris, founder. CTO of VivaMed BioPharma; co-founder of MedSim.ai, FastRead.io and Formulai.

AI agents do our research and engineering. Write to nick@chipletos.com.

Explainers

All posts

03VerifySheet 03 / 07

Check one of our files yourself

Drop one of our published files here, and your browser confirms it is exactly the file we publish. Nothing is sent anywhere.

Check your own certificate

Drop a lithography certificate bundle of your own into the open-source verifier: it runs in your browser, and nothing is uploaded. Supply an expected SHA-256 fingerprint from a trusted source outside your bundle; a blank fingerprint remains UNVERIFIED. It checks the certificate’s internal consistency and integrity, not the physics.

Open the certificate verifier Source files

File check · runs in this tab

$ Drop one of our published files anywhere on this panel.

or try

04Theorems & BoundsSheet 04 / 07

Theorems & Bounds

Each statement is made inside its own stated model.

Computer proof by interval arithmetic
$\forall θ \in Θ_{pair} : C_{pairwise} (θ) / C_{true} (θ) \geq 1.10467$
$\forall θ \in Θ_{pair} :$ $C_{pairwise} (θ) / C_{true} (θ) \geq 1.10467$
The pairwise extraction floor
Inside our simplified model of the vias, adding up coupling one pair at a time over-predicts the worst coupling by at least 10.467% for every layout in this family, proved by interval arithmetic. Against our own boundary-element solver the measured gap is about 9.8%.
410,165 certified boxes, 0 failure regions
Separately, in FastCap, an outside solver: added-up pair answers over-predicted the largest coupling term on 12 of 12 layouts
Read the result Certificate
Checked by a proof assistant (Lean)
$A A^{⊤} ⪰ 0 for every real matrix A$
$A A^{⊤} ⪰ 0$ $for every real matrix A$
The algebra step behind passive wiring models
A short algebraic argument rules out our wiring models creating energy out of nothing; only one standard lemma it uses is checked in Lean.
Certificate
Computer proof by interval arithmetic
$\forall θ \in Θ_{pair} : C_{true} (θ) / C_{pairwise} (θ) \geq 0.83$
$\forall θ \in Θ_{pair} :$ $C_{true} (θ) / C_{pairwise} (θ) \geq 0.83$
A floor under isolation, too
Inside our simplified model of the vias, spacing alone cannot push this family's pair coupling below 83% of its isolated value.
Certificate
Checked by a proof assistant (Lean)
$sound certificate for an m -⁠bit verdict ⟹ 2^{m} \leq ∣ C ∣$
$sound certificate for an m -⁠bit verdict$ $⟹ 2^{m} \leq ∣ C ∣$
One number cannot sign off an array
If any mix of pass and fail across the pairs can happen, one pass-or-fail score cannot vouch for a group of coupled connections: a trustworthy summary needs at least one yes-or-no answer per pair.
Certificate
Checked by a proof assistant (Lean)
$2 (n + 1) < 2^{C} ⟹ a majority of n -⁠trace experiments miss a capacity-⁠ C leak$
$2 (n + 1) < 2^{C}$ $⟹ a majority of n -⁠trace experiments miss a capacity-⁠ C leak$
In a modelled timing channel, most test runs miss a rare leak
For a rare leak in a modelled timing channel, below a stated threshold most test runs miss the leak, and the number of test traces needed doubles with every bit of leak capacity (a lower bound, in the model).
Certificate

05Artifacts & Open SourceSheet 05 / 07

Open-source tools and data

35open repositories, datasets and live demos, in 30 projects, grouped by the lifecycle step they serve.

All 30 projects, by lifecycle step

Print9

Trust10

Package8

06Intellectual PropertySheet 06 / 07

Intellectual Property

The four technology families our results sit in, and how each is checked.

Lifecycle step	Technology family	How it is checked
Print	Certificates for machine-generated lithography masks: a range that contains the simulated image, and re-checks after a single edit (chains of edits are not established)	Ranges by interval arithmetic, under standard floating-point rules and an assumed-accurate maths library · run on our own machines
Trust	Hardware trust: Lean-checked bounds showing why testing alone cannot prove a leak absent in a modelled timing channel; a certificate scheme is proposed, not yet published	The Lean proof assistant · the Z3 logic solver
Package	Proved error floors for pairwise extraction on one via family, in a simplified model	Interval-arithmetic proofs over whole design ranges · our own field solver · FastCap and Palace, two outside solvers
Package	Glass-core interposers: the electrical design of through-glass vias (one result published: a layout search gated by our own solver, in simulation)	Boundary-element extraction of electrical behaviour

Where we are

Research results in simulation, nothing measured on silicon, no customer yet, and not yet a released product. Disclosures

Details

Third-party tools named here (FastCap and Palace) are used or cited only: ChipletOS has no commercial, partnership, supply, evaluation or endorsement relationship with their makers.

When a number is left off

We leave a number off a page, or mark it, when

its file has not loaded yet
nobody has looked into it yet
a search for it found nothing
its file holds no value for it
its file is missing or altered
files disagree on what it describes
its sample is too small for the claim
two files give different values
its file cannot be published
it was measured over ninety days ago
the question does not apply here
the program behind it stopped with an error

The Proof-Carrying Platform for the Multi-Die Era.

From mask to package, in three checks

Print

Trust

Package

What we have shown

A coupling predictor, graded by an outside solver

A printing check whose range held our simulation on every test mask

The capacitance at a via’s ends, simulated

Small mask edits, re-checked without starting over

Wiring models built to rule out invented energy

More results

Why now

Who it is for

Who we are

Explainers

Check one of our files yourself

Check your own certificate

Theorems & Bounds

The pairwise extraction floor

The algebra step behind passive wiring models

A floor under isolation, too

One number cannot sign off an array

In a modelled timing channel, most test runs miss a rare leak

Open-source tools and data

Intellectual Property

Where we are