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.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.
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