I feel like my standards of what is worthy of a blog post are creeping up. I don’t like that.
I also am haunted by the projects and ideas that I don’t make progress on. They just keep piling up. An old one I keep thinking I should return to with my greater wisdom is nand2coq https://github.com/philzook58/nand2coq. The idea is to try and use my fancy formal methods knowledge and apply them to the nand2tetris course. You can find the code below in the verilog folder.
Here is a pretty simple verilog implementation of a nand2tetris cpu. It’s based on a version I made a couple years ago. I inlined all the little pieces, which significantly increases the clarity I think at the expense of the point that the cpu is made of a hierarchy of smaller structures. Despite that, I suspect the implementation below is at least very close to acceptable to a fpga synthesis tool.
There is something a little more satisfying to using actual appropriate languages rather than the nand2tetris walled garden.
It can load a program from file and has a little testbench that reports the values of registers.
A problem I’ve had before is I was so focussed on getting it onto an fpga. That makes things tougher because the fpga toolchain is kind of a pain. By the time I get one up, my energy is spent for the day. sing the Icarus verilog simulator is pretty nice though and still pretty satisfying.
I hope the following is somewhat self explanatory if you’ve looked at the nand2tetris course https://www.nand2tetris.org/course I’m probably delusional on that count though. Project 5 in particular has lots of useful tidbits, such as the instruction decoding table.
`define PROGRAMFILE "setd.hack" module Computer(input clk, input reset, output [0:15] PC, output [0:15] AReg, output [0:15] DReg, output [0:15] MReg, output [0:15] instruction); reg [0:15] PC; // Current Program Counter reg [0:15] AReg; // A register reg [0:15] DReg; // D Register wire [0:15] MReg; // M Register. A Pseudo register that is actuall the output of current index of ram reg [0:15] ram[0:16383]; reg [0:15] rom[0:16383]; wire [0:15] instruction; wire writeA; // Write to A wire writeD; // Write to D wire writeM; // Write to M wire pcload; // Write to PC wire [0:15] aluOut; //////////////////////////// // Program Counter // If you want to jump assign pcload = ((j2 & zr) | (j1 & ng) | (j2 & !ng)) & i; // only jump on C commands always @(posedge clk) begin if (reset == 1'b1) PC <= 16'b0; else if (pcload == 1'b1) PC <= AReg; else PC <= PC + 1; end ////////////////////////// //// ROM ///////////// assign instruction = rom[PC]; initial begin $readmemb(`PROGRAMFILE, rom); end ///////////////////// //// RAM //////////// assign MReg = ram[AReg]; always @(posedge clk) begin // Also clear RAM on reset? if (writeM == 1'b1) ram[AReg] <= aluOut; end ///////////////////// wire a, i, zx, zy, nx, ny, f, no; wire d1, d2, d3; wire j1, j2, j3; /// CPU/////////// // Instruction bit interpretations assign i = instruction; // instruction type. 0 = load immediate into AReg, 1 = compute alu function C command assign a = instruction; // a = 0 use A as operand, if a = 1 use M as operand assign zx = instruction; // x is zero assign nx = instruction; // negate x assign zy = instruction; // y is zero assign ny = instruction; // negate y assign f = instruction; // select addition vs. bitwise and assign no = instruction; // negate output assign d1 = instruction; // d1 controls loading into a assign d2 = instruction; // d2 loads into D assign d3 = instruction; // d3 loads into M (ram) assign j1 = instruction; assign j2 = instruction; assign j3 = instruction; // If the A register should be written wire [0:15] aregIn; assign aregIn = i ? aluOut : instruction; assign writeA = !i | d1; // load the A reg if an A instruction or if that destination is set in C instruction always @(posedge clk) begin if (writeA == 1'b1) AReg <= aregIn; end // If the D register should be written. assign writeD = i & d2; always @(posedge clk) begin if (writeD == 1'b1) DReg <= aluOut; end // If the M register should be written assign writeM = i & d3; ///////////// /// ALU ///////////// wire [0:15] x; wire [0:15] y; wire [0:15] zerox; wire [0:15] zeroy; wire [0:15] notx; wire [0:15] noty; wire [0:15] andplus; assign y = a ? MReg : AReg; // The Y input to the alu is either A or M assign x = DReg; // Table 2.6 of Nand2Tetris book assign zerox = zx ? 16'h0000 : x; assign notx = nx ? ~zerox : zerox; assign zeroy = zy ? 16'h0000 : y; assign noty = ny ? ~zeroy : zeroy; assign andplus = f ? (notx + noty) : (notx & noty); assign aluOut = no ? ~andplus : andplus; assign zr = aluOut == 16'h0000; assign ng = aluOut == 1; // check sign bit? Is this the right number? ///////////////////// endmodule
module tb(); reg clk, reset; wire [15:0] PC; wire [15:0] AReg; wire [15:0] DReg; wire [15:0] MReg; wire [15:0] instruction; Computer U1(clk, reset, PC, AReg, DReg, MReg, instruction); always #5 clk <= ~clk; initial begin $monitor("%t PC = %h A = %h D = %h M = %h I = %b", $time, PC, AReg, DReg, MReg, instruction); clk = 0; reset = 1; #20 reset = 0; #100 $finish; end endmodule
You may compile a assembly program
myprog.asm (I pulled this assembler of the internet. I can’t find mine)
python assembly.py myprog
And then set the variable at the top of
myprog.hack (yes this is super janky)
And run the computer via:
iverilog Computer_tb.v Computer2.v ./a.out
Here’s a nothing program
@15 D=A M=D+1 A=M+1 D=A-1 @0 0;JMP
It compiles to the following file
0000000000001111 1110110000010000 1110011111001000 1111110111100000 1110110010010000 0000000000000000 1110101010000111
Which outputs when run
philip@philip-desktop:~/Documents/fpga/nand2coq/verilog$ iverilog Computer_tb.v Computer2.v && ./a.out WARNING: Computer2.v:37: $readmemb(setd.hack): Not enough words in the file for the requested range [0:16383]. 0 PC = xxxx A = xxxx D = xxxx M = xxxx I = xxxxxxxxxxxxxxxx 5 PC = 0000 A = xxxx D = xxxx M = xxxx I = 0000000000001111 15 PC = 0000 A = 000f D = xxxx M = xxxx I = 0000000000001111 25 PC = 0001 A = 000f D = xxxx M = xxxx I = 1110110000010000 35 PC = 0002 A = 000f D = 000f M = xxxx I = 1110011111001000 45 PC = 0003 A = 000f D = 000f M = 0010 I = 1111110111100000 55 PC = 0004 A = 0011 D = 000f M = xxxx I = 1110110010010000 65 PC = 0005 A = 0011 D = 0010 M = xxxx I = 0000000000000000 75 PC = 0006 A = 0000 D = 0010 M = xxxx I = 1110101010000111 85 PC = 0000 A = 0000 D = 0010 M = xxxx I = 0000000000001111 95 PC = 0001 A = 000f D = 0010 M = 0010 I = 1110110000010000 105 PC = 0002 A = 000f D = 000f M = 0010 I = 1110011111001000 115 PC = 0003 A = 000f D = 000f M = 0010 I = 1111110111100000
Some things that tripped me up:
- You really need to make sure you declare your variables. Verilog automatically assumes things if you don’t which screw it up. Verilog is not a good language.
- I for some reason swapped some cases
- I’m still not sure my endianness is good
- My reset logic may not be so good. I may want to reset all ram and registers. This is probably asking for weird bugs.
Bits and Bobbles
I want to verify this in some meaningful way. I suspect there are bugs in the above implementation.
- Make a linker
- Make a dsl to compile to verilog
- Verify equivalence of different implementations
- Get running on Icestick
- Quickcheck or Brute force test using verilator. Equivalence to hack interpreter
- Verilator to ocaml bindings, compile coq interpeter and compare
- Symbolic Executor
- Datalog disassembler
- Horn clause translation of hack
https://github.com/jopdorp/nand2tetris-verilog Another implementation of nand2tetris cpu in verilog. https://gitlab.com/x653/nand2tetris-fpga/ another implementation of nand2teris in verilog https://misterfpga.org/viewtopic.php?t=28
- Bluespec is quite cool
Here’s a fun idea: Use symbiyosys https://symbiyosys.readthedocs.io/en/latest/quickstart.html for nand2tetris verification. One can write a “speclike” verilog implementation and compare with a “circuitlike” implementation. Seems to work for simple stuff.
module mynot(input a, output b); nand U1(b,a,a); endmodule module mynot2(input a, output b); assign b = ~a; endmodule module myand(input a, input b, output c); wire d; nand U1(d,a,b); mynot U2(d,c); endmodule module and_spec(input a, input b, output c); assign c = a & b; endmodule module Reg(input in,input load,input clk,output reg out); always @(posedge clk) begin case (load) 1'b1 : out <= in; 1'b0 : out <= out; endcase end endmodule module tb2(); reg clk; wire out; reg in, load; Reg U1(in,load,clk,out); always #5 clk <= ~clk; initial begin $monitor("%t Reg : in = %b load = %b out = %b clk = %b", $time, in, load, out, clk); in = 0; load = 0; clk = 0; #1 #10 in = 1; #10 load = 1; #10 in = 0; #10 load = 0; #10 in = 1; #25 $finish; end endmodule /* module tb(); reg a; wire b1; mynot U1(a,b1); initial begin $monitor("mynot : a = %b b = %b", a, b1); a = 1'b0; #1 a = 1'b1; #1 $finish; end endmodule */ module mynoteq(); reg a, b; wire b1, b2; mynot U1(a,b1); mynot2 U2(a,b2); wire and1, and2; myand U3(a,b,and1); and_spec U4(a,b,and2); `ifdef FORMAL always @(*) begin assert (b1 == b2); assert (and1 == and2); end `endif endmodule
[options] mode prove [engines] smtbmc z3 [script] read -formal not.v prep -top mynoteq [files] not.v