For people interested in this: I've been working on an open-source libtpu implementation for https://tenstorrent.com/ accelerators as a side project, it can already run most of torchtpu, see https://github.com/pcmoritz/libtt (based on the tenstorrent software stack). It shows all the things involved in lowering torch to tile based accelerators.

▲

asparagui an hour ago | parent | next [-]

Very cool! I have been using Lean to drive PJRT like so: https://github.com/brettkoonce/lean4-mlir and in theory your code could unlock another platform!

	▲	pcmoritz an hour ago \| parent [-]
		Thanks for sharing, this is super cool! Right now my approach to correctness it to just run as many tests as possible and fix them (torchtpu greatly expands the amount of available tests), but formal verification is also super cool. Having a look at your book https://lean.brettkoonce.com/blueprint.pdf The Tenstorrent ISA is documented btw https://github.com/tenstorrent/tt-isa-documentation, I wonder if one could do the verification end-to-end with the hardware.

▲

yhjc2692 2 hours ago | parent | prev [-]

This is super cool!

▲

pcmoritz an hour ago | parent [-]

Thanks for the encouragement, if you have the hardware and end up trying it out I'd love to get your feedback (feel free to drop an issue in the repo) :)

▲

yhjc2692 an hour ago | parent [-]

I would love to do that, but unfortunately don’t have one on hand (yet?). In fact, I’m curious - did you buy a TT device to work on this, or are you using a cloud provider like Koyeb?

	▲	pcmoritz an hour ago \| parent [-]
		I first built my own to try it out (the exact hardware is described in https://relativity.cc/hardware/ under "one Blackhole card") and when I liked the hardware I got a quietbox 2. It is very high quality but a little expensive (but inexpensive compared to other LLM hardware and it has excellent interconnects which is very rare in the consumer/dev space).