Simple Nand2Tetris Verilog CPU
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[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 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
- 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
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
sby file
[options]
mode prove
[engines]
smtbmc z3
[script]
read -formal not.v
prep -top mynoteq
[files]
not.v