philzook58/nand2coq

Build an educational formally verified version of the Nand 2 Tetris course using Coq (and other formal tools).

nand2coq

The goal of this project is to build an educational formally verified version of the Nand 2 Tetris course using Coq (and other formal tools).

https://www.nand2tetris.org/

https://www.coursera.org/learn/build-a-computer

In the course, a computer is built from the ground up, starting from Nand gates, abstracting to larger digital circuits, a CPU, Assembly, a stack based virtual machine, and finally a high level Java-like language.

This project ideally would become a baby DeepSpec.

https://deepspec.org/

Useful Resources:

Software Foundations, your one stop shop for getting started in Coq. https://softwarefoundations.cis.upenn.edu/

Adam Chlipala's Textbooks http://adam.chlipala.net/cpdt/ http://adam.chlipala.net/frap/ http://plv.csail.mit.edu/kami/

SiFive is reimplementing Kami. A very worthy README https://github.com/sifive/Kami

Chlipala & Braibant - Featherweight Synthesis http://braibant.github.io/update/2014/07/31/fe-si.html

Proof General - A Standard Proof Assistant mode for Emacs https://proofgeneral.github.io/

Coq Reference manual. Some useful things here (descriptions of tactics etc) https://coq.inria.fr/refman/index.html

Coq Standard Library. Kind of a Nightmare to look through. https://coq.inria.fr/library/

Mathematical Components Book. A book on using Coq with the Mathemtical Components library https://math-comp.github.io/mcb/

Another Text http://ilyasergey.net/pnp/

Awesome Coq List https://github.com/uhub/awesome-coq

Programming Language Foundations - An Agda Textbook https://plfa.github.io/

Coq course https://github.com/vlopezj/coq-course

A Listing with these links and more https://avigad.github.io/formal_methods_in_education/

Haskell For Coq Programmer's http://blog.ezyang.com/2014/03/haskell-for-coq-programmers/

Formal verification of microprocessors: a first experiment with the Coq proof assistant https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.39.9165&rep=rep1&type=pdf

RISC-V formal specs: 3 Haskell, 1 SAIL, 1 Kami https://mail.haskell.org/pipermail/haskell-cafe/2019-May/131067.html

https://github.com/stonebuddha/eopl

https://project-oak.github.io/silveroak/demo/tutorial.html

https://github.com/conal/agda-hardware

Pi-Ware Agda https://drops.dagstuhl.de/opus/volltexte/2018/8479/pdf/LIPIcs-TYPES-2015-9.pdf

---

It would be super cool to actually run this on an FPGA. The open source FPGA world is blowing up

Seems like a good tutorial getting started with open source FPGA https://medium.com/@luke_73359/getting-started-with-icestorm-verilog-on-the-ice40hx1k-fpga-cbc71ad3947d https://mcmayer.net/first-steps-with-the-icestorm-toolchain/

Good beginner fpga project explanations https://www.fpga4fun.com/

Some interesting blog posts on verifying Verilog using open source tools https://zipcpu.com/

Many freely available cores https://opencores.org/

Icestorm - The project that started the open source FPGA revolution http://www.clifford.at/icestorm/

ECP5 FPGAs - A Work in progress, but I think it is getting there. By far the most powerful FPGA with open source tooling https://github.com/SymbiFlow/prjtrellis

Open Source FPGA Twitter - Good place to hear news https://twitter.com/ico_tc?lang=en

My Garbo: http://www.philipzucker.com/nand2tetris-in-verilog-and-fpga-and-coq/ http://www.philipzucker.com/simple-fpga-stuff/

Some Boards:

Icestick https://www.latticesemi.com/icestick

Icebreaker https://www.crowdsupply.com/1bitsquared/icebreaker-fpga http://icebreaker-fpga.com/

TinyFPGA https://tinyfpga.com/

Awesome HDL list https://github.com/drom/awesome-hdl