The chip netlist whose area and delay are published matches its design: a formal equivalence proof
Turning a chip design into gates can quietly change what it does, and tests on sample inputs cannot rule that out. The lab used an open-source tool to prove that the gate-level circuit of its admission engine is equivalent to the design it came from. The proof covers the circuit whose area and delay are published.
What it shows
A digital chip starts as a design written in a hardware description language, at the level engineers call RTL. Synthesis tools turn that design into a netlist: a list of logic gates and flip-flops and the wires between them. The netlist is what gets built, and it is what area and speed figures describe. If synthesis changes the behaviour, the chip does something other than what was designed and reviewed.
The two proofs
The lab's design is an admission engine. The evidence file shows one line of it, in its record of a deliberate breakage: the block enables an allocation only when its decision authorises it. The lab's claim, in our claim file, states two proofs. The first covers the netlist mapped to SkyWater's open cell library, the netlist whose area and delay are published. It is proved equivalent to the design, using SkyWater's own functional models of the cells it uses. The second covers an earlier step on its own, where the tool turns the design into its own generic gates.
The tool that does the proving
Both proofs use Yosys, an open-source synthesis suite. Yosys places a comparison cell on each matched pair of signals and then proves every one of them. The claim gives the number of comparison cells at each step. Every one was proved.
Why it matters, and to whom
This matters to Wi-Fi chipset and silicon vendors who might put such a block into an access point or device chip. A buyer of a hardware block wants to know that the circuit that was measured is the circuit that was reviewed. Simulation checks sample inputs. An equivalence proof covers every input, so it rules out a whole class of synthesis bugs that testing can miss.
It also ties the published area and delay to the proved design. Without the first proof, those figures would describe a netlist that nothing had shown to match the design.
How it was checked
The evidence file records the command that runs the check, its passing result line from a clean copy of the lab's code, and how long the run took: 20.9 seconds.
The lab also tested the check by breaking the design on purpose: it tied the allocation signal on, so the block would allocate whatever its decision said. The evidence file records that the check then failed, because the design no longer matched the lab's reference engine written in C. That shows the comparison with the reference can fail; the served files do not report a deliberate break of the netlist proof itself, which is the test suggested at the end of this page.
What the outside tool does and does not rule out
The outside tool here is Yosys, and the cell models for the mapped proof are SkyWater's, not the lab's. That makes the proof harder to fake than a check the lab wrote itself. It does not rule out a bug in Yosys: when the same tool does the synthesis and the proof, one fault could affect both.
What it does not claim
- It does not claim anything about timing. An equivalence proof says the logic is the same; it says nothing about whether signals arrive in time. The lab's own scope note, from the evidence file, reads: Covers every input to the mapped netlist. WireLoad = none: no place-and-route, no parasitics, no OpenSTA, no sign-off corner, no tape-out. The 4816.17 ps / ~207 MHz figure must never travel without that caveat.
- It does not claim a new method. Proving that a synthesised netlist matches its source design is the documented purpose of the Yosys equivalence commands, and YosysHQ describes a framework built for checking netlists after synthesis. This result applies that flow to one more design. Its value is evidence that this netlist matches its design, not an invention.
- It does not claim that the admission engine is the right design for real access points. That question belongs to the lab's other results on access-point memory and on attack search.
How to reproduce it
The evidence file names the command that re-runs the check. It needs the lab's code at the commit named in the evidence file, Yosys, and SkyWater's public cell library.
To test it harder, change one gate in the mapped netlist and re-run the proof; the proof should fail. To go further than the lab, run layout and timing analysis on the mapped netlist, then prove equivalence again on the netlist that comes out of layout. That would carry the guarantee one step closer to a real chip.
Formal statement
Here d is the design and n is the netlist. In words: whenever the matched flip-flops of the two circuits agree, they give the same outputs on every input and step to states that agree again. This is the shape of a proof by induction over matched flip-flops, which is how the Yosys command for proving equivalence cells works.
Prior art
- YosysHQ, Yosys documentation, "Equivalence checking" commands: builds comparison cells between two designs and proves them by induction; the method used here
- Engelhardt and Wolf, "New Open Source Design Verification Tools from YosysHQ": an open framework for checking netlists after synthesis
Evidence
- The evidence file for this result
- Our claim file, with its limits
- All our published files, each with a fingerprint you can check