使用 EBMC 比较两个 Verilog CPU 实现

大约一年前，作者和朋友用阿里巴巴的套件制作了一个 4 位 CPU[https://www.philipzucker.com/...]，非常有趣，作者认为该系统简单，适合用形式化方法进行修补。

数字设计领域围绕 VHDL 和 Verilog 展开，程序员看到 Verilog 时可能会混淆，它既是一种网络列表/电路描述语言，用于描述子部件的连接和方式，也是一种用于描述数字系统行为的编程语言，用于电路仿真。

可以在 Colab 上跟随[https://colab.research.google...]进行操作。

高电平 CPU 解释器

TD4 设计中，指令的 4 位高字节是操作码，如MOV_A_B等。基于当前指令可切换到下一个 CPU 状态，可以用一种直接的风格为 CPU 编写解释器。这里有一个由 ChatGPT 从作者的 Python 模型翻译的 CPU 代码[https://chatgpt.com/share/67a...]，经过几次迭代和调整。Google 搜索发现case语句可能存在一些问题。

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

芯片级 CPU 模型

还可以编写更低级的公式，根据原理图逐个芯片建模并互连。计算机的基本结构包括 4 个 4 位寄存器 A、B、Out、PC 等，通过计数器电路实现，还有多路选择器等。这里给出了各个芯片的 Verilog 代码，如计数器、加法器、数据选择器、命令解码器等。

%%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
);