Skip to content

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

Notifications You must be signed in to change notification settings

philzook58/nand2coq

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

43 Commits
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

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

About

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

Topics

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published