Comparing Two Verilog CPU Implementations using EBMC
About a year ago my friends and I built a 4bit cpu out of a kit from aliexpress. https://www.philipzucker.com/td4-4bit-cpu/ It’s a lot of fun. I also think the system is so simple that is is kind of a nice target for tinkering around with formal methods.
From my understanding, the digital design world orbits around VHDL and Verilog. A confusion that can arise when a programmer sees verilog is that it is just another programming language. Yes and no. These languages play multiple roles. They can be seen and used as a sort of netlist / circuit description language, describing which subpieces are connected and how. But they can also be seen as a programming language for describing the behavior of a digital system and that is how they are used in simulation of these circuits.
Follow along on colab here https://colab.research.google.com/github/philzook58/philzook58.github.io/blob/master/pynb/2025-02-11-td4_ebmc.ipynb
High Level Interpreter of the CPU
The TD4 is designed so that the 4 high bits of an instruction are an opcode, things like MOV_A_B
Based on the current instruction we can switch on it to get the next state of the CPU.
One can write an interpreter for the CPU in a pretty straightforward style. I’m not a hardware designer. I don’t really know verilog very well. I’m just doing what makes sense to me. Do not take this as a lesson in the right way to write verilog.
A first pass at a cpu translated by chatgpt from my python model https://chatgpt.com/share/67aadd55-11b4-8008-9c78-080a836d2c92 . It took a couple iterations and then I fiddled with some bits. There’s no assurance my python model was correct either.
Googling around there seem to be some footguns possible with the case statement. It is nice though.
%%file /tmp/td4_high.sv
`timescale 1ns/1ps
module td4_cpu_high (
input clk,
input notreset,
input [7:0] insn, // Program ROM (16 instructions)
input [3:0] inp, // Input switches
output reg [3:0] outp, // Output LEDs
output reg [3:0] A, // Register A
output reg [3:0] B, // Register B
output reg [3:0] pc // Program Counter
);
reg carry;
// Instruction opcodes
parameter ADD_A_IM = 4'b0000, MOV_A_B = 4'b0001, IN_A = 4'b0010, MOV_A_IM = 4'b0011;
parameter MOV_B_A = 4'b0100, ADD_B_IM = 4'b0101, IN_B = 4'b0110, MOV_B_IM = 4'b0111;
parameter OUT_B = 4'b1001, OUT_IM = 4'b1011, JNC_IM = 4'b1110, JMP_IM = 4'b1111;
always @(posedge clk or negedge notreset) begin
if (!notreset) begin
A <= 4'b0000;
B <= 4'b0000;
pc <= 4'b0000;
carry <= 1'b0;
outp <= 4'b0000;
end else begin
case (insn[7:4])
ADD_A_IM: {carry, A} <= A + insn[3:0]; // Add immediate to A
MOV_A_B: A <= B; // Move B to A
IN_A: A <= inp; // Read input to A
MOV_A_IM: A <= insn[3:0]; // Move immediate to A
MOV_B_A: B <= A; // Move A to B
ADD_B_IM: {carry, B} <= B + insn[3:0]; // Add immediate to B
IN_B: B <= inp; // Read input to B
MOV_B_IM: B <= insn[3:0]; // Move immediate to B
OUT_B: outp <= B; // Output B to LEDs
OUT_IM: outp <= insn[3:0]; // Output immediate to LEDs
endcase
// Control Flow (PC updates)
case (insn[7:4])
JNC_IM: pc <= (!carry) ? insn[3:0] : pc + 1; // Jump if no carry
JMP_IM: pc <= insn[3:0]; // Unconditional jump
default: pc <= pc + 1; // Increment PC normally
endcase
end
end
endmodule
Overwriting /tmp/td4_high.sv
Chip Level Model of CPU
But we can also write a lower level formulation, modelling chip by chip and interconnecting them according the the schematic. This is using verilog more according to its hardware description language sense.
The basic structure of the computer is:
- There are 4 4bit registers A,B,Out,PC implemented using counter circuits. Only PC has the counting enabled.
- 2 multiplexers select operands from A,B,IN,0.
- An adder can combine the operands with the immediate value which is the 4 lowest bits of the instruction.
- The command decoder is some custom digital logic
The high level diagram
The schematic.
I made this verilog by going through chip by chip, kind of glancing at the datasheet and making some best guesses. Don’t put this in your life support machine.
I’ve noted before in my previous post that the schematic is wrong in the command decoder. I realized this again when I started emulating using iverilog
%%file /tmp/td4_low.sv
`timescale 1ns/1ps
module counter_74HC161(
input [3:0] abcd,
input enable,
input notreset,
input notld,
input clk,
output reg [3:0] qabcd
);
always @(posedge clk or negedge notreset)
begin
if (!notreset)
qabcd <= 4'b0000; // Reset counter
else if (!notld)
qabcd <= abcd; // Load input value
else if (enable)
qabcd <= qabcd + 1; // Increment counter
else
qabcd <= qabcd; // Hold counter
end
endmodule
module adder_74HC283(
input [3:0] a,
input [3:0] b,
input cin,
output [3:0] s,
output cout
);
assign {cout, s} = a + b + cin;
endmodule
module data_select_74HC153(
input [3:0] a,
input [3:0] b,
input [1:0] sel,
output [1:0] y
);
assign y[0] = a[sel];
assign y[1] = b[sel];
endmodule
module command_decoder(
input notcarry,
input [7:0] d,
output [3:0] l,
output sel_a
);
// It is unlikely I got this right. Well. Seems ok so far
wire s3 = d[4] | d[7];
wire s6 = d[4] | notcarry;
wire s12 = !d[6];
assign l[0] = d[7] | d[6];
assign l[1] = s12 | d[7];
assign l[2] = !(d[7] & s12);
assign l[3] = !(s6 & d[7] & d[6]);
assign sel_a = s3;
endmodule
module td4_cpu_low(
input clk,
input notreset, // reset signal
input [7:0] insn, // instruction
input [3:0] inp, // input switches
output reg [3:0] A,
output reg [3:0] B,
output reg [3:0] pc,
output reg [3:0] outp
);
wire [3:0] alu_out;
wire [3:0] notload;
wire cout;
wire [3:0] imm; // immediate data
wire sel_a;
wire sel_b = insn[5];
wire [3:0] opa;
wire [3:0] opb = insn[3:0];
assign imm = insn[3:0];
adder_74HC283 alu(
.a(opa),
.b(opb),
.cin(1'b0),
.s(alu_out),
.cout(cout)
);
data_select_74HC153 mux1(
.a({1'b0, inp[0], B[0], A[0]}),
.b({1'b0, inp[1], B[1], A[1]}),
.sel({sel_b, sel_a}),
.y(opa[1:0])
);
data_select_74HC153 mux2(
.a({1'b0, inp[2], B[2], A[2]}),
.b({1'b0, inp[3], B[3], A[3]}),
.sel({sel_b, sel_a}),
.y(opa[3:2])
);
reg prev_carry;
always @(posedge clk or negedge notreset)
begin
if (!notreset)
prev_carry <= 1'b0;
else
prev_carry <= cout;
end
command_decoder cmd(
.notcarry(!prev_carry),
.d(insn),
.l(notload),
.sel_a(sel_a)
);
counter_74HC161 a_counter(
.abcd(alu_out),
.notreset(notreset),
.enable(1'b0),
.notld(notload[0]),
.clk(clk),
.qabcd(A)
);
counter_74HC161 b_counter(
.abcd(alu_out),
.notreset(notreset),
.enable(1'b0),
.notld(notload[1]),
.clk(clk),
.qabcd(B)
);
counter_74HC161 out_counter(
.abcd(alu_out),
.notreset(notreset),
.enable(1'b0),
.notld(notload[2]),
.clk(clk),
.qabcd(outp)
);
counter_74HC161 pc_counter(
.abcd(alu_out),
.notreset(notreset),
.enable(1'b1),
.notld(notload[3]),
.clk(clk),
.qabcd(pc)
);
endmodule
Overwriting /tmp/td4_low.sv
Running the CPU
We can run both version of the CPU in a simulator.
I’m using icarus verilog which is pretty easy to use. In verilog, you often have to make testbenches which drive the circuits of interest. These testbenches use verilog like a programming language and can use non synthesizable constructs. One could also use verilator whicvh transpiles verilog to C++ and drive it using C++ code.
I hardcoded a couple programs into the source. You can also read them from file (readmemh).
%%file /tmp/td4_tb.sv
`timescale 1ns/1ps
module tb_td4_cpu;
// Instruction opcodes
parameter ADD_A_IM = 4'b0000, MOV_A_B = 4'b0001, IN_A = 4'b0010, MOV_A_IM = 4'b0011;
parameter MOV_B_A = 4'b0100, ADD_B_IM = 4'b0101, IN_B = 4'b0110, MOV_B_IM = 4'b0111;
parameter OUT_B = 4'b1001, OUT_IM = 4'b1011, JNC_IM = 4'b1110, JMP_IM = 4'b1111;
reg clk;
reg notreset;
reg [7:0] insn;
reg [7:0] prog [0:15];
reg [3:0] inp;
wire [3:0] pc;
wire [3:0] outp;
wire [3:0] A;
wire [3:0] B;
wire [3:0] pc_low;
wire [3:0] outp_low;
wire [3:0] A_low;
wire [3:0] B_low;
assign insn = prog[pc];
`ifdef PROGADDB
// A simple program to add 1 to B, move it to out, and then jump back to start
initial begin
prog[0] = {ADD_B_IM, 4'b0001}; // ADD B 1
prog[1] = {OUT_B, 4'b0000}; // OUT B
prog[2] = {JMP_IM, 4'b0000}; // JMP 0
end
`endif
`ifdef PROGJNC
// Fiddling around with conditional hjumps
initial begin
prog[0] = {ADD_B_IM, 4'b1111}; //
//prog[1] = {ADD_B_IM, 4'b0010}; //
prog[1] = {JNC_IM, 4'b0000}; //
prog[2] = {JMP_IM, 4'b0001}; // JMP 0
end
`endif
always @(*) begin
assert (pc == pc_low) else $error("PC mismatch at time %0t", $time);
assert (outp == outp_low) else $error("OUTP mismatch at time %0t", $time);
assert (A == A_low) else $error("A mismatch at time %0t", $time);
assert (B == B_low) else $error("B mismatch at time %0t", $time);
end
// Instantiate the TD4 CPU
td4_cpu_high uut_high (
.clk(clk),
.notreset(notreset),
.insn(insn),
.inp(inp),
.pc(pc),
.A(A),
.B(B),
.outp(outp)
);
td4_cpu_low uut_low (
.clk(clk),
.notreset(notreset),
.insn(insn),
.inp(inp),
.pc(pc_low),
.A(A_low),
.B(B_low),
.outp(outp_low)
);
always #10 clk = ~clk;
initial begin
$display("Time\t INSN INP |Hi PC A B OUTP |Lo PC A B OUTP");
$monitor("%0t\t %b %b | %b %b %b %b | %b %b %b %b",
$time, insn, inp, pc, A, B, outp, pc_low, A_low, B_low, outp_low);
clk = 0;
notreset = 0; // Apply reset
inp = 4'b0000;
#20 notreset = 1; // Release reset
// Run it for a while
#300 $finish;
end
endmodule
Overwriting /tmp/td4_tb.sv
We can run the first program which is a simple loop adding 1 to B, moving B to Out and then jumping back to the beginning. We can see both version of the CPU running side by side. An assertion is triggered if their output does not agree. It does agree here.
! iverilog -DPROGADDB -Wall -g2012 -o /tmp/td4 /tmp/td4_high.sv /tmp/td4_low.sv /tmp/td4_tb.sv && vvp /tmp/td4
Time INSN INP |Hi PC A B OUTP |Lo PC A B OUTP
0 01010001 0000 | 0000 0000 0000 0000 | 0000 0000 0000 0000
30000 10010000 0000 | 0001 0000 0001 0000 | 0001 0000 0001 0000
50000 11110000 0000 | 0010 0000 0001 0001 | 0010 0000 0001 0001
70000 01010001 0000 | 0000 0000 0001 0001 | 0000 0000 0001 0001
90000 10010000 0000 | 0001 0000 0010 0001 | 0001 0000 0010 0001
110000 11110000 0000 | 0010 0000 0010 0010 | 0010 0000 0010 0010
130000 01010001 0000 | 0000 0000 0010 0010 | 0000 0000 0010 0010
150000 10010000 0000 | 0001 0000 0011 0010 | 0001 0000 0011 0010
170000 11110000 0000 | 0010 0000 0011 0011 | 0010 0000 0011 0011
190000 01010001 0000 | 0000 0000 0011 0011 | 0000 0000 0011 0011
210000 10010000 0000 | 0001 0000 0100 0011 | 0001 0000 0100 0011
230000 11110000 0000 | 0010 0000 0100 0100 | 0010 0000 0100 0100
250000 01010001 0000 | 0000 0000 0100 0100 | 0000 0000 0100 0100
270000 10010000 0000 | 0001 0000 0101 0100 | 0001 0000 0101 0100
290000 11110000 0000 | 0010 0000 0101 0101 | 0010 0000 0101 0101
310000 01010001 0000 | 0000 0000 0101 0101 | 0000 0000 0101 0101
/tmp/td4_tb.sv:85: $finish called at 320000 (1ps)
EBMC
But I can also make a testbench to run them through EBMC, which is a bounded model checker for verilog. https://www.cprover.org/ebmc/ Download here and install https://github.com/diffblue/hw-cbmc/releases . EBMC is a cousin of CBMC and Kani for C and Rust respectively, which I’m pretty bullish on.
Using a bounded model checker lets the instruction run be symbolically chosen, which is more complete and easier than me writing a ton of programs (I suppose I could fuzz them too? Wouldn’t be so bad). The key is to be feeding the same stuff into both versions of the cpu. Even though I don’t have confidence on either implementation, any difference in behavior is something to look into. In the end of the day, this is almost all formal methods can be. Comparing one way of saying a thing to another. Often these are a logicy spec and a programmy implementation, but they can be two programs too.
I’m a little unclear on exactly what is supported in ebmc vs iverilog. There are some features in all parts of the Venn diagram of support, so I couldn’t easily make one mega testbench.
%%file /tmp/td4_tb_ebmc.sv
`timescale 1ns/1ps
module main(
input clk,
input notreset,
input [7:0] insn,
input [3:0] inp);
wire [3:0] pc;
wire [3:0] outp;
wire [3:0] A;
wire [3:0] B;
wire [3:0] pc_low;
wire [3:0] outp_low;
wire [3:0] A_low;
wire [3:0] B_low;
// Instantiate the TD4 CPU
td4_cpu_high uut_high (
.clk(clk),
.notreset(notreset),
.insn(insn),
.inp(inp),
.pc(pc),
.A(A),
.B(B),
.outp(outp)
);
td4_cpu_low uut_low (
.clk(clk),
.notreset(notreset),
.insn(insn),
.inp(inp),
.pc(pc_low),
.A(A_low),
.B(B_low),
.outp(outp_low)
);
assert property (notreset == 0 | A_low == A);
assert property (notreset == 0 | B_low == B);
assert property (notreset == 0 | pc_low == pc);
assert property (notreset == 0 | outp_low == outp);
endmodule
Overwriting /tmp/td4_tb_ebmc.sv
I run with --reset to reset the thing at the start. I couldn’t figure out how to just assign the initial states to each other.
We get a counterexample right off the bat. It’s a lot of info. There are probably ways to prune it down.
! ebmc /tmp/td4_high.sv /tmp/td4_low.sv /tmp/td4_tb_ebmc.sv --top main --reset "notreset==0" --trace --bound 2 --property main.assert.1
Parsing /tmp/td4_high.sv
Parsing /tmp/td4_low.sv
Parsing /tmp/td4_tb_ebmc.sv
Converting
Type-checking Verilog::adder_74HC283
Type-checking Verilog::command_decoder
Type-checking Verilog::counter_74HC161
Type-checking Verilog::data_select_74HC153
Type-checking Verilog::td4_cpu_high
Type-checking Verilog::td4_cpu_low
Making td4_cpu_low.A a wire
Making td4_cpu_low.B a wire
Making td4_cpu_low.outp a wire
Making td4_cpu_low.pc a wire
Type-checking Verilog::main
Generating Decision Problem
Using MiniSAT 2.2.1 with simplifier
Properties
Solving with propositional reduction
SAT checker: instance is SATISFIABLE
SAT: path found
SAT checker inconsistent: instance is UNSATISFIABLE
UNSAT: No path found within bound
** Results:
[main.assert.1] always main.notreset == 0 || main.A_low == main.A: [91mREFUTED[0m
Counterexample:
Transition system state 0
----------------------------------------------------
main.clk = 0
main.notreset = 0
main.insn = 1 (00000001)
main.inp = 4'b0000 (0000)
main.pc = 4'b0000 (0000)
main.outp = 4'b0000 (0000)
main.A = 4'b0000 (0000)
main.B = 4'b0000 (0000)
main.pc_low = 4'b0000 (0000)
main.outp_low = 4'b0000 (0000)
main.A_low = 4'b0000 (0000)
main.B_low = 4'b0000 (0000)
main.uut_high.clk = 0
main.uut_high.notreset = 0
main.uut_high.insn = 1 (00000001)
main.uut_high.inp = 4'b0000 (0000)
main.uut_high.outp = 4'b0000 (0000)
main.uut_high.A = 4'b0000 (0000)
main.uut_high.B = 4'b0000 (0000)
main.uut_high.pc = 4'b0000 (0000)
main.uut_high.carry = 0
main.uut_high.ADD_A_IM = 4'b0000 (0000)
main.uut_high.MOV_A_B = 4'b0001 (0001)
main.uut_high.IN_A = 4'b0010 (0010)
main.uut_high.MOV_A_IM = 4'b0011 (0011)
main.uut_high.MOV_B_A = 4'b0100 (0100)
main.uut_high.ADD_B_IM = 4'b0101 (0101)
main.uut_high.IN_B = 4'b0110 (0110)
main.uut_high.MOV_B_IM = 4'b0111 (0111)
main.uut_high.OUT_B = 4'b1001 (1001)
main.uut_high.OUT_IM = 4'b1011 (1011)
main.uut_high.JNC_IM = 4'b1110 (1110)
main.uut_high.JMP_IM = 4'b1111 (1111)
main.uut_low.clk = 0
main.uut_low.notreset = 0
main.uut_low.insn = 1 (00000001)
main.uut_low.inp = 4'b0000 (0000)
main.uut_low.A = 4'b0000 (0000)
main.uut_low.B = 4'b0000 (0000)
main.uut_low.pc = 4'b0000 (0000)
main.uut_low.outp = 4'b0000 (0000)
main.uut_low.alu_out = 4'b0001 (0001)
main.uut_low.notload = 4'b1110 (1110)
main.uut_low.cout = 0
main.uut_low.imm = 4'b0001 (0001)
main.uut_low.sel_a = 0
main.uut_low.sel_b = 0
main.uut_low.opa = 4'b0000 (0000)
main.uut_low.opb = 4'b0001 (0001)
main.uut_low.prev_carry = 0
main.uut_low.alu.a = 4'b0000 (0000)
main.uut_low.alu.b = 4'b0001 (0001)
main.uut_low.alu.cin = 0
main.uut_low.alu.s = 4'b0001 (0001)
main.uut_low.alu.cout = 0
main.uut_low.mux1.a = 4'b0000 (0000)
main.uut_low.mux1.b = 4'b0000 (0000)
main.uut_low.mux1.sel = 2'b00 (00)
main.uut_low.mux1.y = 2'b00 (00)
main.uut_low.mux2.a = 4'b0000 (0000)
main.uut_low.mux2.b = 4'b0000 (0000)
main.uut_low.mux2.sel = 2'b00 (00)
main.uut_low.mux2.y = 2'b00 (00)
main.uut_low.cmd.notcarry = 1
main.uut_low.cmd.d = 1 (00000001)
main.uut_low.cmd.l = 4'b1110 (1110)
main.uut_low.cmd.sel_a = 0
main.uut_low.cmd.s3 = 0
main.uut_low.cmd.s6 = 1
main.uut_low.cmd.s12 = 1
main.uut_low.a_counter.abcd = 4'b0001 (0001)
main.uut_low.a_counter.enable = 0
main.uut_low.a_counter.notreset = 0
main.uut_low.a_counter.notld = 0
main.uut_low.a_counter.clk = 0
main.uut_low.a_counter.qabcd = 4'b0000 (0000)
main.uut_low.b_counter.abcd = 4'b0001 (0001)
main.uut_low.b_counter.enable = 0
main.uut_low.b_counter.notreset = 0
main.uut_low.b_counter.notld = 1
main.uut_low.b_counter.clk = 0
main.uut_low.b_counter.qabcd = 4'b0000 (0000)
main.uut_low.out_counter.abcd = 4'b0001 (0001)
main.uut_low.out_counter.enable = 0
main.uut_low.out_counter.notreset = 0
main.uut_low.out_counter.notld = 1
main.uut_low.out_counter.clk = 0
main.uut_low.out_counter.qabcd = 4'b0000 (0000)
main.uut_low.pc_counter.abcd = 4'b0001 (0001)
main.uut_low.pc_counter.enable = 1
main.uut_low.pc_counter.notreset = 0
main.uut_low.pc_counter.notld = 1
main.uut_low.pc_counter.clk = 0
main.uut_low.pc_counter.qabcd = 4'b0000 (0000)
Transition system state 1
----------------------------------------------------
main.clk = 0
main.notreset = 1
main.insn = 34 (00100010)
main.inp = 4'b1100 (1100)
main.pc = 4'b0000 (0000)
main.outp = 4'b0000 (0000)
main.A = 4'b0000 (0000)
main.B = 4'b0000 (0000)
main.pc_low = 4'b0000 (0000)
main.outp_low = 4'b0000 (0000)
main.A_low = 4'b0000 (0000)
main.B_low = 4'b0000 (0000)
main.uut_high.clk = 0
main.uut_high.notreset = 1
main.uut_high.insn = 34 (00100010)
main.uut_high.inp = 4'b1100 (1100)
main.uut_high.outp = 4'b0000 (0000)
main.uut_high.A = 4'b0000 (0000)
main.uut_high.B = 4'b0000 (0000)
main.uut_high.pc = 4'b0000 (0000)
main.uut_high.carry = 0
main.uut_high.ADD_A_IM = 4'b0000 (0000)
main.uut_high.MOV_A_B = 4'b0001 (0001)
main.uut_high.IN_A = 4'b0010 (0010)
main.uut_high.MOV_A_IM = 4'b0011 (0011)
main.uut_high.MOV_B_A = 4'b0100 (0100)
main.uut_high.ADD_B_IM = 4'b0101 (0101)
main.uut_high.IN_B = 4'b0110 (0110)
main.uut_high.MOV_B_IM = 4'b0111 (0111)
main.uut_high.OUT_B = 4'b1001 (1001)
main.uut_high.OUT_IM = 4'b1011 (1011)
main.uut_high.JNC_IM = 4'b1110 (1110)
main.uut_high.JMP_IM = 4'b1111 (1111)
main.uut_low.clk = 0
main.uut_low.notreset = 1
main.uut_low.insn = 34 (00100010)
main.uut_low.inp = 4'b1100 (1100)
main.uut_low.A = 4'b0000 (0000)
main.uut_low.B = 4'b0000 (0000)
main.uut_low.pc = 4'b0000 (0000)
main.uut_low.outp = 4'b0000 (0000)
main.uut_low.alu_out = 4'b1110 (1110)
main.uut_low.notload = 4'b1110 (1110)
main.uut_low.cout = 0
main.uut_low.imm = 4'b0010 (0010)
main.uut_low.sel_a = 0
main.uut_low.sel_b = 1
main.uut_low.opa = 4'b1100 (1100)
main.uut_low.opb = 4'b0010 (0010)
main.uut_low.prev_carry = 0
main.uut_low.alu.a = 4'b1100 (1100)
main.uut_low.alu.b = 4'b0010 (0010)
main.uut_low.alu.cin = 0
main.uut_low.alu.s = 4'b1110 (1110)
main.uut_low.alu.cout = 0
main.uut_low.mux1.a = 4'b0000 (0000)
main.uut_low.mux1.b = 4'b0000 (0000)
main.uut_low.mux1.sel = 2'b10 (10)
main.uut_low.mux1.y = 2'b00 (00)
main.uut_low.mux2.a = 4'b0100 (0100)
main.uut_low.mux2.b = 4'b0100 (0100)
main.uut_low.mux2.sel = 2'b10 (10)
main.uut_low.mux2.y = 2'b11 (11)
main.uut_low.cmd.notcarry = 1
main.uut_low.cmd.d = 34 (00100010)
main.uut_low.cmd.l = 4'b1110 (1110)
main.uut_low.cmd.sel_a = 0
main.uut_low.cmd.s3 = 0
main.uut_low.cmd.s6 = 1
main.uut_low.cmd.s12 = 1
main.uut_low.a_counter.abcd = 4'b1110 (1110)
main.uut_low.a_counter.enable = 0
main.uut_low.a_counter.notreset = 1
main.uut_low.a_counter.notld = 0
main.uut_low.a_counter.clk = 0
main.uut_low.a_counter.qabcd = 4'b0000 (0000)
main.uut_low.b_counter.abcd = 4'b1110 (1110)
main.uut_low.b_counter.enable = 0
main.uut_low.b_counter.notreset = 1
main.uut_low.b_counter.notld = 1
main.uut_low.b_counter.clk = 0
main.uut_low.b_counter.qabcd = 4'b0000 (0000)
main.uut_low.out_counter.abcd = 4'b1110 (1110)
main.uut_low.out_counter.enable = 0
main.uut_low.out_counter.notreset = 1
main.uut_low.out_counter.notld = 1
main.uut_low.out_counter.clk = 0
main.uut_low.out_counter.qabcd = 4'b0000 (0000)
main.uut_low.pc_counter.abcd = 4'b1110 (1110)
main.uut_low.pc_counter.enable = 1
main.uut_low.pc_counter.notreset = 1
main.uut_low.pc_counter.notld = 1
main.uut_low.pc_counter.clk = 0
main.uut_low.pc_counter.qabcd = 4'b0000 (0000)
Transition system state 2
----------------------------------------------------
main.clk = 0
main.notreset = 1
main.insn = 36 (00100100)
main.inp = 4'b0000 (0000)
main.pc = 4'b0001 (0001)
main.outp = 4'b0000 (0000)
main.A = 4'b1100 (1100)
main.B = 4'b0000 (0000)
main.pc_low = 4'b0001 (0001)
main.outp_low = 4'b0000 (0000)
main.A_low = 4'b1110 (1110)
main.B_low = 4'b0000 (0000)
main.uut_high.clk = 0
main.uut_high.notreset = 1
main.uut_high.insn = 36 (00100100)
main.uut_high.inp = 4'b0000 (0000)
main.uut_high.outp = 4'b0000 (0000)
main.uut_high.A = 4'b1100 (1100)
main.uut_high.B = 4'b0000 (0000)
main.uut_high.pc = 4'b0001 (0001)
main.uut_high.carry = 0
main.uut_high.ADD_A_IM = 4'b0000 (0000)
main.uut_high.MOV_A_B = 4'b0001 (0001)
main.uut_high.IN_A = 4'b0010 (0010)
main.uut_high.MOV_A_IM = 4'b0011 (0011)
main.uut_high.MOV_B_A = 4'b0100 (0100)
main.uut_high.ADD_B_IM = 4'b0101 (0101)
main.uut_high.IN_B = 4'b0110 (0110)
main.uut_high.MOV_B_IM = 4'b0111 (0111)
main.uut_high.OUT_B = 4'b1001 (1001)
main.uut_high.OUT_IM = 4'b1011 (1011)
main.uut_high.JNC_IM = 4'b1110 (1110)
main.uut_high.JMP_IM = 4'b1111 (1111)
main.uut_low.clk = 0
main.uut_low.notreset = 1
main.uut_low.insn = 36 (00100100)
main.uut_low.inp = 4'b0000 (0000)
main.uut_low.A = 4'b1110 (1110)
main.uut_low.B = 4'b0000 (0000)
main.uut_low.pc = 4'b0001 (0001)
main.uut_low.outp = 4'b0000 (0000)
main.uut_low.alu_out = 4'b0100 (0100)
main.uut_low.notload = 4'b1110 (1110)
main.uut_low.cout = 0
main.uut_low.imm = 4'b0100 (0100)
main.uut_low.sel_a = 0
main.uut_low.sel_b = 1
main.uut_low.opa = 4'b0000 (0000)
main.uut_low.opb = 4'b0100 (0100)
main.uut_low.prev_carry = 0
main.uut_low.alu.a = 4'b0000 (0000)
main.uut_low.alu.b = 4'b0100 (0100)
main.uut_low.alu.cin = 0
main.uut_low.alu.s = 4'b0100 (0100)
main.uut_low.alu.cout = 0
main.uut_low.mux1.a = 4'b0000 (0000)
main.uut_low.mux1.b = 4'b0001 (0001)
main.uut_low.mux1.sel = 2'b10 (10)
main.uut_low.mux1.y = 2'b00 (00)
main.uut_low.mux2.a = 4'b0001 (0001)
main.uut_low.mux2.b = 4'b0001 (0001)
main.uut_low.mux2.sel = 2'b10 (10)
main.uut_low.mux2.y = 2'b00 (00)
main.uut_low.cmd.notcarry = 1
main.uut_low.cmd.d = 36 (00100100)
main.uut_low.cmd.l = 4'b1110 (1110)
main.uut_low.cmd.sel_a = 0
main.uut_low.cmd.s3 = 0
main.uut_low.cmd.s6 = 1
main.uut_low.cmd.s12 = 1
main.uut_low.a_counter.abcd = 4'b0100 (0100)
main.uut_low.a_counter.enable = 0
main.uut_low.a_counter.notreset = 1
main.uut_low.a_counter.notld = 0
main.uut_low.a_counter.clk = 0
main.uut_low.a_counter.qabcd = 4'b1110 (1110)
main.uut_low.b_counter.abcd = 4'b0100 (0100)
main.uut_low.b_counter.enable = 0
main.uut_low.b_counter.notreset = 1
main.uut_low.b_counter.notld = 1
main.uut_low.b_counter.clk = 0
main.uut_low.b_counter.qabcd = 4'b0000 (0000)
main.uut_low.out_counter.abcd = 4'b0100 (0100)
main.uut_low.out_counter.enable = 0
main.uut_low.out_counter.notreset = 1
main.uut_low.out_counter.notld = 1
main.uut_low.out_counter.clk = 0
main.uut_low.out_counter.qabcd = 4'b0000 (0000)
main.uut_low.pc_counter.abcd = 4'b0100 (0100)
main.uut_low.pc_counter.enable = 1
main.uut_low.pc_counter.notreset = 1
main.uut_low.pc_counter.notld = 1
main.uut_low.pc_counter.clk = 0
main.uut_low.pc_counter.qabcd = 4'b0001 (0001)
I was suspecting there would be trouble around the carry operation. After looking it over and fixing up some bugs, I wrote a testbench to run through iverilog, which is more readable.
The issue is that I don’t reset the carry flag enough in my (or chatgpt’s) first pass at the high level interpreter. For example, jumps should clear the carry.
Also, I realzied in the previous post that many of the operations called “mov” are not moves, but are really adds that also accept the immediate. This was useful for shaving some instructions off. Again, the thing is wired up so that the alu always receives the immeidate value from the instruction. The actually get a mov, you need the immediate to be 0.
! iverilog -DPROGJNC -Wall -g2012 -o /tmp/td4 /tmp/td4_high.sv /tmp/td4_low.sv /tmp/td4_tb.sv && vvp /tmp/td4
Time INSN INP |Hi PC A B OUTP |Lo PC A B OUTP
0 01011111 0000 | 0000 0000 0000 0000 | 0000 0000 0000 0000
30000 11100000 0000 | 0001 0000 1111 0000 | 0001 0000 1111 0000
50000 01011111 0000 | 0000 0000 1111 0000 | 0000 0000 1111 0000
70000 11100000 0000 | 0001 0000 1110 0000 | 0001 0000 1110 0000
90000 11110001 0000 | 0010 0000 1110 0000 | 0010 0000 1110 0000
110000 11100000 0000 | 0001 0000 1110 0000 | 0001 0000 1110 0000
ERROR: /tmp/td4_tb.sv:48: PC mismatch at time 130000
Time: 130000 Scope: tb_td4_cpu
130000 11110001 0000 | 0010 0000 1110 0000 | 0000 0000 1110 0000
150000 11100000 0000 | 0001 0000 1110 0000 | 0001 0000 1110 0000
ERROR: /tmp/td4_tb.sv:48: PC mismatch at time 170000
Time: 170000 Scope: tb_td4_cpu
170000 11110001 0000 | 0010 0000 1110 0000 | 0000 0000 1110 0000
190000 11100000 0000 | 0001 0000 1110 0000 | 0001 0000 1110 0000
ERROR: /tmp/td4_tb.sv:48: PC mismatch at time 210000
Time: 210000 Scope: tb_td4_cpu
210000 11110001 0000 | 0010 0000 1110 0000 | 0000 0000 1110 0000
230000 11100000 0000 | 0001 0000 1110 0000 | 0001 0000 1110 0000
ERROR: /tmp/td4_tb.sv:48: PC mismatch at time 250000
Time: 250000 Scope: tb_td4_cpu
250000 11110001 0000 | 0010 0000 1110 0000 | 0000 0000 1110 0000
270000 11100000 0000 | 0001 0000 1110 0000 | 0001 0000 1110 0000
ERROR: /tmp/td4_tb.sv:48: PC mismatch at time 290000
Time: 290000 Scope: tb_td4_cpu
290000 11110001 0000 | 0010 0000 1110 0000 | 0000 0000 1110 0000
310000 11100000 0000 | 0001 0000 1110 0000 | 0001 0000 1110 0000
/tmp/td4_tb.sv:95: $finish called at 320000 (1ps)
So I can write a fixed up version of the high level interpreter. Really, carrys should happen all over the place. The carry flag is unconditionally updated from the alu. This is not uncommon that the carry flag is clobbered by most operations.
%%file /tmp/td4_high2.sv
`timescale 1ns/1ps
module td4_cpu_high (
input clk,
input notreset,
input [7:0] insn, // Program ROM (16 instructions)
input [3:0] inp, // Input switches
output reg [3:0] outp, // Output LEDs
output reg [3:0] A, // Register A
output reg [3:0] B, // Register B
output reg [3:0] pc // Program Counter
);
reg carry;
// Instruction opcodes
parameter ADD_A_IM = 4'b0000, MOV_A_B = 4'b0001, IN_A = 4'b0010, MOV_A_IM = 4'b0011;
parameter MOV_B_A = 4'b0100, ADD_B_IM = 4'b0101, IN_B = 4'b0110, MOV_B_IM = 4'b0111;
parameter OUT_B = 4'b1001, OUT_IM = 4'b1011, JNC_IM = 4'b1110, JMP_IM = 4'b1111;
always @(posedge clk or negedge notreset) begin
if (!notreset) begin
A <= 4'b0000;
B <= 4'b0000;
pc <= 4'b0000;
carry <= 1'b0;
outp <= 4'b0000;
end else begin
case (insn[7:4])
ADD_A_IM: {carry, A} <= A + insn[3:0]; // Add immediate to A
MOV_A_B: {carry, A} <= B + insn[3:0]; // ACTUALLY add immedate also
IN_A: {carry, A} <= inp + insn[3:0]; // Read input to A
MOV_A_IM: {carry, A} <= insn[3:0]; // Move immediate to A
MOV_B_A: {carry, B} <= A + insn[3:0]; // Move A to B
ADD_B_IM: {carry, B} <= B + insn[3:0]; // Add immediate to B
IN_B: {carry, B} <= inp + insn[3:0]; // Read input to B
MOV_B_IM: {carry, B} <= insn[3:0]; // Move immediate to B
OUT_B: {carry, outp} <= B + insn[3:0]; // Output B to LEDs
OUT_IM: {carry, outp} <= insn[3:0]; // Output immediate to LEDs
endcase
// Control Flow (PC updates)
case (insn[7:4])
JNC_IM:
begin
pc <= (!carry) ? insn[3:0] : pc + 1; // Jump if no carry
carry <= 1'b0;
end
JMP_IM:
begin
pc <= insn[3:0]; // Unconditional jump
carry <= 1'b0;
end
default: pc <= pc + 1; // Increment PC normally
endcase
end
end
endmodule
Overwriting /tmp/td4_high2.sv
! ebmc /tmp/td4_high2.sv /tmp/td4_low.sv /tmp/td4_tb_ebmc.sv --top main --reset "notreset==0" --trace --bound 2 --property main.assert.3
Parsing /tmp/td4_high2.sv
Parsing /tmp/td4_low.sv
Parsing /tmp/td4_tb_ebmc.sv
Converting
Type-checking Verilog::adder_74HC283
Type-checking Verilog::command_decoder
Type-checking Verilog::counter_74HC161
Type-checking Verilog::data_select_74HC153
Type-checking Verilog::td4_cpu_high
Type-checking Verilog::td4_cpu_low
Making td4_cpu_low.A a wire
Making td4_cpu_low.B a wire
Making td4_cpu_low.outp a wire
Making td4_cpu_low.pc a wire
Type-checking Verilog::main
Generating Decision Problem
Using MiniSAT 2.2.1 with simplifier
Properties
Solving with propositional reduction
SAT checker: instance is SATISFIABLE
SAT: path found
SAT checker inconsistent: instance is UNSATISFIABLE
UNSAT: No path found within bound
** Results:
[main.assert.3] always main.notreset == 0 || main.pc_low == main.pc: [91mREFUTED[0m
Counterexample:
Transition system state 0
----------------------------------------------------
main.clk = 0
main.notreset = 0
main.insn = 1 (00000001)
main.inp = 4'b0000 (0000)
main.pc = 4'b0000 (0000)
main.outp = 4'b0000 (0000)
main.A = 4'b0000 (0000)
main.B = 4'b0000 (0000)
main.pc_low = 4'b0000 (0000)
main.outp_low = 4'b0000 (0000)
main.A_low = 4'b0000 (0000)
main.B_low = 4'b0000 (0000)
main.uut_high.clk = 0
main.uut_high.notreset = 0
main.uut_high.insn = 1 (00000001)
main.uut_high.inp = 4'b0000 (0000)
main.uut_high.outp = 4'b0000 (0000)
main.uut_high.A = 4'b0000 (0000)
main.uut_high.B = 4'b0000 (0000)
main.uut_high.pc = 4'b0000 (0000)
main.uut_high.carry = 0
main.uut_high.ADD_A_IM = 4'b0000 (0000)
main.uut_high.MOV_A_B = 4'b0001 (0001)
main.uut_high.IN_A = 4'b0010 (0010)
main.uut_high.MOV_A_IM = 4'b0011 (0011)
main.uut_high.MOV_B_A = 4'b0100 (0100)
main.uut_high.ADD_B_IM = 4'b0101 (0101)
main.uut_high.IN_B = 4'b0110 (0110)
main.uut_high.MOV_B_IM = 4'b0111 (0111)
main.uut_high.OUT_B = 4'b1001 (1001)
main.uut_high.OUT_IM = 4'b1011 (1011)
main.uut_high.JNC_IM = 4'b1110 (1110)
main.uut_high.JMP_IM = 4'b1111 (1111)
main.uut_low.clk = 0
main.uut_low.notreset = 0
main.uut_low.insn = 1 (00000001)
main.uut_low.inp = 4'b0000 (0000)
main.uut_low.A = 4'b0000 (0000)
main.uut_low.B = 4'b0000 (0000)
main.uut_low.pc = 4'b0000 (0000)
main.uut_low.outp = 4'b0000 (0000)
main.uut_low.alu_out = 4'b0001 (0001)
main.uut_low.notload = 4'b1110 (1110)
main.uut_low.cout = 0
main.uut_low.imm = 4'b0001 (0001)
main.uut_low.sel_a = 0
main.uut_low.sel_b = 0
main.uut_low.opa = 4'b0000 (0000)
main.uut_low.opb = 4'b0001 (0001)
main.uut_low.prev_carry = 0
main.uut_low.alu.a = 4'b0000 (0000)
main.uut_low.alu.b = 4'b0001 (0001)
main.uut_low.alu.cin = 0
main.uut_low.alu.s = 4'b0001 (0001)
main.uut_low.alu.cout = 0
main.uut_low.mux1.a = 4'b0000 (0000)
main.uut_low.mux1.b = 4'b0000 (0000)
main.uut_low.mux1.sel = 2'b00 (00)
main.uut_low.mux1.y = 2'b00 (00)
main.uut_low.mux2.a = 4'b0000 (0000)
main.uut_low.mux2.b = 4'b0000 (0000)
main.uut_low.mux2.sel = 2'b00 (00)
main.uut_low.mux2.y = 2'b00 (00)
main.uut_low.cmd.notcarry = 1
main.uut_low.cmd.d = 1 (00000001)
main.uut_low.cmd.l = 4'b1110 (1110)
main.uut_low.cmd.sel_a = 0
main.uut_low.cmd.s3 = 0
main.uut_low.cmd.s6 = 1
main.uut_low.cmd.s12 = 1
main.uut_low.a_counter.abcd = 4'b0001 (0001)
main.uut_low.a_counter.enable = 0
main.uut_low.a_counter.notreset = 0
main.uut_low.a_counter.notld = 0
main.uut_low.a_counter.clk = 0
main.uut_low.a_counter.qabcd = 4'b0000 (0000)
main.uut_low.b_counter.abcd = 4'b0001 (0001)
main.uut_low.b_counter.enable = 0
main.uut_low.b_counter.notreset = 0
main.uut_low.b_counter.notld = 1
main.uut_low.b_counter.clk = 0
main.uut_low.b_counter.qabcd = 4'b0000 (0000)
main.uut_low.out_counter.abcd = 4'b0001 (0001)
main.uut_low.out_counter.enable = 0
main.uut_low.out_counter.notreset = 0
main.uut_low.out_counter.notld = 1
main.uut_low.out_counter.clk = 0
main.uut_low.out_counter.qabcd = 4'b0000 (0000)
main.uut_low.pc_counter.abcd = 4'b0001 (0001)
main.uut_low.pc_counter.enable = 1
main.uut_low.pc_counter.notreset = 0
main.uut_low.pc_counter.notld = 1
main.uut_low.pc_counter.clk = 0
main.uut_low.pc_counter.qabcd = 4'b0000 (0000)
Transition system state 1
----------------------------------------------------
main.clk = 0
main.notreset = 1
main.insn = 211 (11010011)
main.inp = 4'b0000 (0000)
main.pc = 4'b0000 (0000)
main.outp = 4'b0000 (0000)
main.A = 4'b0000 (0000)
main.B = 4'b0000 (0000)
main.pc_low = 4'b0000 (0000)
main.outp_low = 4'b0000 (0000)
main.A_low = 4'b0000 (0000)
main.B_low = 4'b0000 (0000)
main.uut_high.clk = 0
main.uut_high.notreset = 1
main.uut_high.insn = 211 (11010011)
main.uut_high.inp = 4'b0000 (0000)
main.uut_high.outp = 4'b0000 (0000)
main.uut_high.A = 4'b0000 (0000)
main.uut_high.B = 4'b0000 (0000)
main.uut_high.pc = 4'b0000 (0000)
main.uut_high.carry = 0
main.uut_high.ADD_A_IM = 4'b0000 (0000)
main.uut_high.MOV_A_B = 4'b0001 (0001)
main.uut_high.IN_A = 4'b0010 (0010)
main.uut_high.MOV_A_IM = 4'b0011 (0011)
main.uut_high.MOV_B_A = 4'b0100 (0100)
main.uut_high.ADD_B_IM = 4'b0101 (0101)
main.uut_high.IN_B = 4'b0110 (0110)
main.uut_high.MOV_B_IM = 4'b0111 (0111)
main.uut_high.OUT_B = 4'b1001 (1001)
main.uut_high.OUT_IM = 4'b1011 (1011)
main.uut_high.JNC_IM = 4'b1110 (1110)
main.uut_high.JMP_IM = 4'b1111 (1111)
main.uut_low.clk = 0
main.uut_low.notreset = 1
main.uut_low.insn = 211 (11010011)
main.uut_low.inp = 4'b0000 (0000)
main.uut_low.A = 4'b0000 (0000)
main.uut_low.B = 4'b0000 (0000)
main.uut_low.pc = 4'b0000 (0000)
main.uut_low.outp = 4'b0000 (0000)
main.uut_low.alu_out = 4'b0011 (0011)
main.uut_low.notload = 4'b0111 (0111)
main.uut_low.cout = 0
main.uut_low.imm = 4'b0011 (0011)
main.uut_low.sel_a = 1
main.uut_low.sel_b = 0
main.uut_low.opa = 4'b0000 (0000)
main.uut_low.opb = 4'b0011 (0011)
main.uut_low.prev_carry = 0
main.uut_low.alu.a = 4'b0000 (0000)
main.uut_low.alu.b = 4'b0011 (0011)
main.uut_low.alu.cin = 0
main.uut_low.alu.s = 4'b0011 (0011)
main.uut_low.alu.cout = 0
main.uut_low.mux1.a = 4'b0000 (0000)
main.uut_low.mux1.b = 4'b0000 (0000)
main.uut_low.mux1.sel = 2'b01 (01)
main.uut_low.mux1.y = 2'b00 (00)
main.uut_low.mux2.a = 4'b0000 (0000)
main.uut_low.mux2.b = 4'b0000 (0000)
main.uut_low.mux2.sel = 2'b01 (01)
main.uut_low.mux2.y = 2'b00 (00)
main.uut_low.cmd.notcarry = 1
main.uut_low.cmd.d = 211 (11010011)
main.uut_low.cmd.l = 4'b0111 (0111)
main.uut_low.cmd.sel_a = 1
main.uut_low.cmd.s3 = 1
main.uut_low.cmd.s6 = 1
main.uut_low.cmd.s12 = 0
main.uut_low.a_counter.abcd = 4'b0011 (0011)
main.uut_low.a_counter.enable = 0
main.uut_low.a_counter.notreset = 1
main.uut_low.a_counter.notld = 1
main.uut_low.a_counter.clk = 0
main.uut_low.a_counter.qabcd = 4'b0000 (0000)
main.uut_low.b_counter.abcd = 4'b0011 (0011)
main.uut_low.b_counter.enable = 0
main.uut_low.b_counter.notreset = 1
main.uut_low.b_counter.notld = 1
main.uut_low.b_counter.clk = 0
main.uut_low.b_counter.qabcd = 4'b0000 (0000)
main.uut_low.out_counter.abcd = 4'b0011 (0011)
main.uut_low.out_counter.enable = 0
main.uut_low.out_counter.notreset = 1
main.uut_low.out_counter.notld = 1
main.uut_low.out_counter.clk = 0
main.uut_low.out_counter.qabcd = 4'b0000 (0000)
main.uut_low.pc_counter.abcd = 4'b0011 (0011)
main.uut_low.pc_counter.enable = 1
main.uut_low.pc_counter.notreset = 1
main.uut_low.pc_counter.notld = 0
main.uut_low.pc_counter.clk = 0
main.uut_low.pc_counter.qabcd = 4'b0000 (0000)
Transition system state 2
----------------------------------------------------
main.clk = 0
main.notreset = 1
main.insn = 32 (00100000)
main.inp = 4'b0000 (0000)
main.pc = 4'b0001 (0001)
main.outp = 4'b0000 (0000)
main.A = 4'b0000 (0000)
main.B = 4'b0000 (0000)
main.pc_low = 4'b0011 (0011)
main.outp_low = 4'b0000 (0000)
main.A_low = 4'b0000 (0000)
main.B_low = 4'b0000 (0000)
main.uut_high.clk = 0
main.uut_high.notreset = 1
main.uut_high.insn = 32 (00100000)
main.uut_high.inp = 4'b0000 (0000)
main.uut_high.outp = 4'b0000 (0000)
main.uut_high.A = 4'b0000 (0000)
main.uut_high.B = 4'b0000 (0000)
main.uut_high.pc = 4'b0001 (0001)
main.uut_high.carry = 0
main.uut_high.ADD_A_IM = 4'b0000 (0000)
main.uut_high.MOV_A_B = 4'b0001 (0001)
main.uut_high.IN_A = 4'b0010 (0010)
main.uut_high.MOV_A_IM = 4'b0011 (0011)
main.uut_high.MOV_B_A = 4'b0100 (0100)
main.uut_high.ADD_B_IM = 4'b0101 (0101)
main.uut_high.IN_B = 4'b0110 (0110)
main.uut_high.MOV_B_IM = 4'b0111 (0111)
main.uut_high.OUT_B = 4'b1001 (1001)
main.uut_high.OUT_IM = 4'b1011 (1011)
main.uut_high.JNC_IM = 4'b1110 (1110)
main.uut_high.JMP_IM = 4'b1111 (1111)
main.uut_low.clk = 0
main.uut_low.notreset = 1
main.uut_low.insn = 32 (00100000)
main.uut_low.inp = 4'b0000 (0000)
main.uut_low.A = 4'b0000 (0000)
main.uut_low.B = 4'b0000 (0000)
main.uut_low.pc = 4'b0011 (0011)
main.uut_low.outp = 4'b0000 (0000)
main.uut_low.alu_out = 4'b0000 (0000)
main.uut_low.notload = 4'b1110 (1110)
main.uut_low.cout = 0
main.uut_low.imm = 4'b0000 (0000)
main.uut_low.sel_a = 0
main.uut_low.sel_b = 1
main.uut_low.opa = 4'b0000 (0000)
main.uut_low.opb = 4'b0000 (0000)
main.uut_low.prev_carry = 0
main.uut_low.alu.a = 4'b0000 (0000)
main.uut_low.alu.b = 4'b0000 (0000)
main.uut_low.alu.cin = 0
main.uut_low.alu.s = 4'b0000 (0000)
main.uut_low.alu.cout = 0
main.uut_low.mux1.a = 4'b0000 (0000)
main.uut_low.mux1.b = 4'b0000 (0000)
main.uut_low.mux1.sel = 2'b10 (10)
main.uut_low.mux1.y = 2'b00 (00)
main.uut_low.mux2.a = 4'b0000 (0000)
main.uut_low.mux2.b = 4'b0000 (0000)
main.uut_low.mux2.sel = 2'b10 (10)
main.uut_low.mux2.y = 2'b00 (00)
main.uut_low.cmd.notcarry = 1
main.uut_low.cmd.d = 32 (00100000)
main.uut_low.cmd.l = 4'b1110 (1110)
main.uut_low.cmd.sel_a = 0
main.uut_low.cmd.s3 = 0
main.uut_low.cmd.s6 = 1
main.uut_low.cmd.s12 = 1
main.uut_low.a_counter.abcd = 4'b0000 (0000)
main.uut_low.a_counter.enable = 0
main.uut_low.a_counter.notreset = 1
main.uut_low.a_counter.notld = 0
main.uut_low.a_counter.clk = 0
main.uut_low.a_counter.qabcd = 4'b0000 (0000)
main.uut_low.b_counter.abcd = 4'b0000 (0000)
main.uut_low.b_counter.enable = 0
main.uut_low.b_counter.notreset = 1
main.uut_low.b_counter.notld = 1
main.uut_low.b_counter.clk = 0
main.uut_low.b_counter.qabcd = 4'b0000 (0000)
main.uut_low.out_counter.abcd = 4'b0000 (0000)
main.uut_low.out_counter.enable = 0
main.uut_low.out_counter.notreset = 1
main.uut_low.out_counter.notld = 1
main.uut_low.out_counter.clk = 0
main.uut_low.out_counter.qabcd = 4'b0000 (0000)
main.uut_low.pc_counter.abcd = 4'b0000 (0000)
main.uut_low.pc_counter.enable = 1
main.uut_low.pc_counter.notreset = 1
main.uut_low.pc_counter.notld = 1
main.uut_low.pc_counter.clk = 0
main.uut_low.pc_counter.qabcd = 4'b0011 (0011)
Then at this point I was still receiving errors. I looked at the instruction in the trace and I realized / remembered that there are secret opcodes. There are only 12 named listed opcodes, but 4bits = 16. We can see here that in step 1, it picks opcode main.insn = 129 (10000001) which corresponds to opcode 1000. There are secret (possibly even useful) opcodes 1010, 1101, 1100, 1000. This is not at all uncommon on real chips to have undocumented or accidental opcodes.
Rather than figuring out what they do from the schematic, I went back an put an assumption into the ebmc testbench to disallow them
%%file /tmp/td4_tb_ebmc2.sv
`timescale 1ns/1ps
module main(
input clk,
input notreset,
input [7:0] insn,
input [3:0] inp);
wire [3:0] pc;
wire [3:0] outp;
wire [3:0] A;
wire [3:0] B;
wire [3:0] pc_low;
wire [3:0] outp_low;
wire [3:0] A_low;
wire [3:0] B_low;
// Instantiate the TD4 CPU
td4_cpu_high uut_high (
.clk(clk),
.notreset(notreset),
.insn(insn),
.inp(inp),
.pc(pc),
.A(A),
.B(B),
.outp(outp)
);
td4_cpu_low uut_low (
.clk(clk),
.notreset(notreset),
.insn(insn),
.inp(inp),
.pc(pc_low),
.A(A_low),
.B(B_low),
.outp(outp_low)
);
assert property (notreset == 0 | A_low == A);
assert property (notreset == 0 | B_low == B);
assert property (notreset == 0 | pc_low == pc);
assert property (notreset == 0 | outp_low == outp);
// 1010, 1101, 1100, 1000
assume property (insn[7:4] != 4'b1000);
assume property (insn[7:4] != 4'b1010);
assume property (insn[7:4] != 4'b1101);
assume property (insn[7:4] != 4'b1100);
endmodule
Overwriting /tmp/td4_tb_ebmc2.sv
With that, it passes the equivalence check up to a high number of bound
! ebmc /tmp/td4_high2.sv /tmp/td4_low.sv /tmp/td4_tb_ebmc2.sv --top main --reset "notreset==0" --trace --bound 100
Parsing /tmp/td4_high2.sv
Parsing /tmp/td4_low.sv
Parsing /tmp/td4_tb_ebmc2.sv
Converting
Type-checking Verilog::adder_74HC283
Type-checking Verilog::command_decoder
Type-checking Verilog::counter_74HC161
Type-checking Verilog::data_select_74HC153
Type-checking Verilog::td4_cpu_high
Type-checking Verilog::td4_cpu_low
Making td4_cpu_low.A a wire
Making td4_cpu_low.B a wire
Making td4_cpu_low.outp a wire
Making td4_cpu_low.pc a wire
Type-checking Verilog::main
Generating Decision Problem
Using MiniSAT 2.2.1 with simplifier
Properties
Solving with propositional reduction
SAT checker: instance is UNSATISFIABLE
UNSAT: No path found within bound
** Results:
[main.assert.1] always main.notreset == 0 || main.A_low == main.A: [32mPROVED up to bound 100[0m
[main.assert.2] always main.notreset == 0 || main.B_low == main.B: [32mPROVED up to bound 100[0m
[main.assert.3] always main.notreset == 0 || main.pc_low == main.pc: [32mPROVED up to bound 100[0m
[main.assert.4] always main.notreset == 0 || main.outp_low == main.outp: [32mPROVED up to bound 100[0m
[main.assume.5] always main.insn[7:4] != 4'b1000: [34mASSUMED[0m
[main.assume.6] always main.insn[7:4] != 4'b1010: [34mASSUMED[0m
[main.assume.7] always main.insn[7:4] != 4'b1101: [34mASSUMED[0m
[main.assume.8] always main.insn[7:4] != 4'b1100: [34mASSUMED[0m
Bits and Bobbles
I could try to use yosys-smtbmc / symbiyosys https://symbiyosys.readthedocs.io/en/latest/reference.html similarly. I kind of like ebmc and haven’t found a clean way to run yosys as a simple single command. This is admittedly an odd use case to want to avoid files.
There are some odd race conditions in the circuit itself which are solved by finite propagation of signals. I suspect it would be better to have a fetch cycle and then an execute cycle. Timing concerns are a mystery to me.
I was not getting the unbounded flags of ebmc to work for me. They do exists though. (bdd, k-induction, and ic3).
Errors
- I had carry logic missing in the high level interpreter
- Arguable whether a bug or feature that instructions secretly always add in the immediate
- Secret instructions opcode 1010, 1101, 1100, 1000
%%file /tmp/counter.sv
`timescale 1ns/1ps
module counter_74HC161(
input [3:0] abcd,
input notreset,
input ld,
input clk,
output reg [3:0] qabcd
);
always @(posedge clk or negedge notreset)
begin
if (!notreset)
qabcd <= 4'b0000; // Reset counter
else if (ld)
qabcd <= abcd; // Load input value
else
qabcd <= qabcd + 1; // Increment counter
end
endmodule
Overwriting /tmp/counter.sv
%%file /tmp/counter_tb.sv
`timescale 1ns/1ps
module tb_counter_74HC161;
// Declare testbench signals
reg [3:0] abcd;
reg notreset, ld, clk;
wire [3:0] qabcd;
// Instantiate the counter module
counter_74HC161 uut (
.abcd(abcd),
.notreset(notreset),
.ld(ld),
.clk(clk),
.qabcd(qabcd)
);
// Generate clock signal
always #5 clk <= ~clk; // Toggle clock every 5 ns (10 ns period, 100 MHz)
initial begin
// Console header
$display("Time\t clk notreset ld abcd qabcd");
$display("-----------------------------------");
// Monitor changes and print signals
$monitor("%0t\t %b %b %b %b %b",
$time, clk, notreset, ld, abcd, qabcd);
// Initialize signals
clk = 0;
notreset = 0;
ld = 0;
abcd = 4'b1010;
// Apply reset
#10 notreset = 1; // Release reset
#10 ld = 1; // Load value into counter
#10 ld = 0; // Start counting
// Let the counter increment for a while
#60 $finish; // End simulation
end
endmodule
Overwriting /tmp/counter_tb.sv
%%bash
iverilog -Wall -g2012 -o /tmp/tb_counter.vvp /tmp/counter_tb.sv /tmp/counter.sv
vvp /tmp/tb_counter.vvp
Time clk notreset ld abcd qabcd
-----------------------------------
0 0 0 0 1010 0000
5000 1 0 0 1010 0000
10000 0 1 0 1010 0000
15000 1 1 0 1010 0001
20000 0 1 1 1010 0001
25000 1 1 1 1010 1010
30000 0 1 0 1010 1010
35000 1 1 0 1010 1011
40000 0 1 0 1010 1011
45000 1 1 0 1010 1100
50000 0 1 0 1010 1100
55000 1 1 0 1010 1101
60000 0 1 0 1010 1101
65000 1 1 0 1010 1110
70000 0 1 0 1010 1110
75000 1 1 0 1010 1111
80000 0 1 0 1010 1111
85000 1 1 0 1010 0000
/tmp/counter_tb.sv:44: $finish called at 90000 (1ps)
90000 0 1 0 1010 0000
! verilator --lint-only /tmp/counter.sv
- V e r i l a t i o n R e p o r t: Verilator 5.027 devel rev v5.026-18-ga6d438d11
- Verilator: Built from 0.013 MB sources in 2 modules, into 0.009 MB in 4 C++ files needing 0.000 MB
- Verilator: Walltime 0.003 s (elab=0.000, cvt=0.001, bld=0.000); cpu 0.000 s on 1 threads; alloced 1.406 MB
! verilator -Wall --binary --top-module tb_counter_74HC161 --sv /tmp/counter.sv /tmp/counter_tb.sv && obj_dir/Vtb_counter_74HC161 && rm -rf obj_dir/
%Warning-DECLFILENAME: /tmp/counter.sv:4:8: Filename 'counter' does not match MODULE name: 'counter_74HC161'
4 | module counter_74HC161(
| ^~~~~~~~~~~~~~~
... For warning description see https://verilator.org/warn/DECLFILENAME?v=5.027
... Use "/* verilator lint_off DECLFILENAME */" and lint_on around source to disable this message.
%Warning-DECLFILENAME: /tmp/counter_tb.sv:4:8: Filename 'counter_tb' does not match MODULE name: 'tb_counter_74HC161'
4 | module tb_counter_74HC161;
| ^~~~~~~~~~~~~~~~~~
%Error: Exiting due to 2 warning(s)
Adder
%%file /tmp/td4.sv
`timescale 1ns/1ps
module counter_74HC161(
input [3:0] abcd,
input enable,
input notreset,
input notld,
input clk,
output reg [3:0] qabcd
);
always @(posedge clk or negedge notreset)
begin
if (!notreset)
qabcd <= 4'b0000; // Reset counter
else if (!notld)
qabcd <= abcd; // Load input value
else if (enable)
qabcd <= qabcd + 1; // Increment counter
else
qabcd <= qabcd; // Hold counter
end
endmodule
module adder_74HC283(
input [3:0] a,
input [3:0] b,
input cin,
output [3:0] s,
output cout
);
assign {cout, s} = a + b + cin;
endmodule
module data_select_74HC153(
input [3:0] a,
input [3:0] b,
input [1:0] sel,
output [1:0] y
);
assign y[0] = a[sel];
assign y[1] = b[sel];
endmodule
module address_decode_74HC154(
input [3:0] a,
output [15:0] y
);
assign y = 1 << a;
endmodule
module command_decoder(
input carry,
input [7:0] d,
output [3:0] l,
output sel_a
);
// It is unlikely I got this right.
wire s3 = d[4] | d[7];
wire s6 = d[4] | carry;
wire s12 = !d[6];
assign l[0] = d[7] | d[6];
assign l[1] = s12 | d[7];
assign l[2] = !(d[7] & s12);
assign l[3] = !(s6 & d[7] & d[6]);
assign sel_a = s3;
endmodule
module td4_cpu(
input clk,
input notreset, // reset signal
input [7:0] insn, // instruction
input [3:0] inp, // input switches
output reg [3:0] A,
output reg [3:0] B,
output reg [3:0] pc,
output reg [3:0] outp
);
wire [3:0] alu_out;
wire [3:0] notload;
wire cout;
wire [3:0] imm; // immediate data
wire sel_a;
wire sel_b = insn[5];
wire [3:0] opa;
wire [3:0] opb = insn[3:0];
//always @(posedge clk) begin
//$display("alu_out %b notload %b opa %b opb %b",
// alu_out, notload, opa, opb);
//end
assign imm = insn[3:0];
adder_74HC283 alu(
.a(opa),
.b(opb),
.cin(1'b0),
.s(alu_out),
.cout(cout)
);
data_select_74HC153 mux1(
.a({1'b0, inp[0], B[0], A[0]}),
.b({1'b0, inp[1], B[1], A[1]}),
.sel({sel_b, sel_a}),
.y(opa[1:0])
);
data_select_74HC153 mux2(
.a({1'b0, inp[2], B[2], A[2]}),
.b({1'b0, inp[3], B[3], A[3]}),
.sel({sel_b, sel_a}),
.y(opa[3:2])
);
reg prev_carry;
always @(posedge clk or negedge notreset)
begin
if (!notreset)
prev_carry <= 1'b0;
else
prev_carry <= cout;
end
command_decoder cmd(
.carry(prev_carry),
.d(insn),
.l(notload),
.sel_a(sel_a)
);
counter_74HC161 a_counter(
.abcd(alu_out),
.notreset(notreset),
.enable(1'b0),
.notld(notload[0]),
.clk(clk),
.qabcd(A)
);
counter_74HC161 b_counter(
.abcd(alu_out),
.notreset(notreset),
.enable(1'b0),
.notld(notload[1]),
.clk(clk),
.qabcd(B)
);
counter_74HC161 out_counter(
.abcd(alu_out),
.notreset(notreset),
.enable(1'b0),
.notld(notload[2]),
.clk(clk),
.qabcd(outp)
);
counter_74HC161 pc_counter(
.abcd(alu_out),
.notreset(notreset),
.enable(1'b1),
.notld(notload[3]),
.clk(clk),
.qabcd(pc)
);
endmodule
Overwriting /tmp/td4.sv
! iverilog -Wall -g2012 -o /tmp/td4.vvp /tmp/td4_tb.sv /tmp/td4.sv && vvp /tmp/td4.vvp
Time PC A B OUTP INSN INP
0 0000 0000 0000 0000 00000000 0000
alu_out xxxx notload 1110
Loading immediate value into register A
20000 0000 0000 0000 0000 00111011 0000
alu_out xxxx notload 1110
30000 0001 xxxx 0000 0000 00111011 0000
Test complete.
/tmp/td4_tb.sv:68: $finish called at 40000 (1ps)
%%file /tmp/td4_tb.sv
`timescale 1ns/1ps
module tb_td4_cpu;
// Instruction opcodes
parameter ADD_A_IM = 4'b0000, MOV_A_B = 4'b0001, IN_A = 4'b0010, MOV_A_IM = 4'b0011;
parameter MOV_B_A = 4'b0100, ADD_B_IM = 4'b0101, IN_B = 4'b0110, MOV_B_IM = 4'b0111;
parameter OUT_B = 4'b1001, OUT_IM = 4'b1011, JNC_IM = 4'b1110, JMP_IM = 4'b1111;
reg clk;
reg notreset;
reg [7:0] insn;
reg [3:0] inp;
wire [3:0] pc;
wire [3:0] outp;
wire [3:0] A;
wire [3:0] B;
// Instantiate the TD4 CPU
td4_cpu uut (
.clk(clk),
.notreset(notreset),
.insn(insn),
.inp(inp),
.pc(pc),
.A(A),
.B(B),
.outp(outp)
);
always #10 clk = ~clk;
initial begin
$display("Time\t PC A B OUTP INSN INP");
$monitor("%0t\t %b %b %b %b %b %b", $time, pc, A, B, outp, insn, inp);
// Initialize signals
clk = 0;
notreset = 0; // Apply reset
insn = 8'b00000000; // No-op
inp = 4'b0000;
#20 notreset = 1; // Release reset
$display("Loading immediate value into register A");
insn = {MOV_A_IM, 4'b1011};
#20;
assert(A === 4'b1011);
$display("Loading immediate value into register B");
insn = {MOV_B_IM, 4'b1010};
#20;
assert(B === 4'b1010);
$display("A = A + 1");
insn = {ADD_A_IM , 4'b0001}; // ADD A = A + B
#20;
assert(A === 4'b1011 + 4'b0001);
#20
assert(A == 4'b1011 + 4'b0010);
$display("JMP 0010");
insn = {JMP_IM, 4'b0010};
#10;
#10;
assert(pc === 4'b0010);
$display("out B");
insn = {OUT_B, 4'b0000};
#20;
assert(outp === B);
/*
$display("Loading immediate value into register B");
insn = 8'b00011010; // Load B with 0b1010
#20;
$display("Outputting the result");
insn = 8'b01000000; // Move A to OUT
#20;
// Increment PC
insn = 8'b01100000; // INC PC
#20;
*/
$display("Test complete.");
$finish;
end
endmodule
Overwriting /tmp/td4_tb.sv
! iverilog -Wall -g2012 -o /tmp/td4.vvp /tmp/td4_tb.sv /tmp/td4.sv && vvp /tmp/td4.vvp
Time PC A B OUTP INSN INP
0 0000 0000 0000 0000 00000000 0000
Loading immediate value into register A
20000 0000 0000 0000 0000 00111011 0000
30000 0001 xxxx 0000 0000 00111011 0000
Test complete.
/tmp/td4_tb.sv:68: $finish called at 40000 (1ps)
%%file /tmp/td4_tb.sv
`timescale 1ns/1ps
module tb_td4_cpu;
// Instruction opcodes
parameter ADD_A_IM = 4'b0000, MOV_A_B = 4'b0001, IN_A = 4'b0010, MOV_A_IM = 4'b0011;
parameter MOV_B_A = 4'b0100, ADD_B_IM = 4'b0101, IN_B = 4'b0110, MOV_B_IM = 4'b0111;
parameter OUT_B = 4'b1001, OUT_IM = 4'b1011, JNC_IM = 4'b1110, JMP_IM = 4'b1111;
reg clk;
reg notreset;
reg [7:0] insn;
reg [7:0] prog [0:15];
reg [3:0] inp;
wire [3:0] pc;
wire [3:0] outp;
wire [3:0] A;
wire [3:0] B;
assign insn = prog[pc];
initial begin
prog[0] = {ADD_B_IM, 4'b0001}; // ADD B 1
prog[1] = {OUT_B, 4'b0000}; // OUT B
prog[2] = {JMP_IM, 4'b0000}; // JMP 0
end
// Instantiate the TD4 CPU
td4_cpu uut (
.clk(clk),
.notreset(notreset),
.insn(insn),
.inp(inp),
.pc(pc),
.A(A),
.B(B),
.outp(outp)
);
always #10 clk = ~clk;
initial begin
$display("Time\t PC A B OUTP INSN INP");
$monitor("%0t\t %b %b %b %b %b %b", $time, pc, A, B, outp, insn, inp);
clk = 0;
notreset = 0; // Apply reset
inp = 4'b0000;
#20 notreset = 1; // Release reset
#200 $finish;
end
endmodule
Overwriting /tmp/td4_tb.sv
! iverilog -Wall -g2012 -o /tmp/td4.vvp /tmp/td4_tb.sv /tmp/td4.sv && vvp /tmp/td4.vvp
Time PC A B OUTP INSN INP
0 0000 0000 0000 0000 01010001 0000
30000 0001 0000 0001 0000 10010000 0000
50000 0010 0000 0001 0001 11110000 0000
70000 0000 0000 0001 0001 01010001 0000
90000 0001 0000 0010 0001 10010000 0000
110000 0010 0000 0010 0010 11110000 0000
130000 0000 0000 0010 0010 01010001 0000
150000 0001 0000 0011 0010 10010000 0000
170000 0010 0000 0011 0011 11110000 0000
190000 0000 0000 0011 0011 01010001 0000
210000 0001 0000 0100 0011 10010000 0000
/tmp/td4_tb.sv:55: $finish called at 220000 (1ps)
Overwriting /tmp/td4_high.sv
! iverilog -Wall -g2012 -o /tmp/td4.vvp /tmp/td4_tb.sv /tmp/td4_high.sv && vvp /tmp/td4.vvp
/tmp/td4_high.sv:1: warning: timescale for td4_cpu inherited from another file.
/tmp/td4_tb.sv:2: ...: The inherited timescale is here.
/tmp/td4_high.sv:27: error: Could not find variable ``a'' in ``tb_td4_cpu.uut''
/tmp/td4_high.sv:27: error: Unable to bind wire/reg/memory `a' in `tb_td4_cpu.uut'
2 error(s) during elaboration.
%%file /tmp/compare_tb.sv
module compare_tb;
reg insn;
reg clk;
reg notreset;
reg [7:0] insn;
reg [3:0] inp1, inp2;
wire [3:0] pc1, pc2;
wire [3:0] outp1, outp2;
wire [3:0] A1, A1;
wire [3:0] B1, A1;
// Instantiate the TD4 CPU
td4_cpu uut (
.clk(clk),
.notreset(notreset),
.insn(insn),
.inp(inp1),
.pc(pc1),
.A(A1),
.B(B1),
.outp(outp1)
);
td4_cpu_high uut (
.clk(clk),
.notreset(notreset),
.insn(insn),
.inp(inp),
.pc(pc2),
.A(A2),
.B(B2),
.outp(outp2)
);
initial begin
end
endmodule
Problems I had:
- The schematic was wrong in the decoder logic
- least and most signifcant bit confusion
- I forgot to wire the immediate into the adder
- notload and notreset vs load and reset
Using EBMC
Download here and install https://github.com/diffblue/hw-cbmc/releases Oh a wasm build, that’s nice
%%file /tmp/counter.sv
module main(input clk, x, y);
reg [1:0] cnt1;
reg z;
initial cnt1=0;
initial z=0;
always @(posedge clk) cnt1=cnt1+1;
always @(posedge clk)
casex (cnt1)
2'b00:;
2'b01:;
2'b1?: z=1;
endcase
p1: assert property (@(posedge clk) (z==0));
endmodule
Writing /tmp/counter.sv
! ebmc --top main --bound 3 /tmp/counter.sv
Parsing /tmp/counter.sv
Converting
Type-checking Verilog::main
Generating Decision Problem
Using MiniSAT 2.2.1 with simplifier
Properties
Solving with propositional reduction
SAT checker: instance is SATISFIABLE
SAT: path found
SAT checker inconsistent: instance is UNSATISFIABLE
UNSAT: No path found within bound
** Results:
[main.p1] always main.z == 0: [91mREFUTED[0m
! yosys -p "read_verilog -sv /tmp/counter.sv; prep -top main; write_smt2 -wires -mem -bv /tmp/counter.smt2" && yosys-smtbmc -s z3 /tmp/main.smt2
/----------------------------------------------------------------------------\
| yosys -- Yosys Open SYnthesis Suite |
| Copyright (C) 2012 - 2024 Claire Xenia Wolf <claire@yosyshq.com> |
| Distributed under an ISC-like license, type "license" to see terms |
\----------------------------------------------------------------------------/
Yosys 0.42+40 (git sha1 a739e21a5, clang++ 14.0.0-1ubuntu1.1 -fPIC -Os)
-- Running command `read_verilog -sv /tmp/counter.sv; prep -top main; write_smt2 -wires -mem -bv /tmp/counter.smt2' --
1. Executing Verilog-2005 frontend: /tmp/counter.sv
Parsing SystemVerilog input from `/tmp/counter.sv' to AST representation.
/tmp/counter.sv:19: ERROR: syntax error, unexpected '@'
%%file /tmp/add.v
// https://www.cprover.org/ebmc/manual/tutorial/
module my_add(input a, b, output [1:0] y);
assign y[0]=a^b;
assign y[1]=a&b;
endmodule
module main(input a, b);
wire [1:0] result;
my_add adder(a, b, result);
assert final (2'(a)+b==result);
endmodule
Overwriting /tmp/add.v
! ebmc --top main /tmp/add.v
Parsing /tmp/add.v
file /tmp/add.v line 15: syntax error before 'final'
Bits and Bobbles
https://www.youtube.com/watch?v=H3tsP9tjYdY&ab_channel=FOSSiFoundation Introduction to Formal Verification with Symbiotic EDA Open Source Tools https://www.youtube.com/watch?v=cxPLuzOMm8g&ab_channel=PsychogenicTechnologies The Hidden Power of Formal Methods in Hardware Design: Crash Course
from collections import namedtuple
class TaggedUnion():
def __init__(self, name, cases):
self.name = name
self.constructors = []
for name, args in cases:
cons = namedtuple(name, args)
self.constructors.append(cons)
setattr(self, name, lambda self, *args, **kwargs: cons(*args, **kwargs))
setattr(self, "is_" + name, lambda x: isinstance(x, cons))
for fname in args:
setattr(self, fname, lambda x: getattr(x, fname))
def num_constructors(self):
return len(self.constructors)
def constructor(self, idx):
return self.constructors[idx]
AExpr = TaggedUnion("AExpr", [
("Int", ["value"]),
("Add", ["lhs", "rhs"]),
])
AExpr.Int(1,2,4)
Add(lhs=2, rhs=4)
from collections import namedtuple
from enum import Enum
Op = Enum("Op", "ADD MOV IN OUT JNC JMP")
Op = Enum("Op", "ADD_A ADD_B MOV_AB MOV_BA IN_A IN_B OUT_B OUT JNC JMP")
Insn = namedtuple("Insn", "op im")
State = namedtuple("State", "a, b, out, pc, c, inp, program")
def step(state):
a, b, out, pc, c, inp, program = state
insn = program[pc]
im = insn.im
match insn.op:
case Op.ADD_A:
im_int = int(im)
assert 0 <= im_int < 16
a_tmp = a+im_int
return State(a_tmp%16, b, out, (pc+1)%16, a_tmp>=16, inp, program)
case Op.MOV_A_B:
return State._replace(pc = (pc+1)%16, )(b, b, out, (pc+1)%16, False, inp, program)
case "IN", "A", None:
return State(inp, b, out, (pc+1)%16, False, inp, program)
case "MOV", "A", im:
im_int = int(im)
assert 0 <= im_int < 16
return State(im_int, b, out, (pc+1)%16, False, inp, program)
case "MOV", "B", "A":
return State(a, a, out, (pc+1)%16, False, inp, program)
case "ADD", "B", im:
im_int = int(im)
assert 0 <= im_int < 16
b_tmp = b+im_int
return State(a, b_tmp%16, out, (pc+1)%16, b_tmp>=16, inp, program)
case "IN", "B", None:
return State(a, inp, out, (pc+1)%16, False, inp, program)
case "MOV", "B", im:
im_int = int(im)
assert 0 <= im_int < 16
return State(a, im_int, out, (pc+1)%16, False, inp, program)
case "OUT", "B", None:
print(b)
return State(a, b, b, (pc+1)%16, False, inp, program)
case "OUT", im, None:
im_int = int(im)
assert 0 <= im_int < 16
print(im_int)
return State(a, b, im_int, (pc+1)%16, False, inp, program)
case "JNC", im, None:
im_int = int(im)
assert 0 <= im_int < 16
return State(a, b, out, im_int if not c else (pc+1)%16, False, inp, program)
case "JMP", im, None:
im_int = int(im)
assert 0 <= im_int < 16
return State(a, b, out, im_int, False, inp, program)
case _:
raise Exception("Unrecognized command")
Bits and Bobbles
%%file /tmp/td4.v
module TD4 (
input clk,
input rst,
input [7:0] dip_switch [16],
input [3:0] in_dip_switch,
output reg [3:0] out_led,
output reg [3:0] A, // Added output for register A
output reg [3:0] B, // Added output for register B
output reg [3:0] PC, // Added output for program counter
output reg carry // Added output for carry flag
);
// Instruction opcodes
parameter ADD_A_IM = 4'b0000, MOV_A_B = 4'b0001, IN_A = 4'b0010, MOV_A_IM = 4'b0011;
parameter MOV_B_A = 4'b0100, ADD_B_IM = 4'b0101, IN_B = 4'b0110, MOV_B_IM = 4'b0111;
parameter OUT_B = 4'b1001, OUT_IM = 4'b1011, JNC_IM = 4'b1110, JMP_IM = 4'b1111;
// Main CPU cycle
always @(posedge clk or posedge rst) begin
if (rst) {A, B, PC, carry, out_led} <= 0;
else begin
// Data
case (dip_switch[PC][7:4])
ADD_A_IM: {carry, A} <= A + dip_switch[PC][3:0];
MOV_A_B: A <= B;
IN_A, MOV_A_IM: A <= dip_switch;
MOV_B_A: B <= A;
ADD_B_IM: {carry, B} <= B + dip_switch[PC][3:0];
IN_B, MOV_B_IM: B <= dip_switch[PC][3:0];
OUT_B: out_led <= B;
OUT_IM: out_led <= dip_switch;
endcase
// Control
case (dip_switch[PC][7:4])
JNC_IM: PC <= !carry ? dip_switch : PC + 1;
JMP_IM: PC <= dip_switch;
default: PC <= PC + 1;
endcase
end
end
endmodule
Writing /tmp/td4.v
%%file /tmp/tb.v
module td4_tb;
reg clk, rst;
reg [3:0] dip_switch;
wire [3:0] out_led;
wire [3:0] A, B, PC;
wire carry;
// Instantiate the TD4 CPU with new outputs for A, B, PC, and carry
TD4 td4 (
.clk(clk), .rst(rst), .dip_switch(dip_switch),
.out_led(out_led), .A(A), .B(B), .PC(PC), .carry(carry)
);
// Clock generation
always #5 clk = ~clk; // 10ns period (100MHz)
initial begin
// Initialize signals
clk = 0;
rst = 1;
dip_switch = 4'b0000;
// Release reset after some delay
#20 rst = 0;
// Test a simple sequence of instructions
#10 dip_switch = 4'b0000; // ADD A, Im
#10 dip_switch = 4'b0001; // MOV A, B
#10 dip_switch = 4'b1001; // OUT B
#10 dip_switch = 4'b1111; // JMP 0
#10 dip_switch = 4'b0000; // Set dip_switch to zero for testing
// Run simulation for some cycles
#1000 $finish;
end
// Monitor outputs
initial begin
$monitor("Time=%0t | clk=%b | rst=%b | dip_switch=%b | out_led=%b | A=%b | B=%b | PC=%b | carry=%b",
$time, clk, rst, dip_switch, out_led, A, B, PC, carry);
end
endmodule
Writing /tmp/tb.v
! iverilog -o /tmp/tb /tmp/td4.v /tmp/tb.v && vvp /tmp/tb
/tmp/td4.v:4: warning: Use of SystemVerilog [size] dimension. Use at least -g2005-sv to remove this warning.
/tmp/td4.v:26: error: Array dip_switch needs an array index here.
/tmp/td4.v:26: error: Array dip_switch needs an array index here.
/tmp/td4.v:31: error: Array dip_switch needs an array index here.
/tmp/td4.v:35: error: Array dip_switch needs an array index here.
/tmp/td4.v:36: error: Array dip_switch needs an array index here.
/tmp/td4.v:4: error: Ports cannot be unpacked arrays. Try enabling SystemVerilog support.
6 error(s) during elaboration.