Symbiflow and Axiom

[Tim Daly]

Tim,

I just watched your Symbiflow video.
https://www.youtube.com/watch?v=-xyAauPa__s

My first question is: I saw you had an Axiom t-shirt.
What does it refer to? Clearly not the Axiom project :-)




I'm Tim Daly, project lead on Axiom, an open source
computer algebra project:
https://en.wikipedia.org/wiki/Axiom_(computer_algebra_system)

My current research project involves proving Axiom's
mathematical algorithms "down to the metal". In this case
the "metal" refers to FPGAs.

Mathematical proofs are done in LEAN
https://github.com/leanprover-community/mathematics_in_lean

Once a LEAN proof exists (which is hard) it can be checked
by a simple proof checker (which is easy).

As you probably know, Intel bought Altera and created a
CPU/FPGA chip combo which is only available to FAANG
scale companies (why, Intel, why?!). AMD bought Xilinx
so they will also have a combo chip at some point.

I am targeting a CPU/FPGA combo setup.

Axiom has hundreds of mathematical algorithms. I am
concentrating on the greatest common divisor (GCD) as
it is simple, widely known, and used.

I want to prove Axiom's Lisp GCD correct using LEAN.
(This involves an enormous amount of dependent type
theory which you really don't want to know :-) )

Then I want to package the algorithm and the proof
into an AES crypto package.

When you run a program that uses GCD I want to
side-load the proof into the FPGA. The FPGA proof
runs "in parallel" with the algorithm on the CPU.

Of course, that implies that the CPU has been shown
to be correct also. I have been studying Verilog hardware
implementations of the RISC-V CPU.

A program running a series of algorithms, such as the GCD,
can use the result from one proof as an axiom for further proofs.
Thus, the proofs are threaded thru the running code in parallel
with the execution, showing that the program is correct at runtime.

Here's where the FPGA comes in.

I need a RISC-V implementation in an FPGA.
I need a proof checker in FPGA.
I need a way to validate FPGA code (nMigen, maybe).

I have pieces of all of those things "in process".

Ultimately the result is proven code from Lisp all the
way "down to the metal".

At the moment I have half-a-dozen FPGA boards
including an iCEStick, a DE10-nano, a DE1-SOC,
an iCEBreaker,  and a VELDT.

I'm doing my best to learn Verilog.

And I'm trying to get up to speed on Symbiflow.

This wasn't really a question. I just wanted to you
know that there is a potentially useful project that
is targeting your tools.

Keep up the good work.

Tim Daly
http://axiom-developer.org/~daly