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;
PC <= AReg;
else
PC <= PC + 1;
end
//////////////////////////

//// ROM /////////////
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[0]; // instruction type. 0 = load immediate into AReg, 1 = compute alu function C command assign a = instruction[3]; // a = 0 use A as operand, if a = 1 use M as operand assign zx = instruction[4]; // x is zero assign nx = instruction[5]; // negate x assign zy = instruction[6]; // y is zero assign ny = instruction[7]; // negate y assign f = instruction[8]; // select addition vs. bitwise and assign no = instruction[9]; // negate output assign d1 = instruction[10]; // d1 controls loading into a assign d2 = instruction[11]; // d2 loads into D assign d3 = instruction[12]; // d3 loads into M (ram) assign j1 = instruction[13]; assign j2 = instruction[14]; assign j3 = instruction[15]; // 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[15] == 1; // check sign bit? Is this the right number? ///////////////////// endmodule  The testbench 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 Computer2.v to 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.

ideas:

• 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
• Koika

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
1'b1 : out <= in;
1'b0 : out <= out;
endcase
end
endmodule

module tb2();
reg clk;
wire 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;
clk = 0;
#1
#10 in = 1;
#10 in = 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


sby file

[options]
mode prove

[engines]
smtbmc z3

[script]