About Tensordyne
TensordyneTensordyne builds next-generation AI inference systems.
12.2M
Gate equivalents in one formal model
241
WHOLE-BLOCK Properties proved or refuted
~26%
Less power, on a block written from spec
Project 1 · Verification
The most complex block
Jonathan Ko, an ASIC verification engineer at Tensordyne, picked the block he considered most complex to verify for next-generation exploration. It has 12.2 million gate equivalents, 1.24 million flops, 45 Mbit of SRAM, and hundreds of state machines running concurrently. Its specifications run to 312 pages.
“Even sub-blocks a tenth this size are very difficult to formally verify with traditional tools. You would never even consider trying something as large as this.”
Jonathan Ko
ASIC Verification Engineer, Tensordyne
He gave Aristotle the RTL, a formal wrapper, the specs, and one prompt describing the setup. Aristotle drafted its properties, asked a few questions about the environment, and flagged where two documents disagreed.
Aristotle wrote 100 of the 241 properties from the specs. The other 141 were assertions already in Tensordyne's RTL. Aristotle proved 185 and refuted 56, each refutation with a reproducible counterexample. Every proof covers the whole partition from power-on, for every input sequence the environment allows, with no bound on the number of cycles.
185
Properties proved
56
Refuted, each with a counterexample
110,000
Cycles deep, deepest bug
8
Bugs found early in the design cycle
The refutations exposed bugs 25,000 to 110,000 cycles after reset, past about 24,600 cycles of memory initialization and long multi-step job sequences. With these findings and earlier Aristotle runs on sub-blocks, Tensordyne found 8 bugs extremely early in the design cycle of its next chip.
Tensordyne’s verification team now uses Aristotle on other blocks.
Project 2 · Design from spec
Early exploration for the next chip
In the second project, Tensordyne tried the whole loop on a common sub block: RTL from spec, proofs, and synthesis. Aristotle got the functional and microarchitecture specifications and the port list of an existing block. It wrote the RTL from scratch and matched every port. Then it derived 37 properties from the specs and the prompt and proved them all.
Tensordyne synthesized each version in its own flow and fed the reports from the first two rounds back to Aristotle. Aristotle came up with every optimization. It read the reports, changed the RTL, explained why each change should help, and re-proved all 37 properties.
Tensordyne measured about 26% less power, 19% less cell area, 25% fewer cells, and 20% less leakage in an early iteration of the block for their next chip.
~26%
Less power
~19%
Less cell area
~25%
Fewer cells
~20%
Less leakage
“We used Aristotle to improve a common block’s power and area by about 20% in early explorations for our next chip.”
Jonathan Ko
ASIC Verification Engineer, Tensordyne
“Formal verification has traditionally meant a steep learning curve and writing properties by hand. Aristotle got us over those hurdles: it’s easy to start, intuitive to understand, and nearly fire-and-forget. Our designers get instant feedback during early RTL creation, and our DV engineers can formally verify state spaces that would be unthinkable with traditional tools. It also audits our functional and microarchitecture specs against the RTL, flagging ambiguities so design intent stays clear.”
Jonathan Ko
ASIC Verification Engineer, Tensordyne