`default_nettype none

module cpu
  (
    nrst,
    clk,
    nmi,
    irq,
    o_led,
    o_state);

`include "parameters.vh"

    localparam STATE_START_1 = 4'hc;
    localparam STATE_START_2 = 4'hd;
    localparam STATE_START_3 = 4'he;
    localparam STATE_START_4 = 4'hf;
    localparam STATE_START_0 = 4'hb;
    localparam STATE_FETCH = 0;
    localparam STATE_EXECUTE = 1;
    localparam STATE_EXECUTE_ZPX = 2;
    localparam STATE_EXECUTE_ZP = 3;
    localparam STATE_FETCH_DATA_2 = 4;
    localparam STATE_EXECUTE_DATA_2 = 5;
    localparam STATE_BRANCH = 7;

localparam
          READ_SOURCE_NONE = 2'h0,
          READ_SOURCE_MEM = 2'h1,
          READ_SOURCE_ALU = 2'h2;

    input wire nrst;
    input wire clk;
    input wire nmi;
    input wire irq;
    output wire [5:0] o_led;
    output wire [31:0] o_state;


    reg [7:0]  X;
    reg [7:0]  Y;
    reg [7:0]  A;
    reg [15:0] PC;
    reg [7:0]  S;
    reg [7:0]  P;

    reg [7:0]  tmp;

    reg [3:0]  state;

    reg [7:0]  instr;

    wire [4:0] address_code;
    wire [7:0] decoded_instr;

    wire       rst = !nrst;

    logic      mem_wr;
    wire [7:0] mem_data;
    wire [15:0] mem_addr_eff;
    logic [7:0] mem_data_wr;
    logic [2:0] mem_sel;
    logic [7:0] mem_aux_addr;
    logic [7:0] mem_aux_addr_lo;
    logic [7:0] mem_aux_addr_hi;

    logic [7:0]  alu_op_1;
    logic [7:0]  alu_op_2;
    logic        alu_op_c;
    logic [2:0]  alu_op_sel;
    wire [7:0]   alu_op_result;
    logic        alu_n;
    logic        alu_z;
    logic        alu_v;
    logic        alu_c;
    reg [7:0]    data;
    reg [15:0]   mem_addr;
    reg [2:0]    mem_addr_offset;
    logic [1:0]  pending_a_read;
    logic [1:0]  pending_x_read;
    logic [1:0]  pending_y_read;
    logic        pending_rel_branch;
    wire         is_arith;

initial A = 0;
initial X = 0;
initial Y = 0;
initial P = 0;
initial S = 8'hff;
initial mem_data_wr = 0;
initial mem_wr = 0;
assign mem_addr_eff = mem_addr;
initial pending_a_read = 0;
initial pending_x_read = 0;
initial pending_y_read = 0;
initial pending_rel_branch = 0;
initial mem_aux_addr = 0;

assign o_state[3:0] = state;
assign o_state[31:24] = A;
assign o_state[23:16] = X;

assign is_arith = (decoded_instr == I_ADC);

alu alui(
         .A(alu_op_1),
         .B(alu_op_2),
         .C(alu_op_c),
         .sel(alu_op_sel),
         .result(alu_op_result),
         .r_n(alu_n),
         .r_z(alu_z),
         .r_v(alu_v),
         .r_c(alu_c));

decoder decoder (
                 .clk(clk),
                 .rst(rst),
                 .instr((state == STATE_EXECUTE ? mem_data : instr)),
                 .address_code(address_code),
                 .decoded(decoded_instr)
                 );

mio mioi(.clk(clk),
         .i_data(mem_data_wr),
         .i_addr(mem_addr_eff),
         .i_wr(mem_wr),
         .o_data(mem_data),
         .o_led(o_led));

dmux dmuxi(
           .sel(mem_sel),
           .i_pc(PC),
           .i_a(A),
           .i_x(X),
           .i_y(Y),
           .i_sp(S),
           .i_aux({mem_aux_addr_hi, mem_aux_addr_lo}),
           .o_mux(mem_addr));

initial state = STATE_FETCH;
initial PC = 0;
initial mem_sel = 0;

always_comb
  begin
      mem_aux_addr_lo = mem_aux_addr;
      mem_aux_addr_hi = 0;
      if (address_code == ADDR_MODE_ABSOLUTE)
        begin
            mem_aux_addr_hi = mem_data;
        end
      else if (address_code == ADDR_MODE_ZP)
        begin
            mem_aux_addr_lo = mem_data;
        end
      else if (address_code == ADDR_MODE_INDEXED_ZP)
        begin
            mem_aux_addr_lo = mem_aux_addr;
        end
  end

always_comb
  begin
      alu_op_1 = 0;
      alu_op_2 = 0;
      alu_op_c = 0;
      alu_op_sel = 0;
      if (decoded_instr == I_DEX)
        begin
            alu_op_1 = X;
            alu_op_2 = 1'b1;
            alu_op_c = 1'b1;
            alu_op_sel = OP_SUB;
        end
      else if (decoded_instr == I_DEY)
        begin
            alu_op_1 = Y;
            alu_op_2 = 1'b1;
            alu_op_c = 1'b1;
            alu_op_sel = OP_SUB;
        end
      else if (address_code == ADDR_MODE_IMMEDIATE ||
               address_code == ADDR_MODE_ABSOLUTE ||
               address_code == ADDR_MODE_ZP ||
               address_code == ADDR_MODE_INDEXED_ZP)
        begin
            alu_op_1 = A;
            alu_op_2 = mem_data;
            if (decoded_instr == I_EOR)
              begin
                  alu_op_c = 0;
                  alu_op_sel = OP_EOR;
              end
            else if (decoded_instr == I_AND)
              begin
                  alu_op_c = 0;
                  alu_op_sel = OP_AND;
              end
            else if (decoded_instr == I_ORA)
              begin
                  alu_op_c = 0;
                  alu_op_sel = OP_OR;
              end
            else if (decoded_instr == I_ADC)
              begin
                  alu_op_c = P[P_C];
                  alu_op_sel = OP_ADC;
              end
        end
  end

always @(posedge clk)
  if (state == STATE_FETCH)
    begin
        if (pending_a_read == READ_SOURCE_MEM)
          begin
              A <= mem_data;
              P[P_Z] <= (mem_data == 0);
              P[P_N] <= mem_data[7];
          end
        else if (pending_a_read == READ_SOURCE_ALU)
          begin
              A <= alu_op_result;
              P[P_Z] <= alu_z;
              P[P_N] <= alu_n;
              if (is_arith)
                begin
                    P[P_C] <= alu_c;
                    P[P_V] <= alu_v;
                end
          end
        pending_a_read <= READ_SOURCE_NONE;

        if (pending_x_read == READ_SOURCE_MEM)
          begin
              X <= mem_data;
              P[P_Z] <= (mem_data == 0);
              P[P_N] <= mem_data[7];
          end
        else if (pending_x_read == READ_SOURCE_ALU)
          begin
              X <= alu_op_result;
              P[P_Z] <= alu_z;
              P[P_N] <= alu_n;
          end
        pending_x_read <= READ_SOURCE_NONE;

        if (pending_y_read == READ_SOURCE_MEM)
          begin
              Y <= mem_data;
              P[P_Z] <= (mem_data == 0);
              P[P_N] <= mem_data[7];
          end
        else if (pending_y_read == READ_SOURCE_ALU)
          begin
              Y <= alu_op_result;
              P[P_Z] <= alu_z;
              P[P_N] <= alu_n;
          end
        pending_y_read <= READ_SOURCE_NONE;

        PC <= PC + 1;
        state <= STATE_EXECUTE;
    end
  else if (state == STATE_EXECUTE)
    begin
        instr <= mem_data;
        if (address_code == ADDR_MODE_ABSOLUTE)
          begin
              PC <= PC + 1;
              state <= STATE_FETCH_DATA_2;
          end
        else if (address_code == ADDR_MODE_IMMEDIATE)
          begin
              if (decoded_instr == I_LDX)
                begin
                    pending_x_read <= READ_SOURCE_MEM;
                end
              else if (decoded_instr == I_LDA)
                begin
                    pending_a_read <= READ_SOURCE_MEM;
                end
              else if (decoded_instr == I_EOR ||
                       decoded_instr == I_AND ||
                       decoded_instr == I_ORA ||
                       decoded_instr == I_ADC)
                begin
                    pending_a_read <= READ_SOURCE_ALU;
                end

              state <= STATE_FETCH;
              PC <= PC + 1;
          end
        else if (address_code == ADDR_MODE_ZP)
          begin
              mem_sel <= DMUX_AUX;
              state <= STATE_EXECUTE_ZP;
              PC <= PC + 1;
          end
        else if (address_code == ADDR_MODE_INDEXED_ZP)
          begin
              mem_sel <= DMUX_AUX;
              state <= STATE_EXECUTE_ZPX;
              PC <= PC + 1;
          end
        else if (address_code == ADDR_MODE_IMPLIED)
          begin
              if (decoded_instr == I_DEX)
                begin
                    pending_x_read <= READ_SOURCE_ALU;
                    state <= STATE_FETCH;
                end
              else if (decoded_instr == I_DEY)
                begin
                    pending_y_read <= READ_SOURCE_ALU;
                    state <= STATE_FETCH;
                end
          end
        else if (decoded_instr == I_BNE)
          begin
              if(!P[P_Z])
                begin
                    pending_rel_branch = 1'b1;
                    state <= STATE_BRANCH;
                end
              else
                begin
                    state <= STATE_FETCH;
                    PC <= PC + 1;
                end
          end
    end
  else if (state == STATE_EXECUTE_ZPX)
    begin
        mem_aux_addr <= mem_data + X;
        state <= STATE_EXECUTE_ZP;
    end
  else if (state == STATE_EXECUTE_ZP)
    begin
        if (address_code == ADDR_MODE_ZP)
          begin
              mem_aux_addr <= mem_data;
          end
        mem_sel <= DMUX_PC;
        pending_a_read <= READ_SOURCE_ALU;

        state <= STATE_FETCH;
    end
  else if (state == STATE_BRANCH)
    begin
        if (pending_rel_branch)
          begin
              PC <= PC + {{8{mem_data[7]}}, mem_data[7:0]} + 1'b1;
          end
        pending_rel_branch <= 0;
        state <= STATE_FETCH;
    end
  else if (state == STATE_FETCH_DATA_2)
    begin
        if (address_code == ADDR_MODE_ABSOLUTE)
          begin
              mem_aux_addr[7:0] <= mem_data;
              mem_sel <= DMUX_AUX;

              state <= STATE_EXECUTE_DATA_2;
              PC <= PC + 1'b1;
          end
    end
    else if (state == STATE_EXECUTE_DATA_2)
        begin
            if (address_code == ADDR_MODE_ABSOLUTE)
              begin
                  mem_sel <= DMUX_PC;
                  state <= STATE_FETCH;
                  if (decoded_instr == I_EOR ||
                      decoded_instr == I_AND ||
                      decoded_instr == I_ORA ||
                      decoded_instr == I_ADC)
                    begin
                        pending_a_read <= READ_SOURCE_ALU;
                    end
                  else if(decoded_instr == I_JMP)
                    begin
                        PC <= mem_addr;
                    end
              end
        end

always_comb
  begin
      mem_data_wr = 0;
      mem_wr = 0;
      if (state == STATE_EXECUTE_DATA_2)
        begin
            if (address_code == ADDR_MODE_ABSOLUTE)
              begin
                  if(decoded_instr == I_STA)
                    begin
                        mem_data_wr = A;
                        mem_wr = 1'b1;
                    end
              end
        end
      else if (state == STATE_EXECUTE_ZP)
        begin
            if(decoded_instr == I_STA)
              begin
                  mem_data_wr = A;
                  mem_wr = 1'b1;
              end
        end
  end

`ifdef FORMAL

    logic f_past_valid;
    logic f2_past_valid;
    logic f3_past_valid;
    logic f4_past_valid;
    logic f5_past_valid;

initial f_past_valid = 0;
initial f2_past_valid = 0;
initial f3_past_valid = 0;
initial f4_past_valid = 0;
initial f5_past_valid = 0;
always @(posedge clk)
  f_past_valid <= 1;

always @(posedge clk)
    if (f_past_valid)
      f2_past_valid <= 1;

always @(posedge clk)
    if (f2_past_valid)
      f3_past_valid <= 1;

always @(posedge clk)
    if (f3_past_valid)
      f4_past_valid <= 1;

always @(posedge clk)
    if (f4_past_valid)
      f5_past_valid <= 1;

always @(posedge clk)
  if (f2_past_valid && state == STATE_EXECUTE)
    if ($past(decoded_instr) == I_DEX)
      begin
          assert(X == $past(X, 3) - 8'd1);
          assert($past(PC) == $past(PC, 3) + 16'd1);
          assert(P[P_Z] == (X == 0));
          assert(P[P_N] == (X[7] == 1));
          assert($stable(P[P_C]));
          assert($stable(P[P_V]));
          assert($stable(P[P_B]));
          assert($stable(P[P_D]));
          assert($stable(P[P_I]));
      end

always @(posedge clk)
  if (f2_past_valid && state == STATE_EXECUTE)
    if ($past(decoded_instr) == I_DEY)
      begin
          assert(Y == $past(Y, 3) - 8'd1);
          assert($past(PC) == $past(PC, 3) + 16'd1);
          assert(P[P_Z] == (Y == 0));
          assert(P[P_N] == (Y[7] == 1));
          assert($stable(P[P_C]));
          assert($stable(P[P_V]));
          assert($stable(P[P_B]));
          assert($stable(P[P_D]));
          assert($stable(P[P_I]));
      end

always @(posedge clk)
  if (f2_past_valid && state == STATE_EXECUTE)
    if ($past(decoded_instr) == I_LDX && $past(address_code) == ADDR_MODE_IMMEDIATE)
      begin
          assert(X == $past(mem_data));
          assert(P[P_Z] == (X == 0));
          assert(P[P_N] == (X[7] == 1));
          if (f3_past_valid)
            begin
                assert($past(PC) == $past(PC, 3) + 16'd2);
            end
      end

always @(posedge clk)
  if (f2_past_valid && state == STATE_EXECUTE)
    if ($past(decoded_instr) == I_LDA && $past(address_code) == ADDR_MODE_IMMEDIATE)
      begin
          assert(A == $past(mem_data));
          assert(P[P_Z] == (A == 0));
          assert(P[P_N] == (A[7] == 1));
          if (f3_past_valid)
            begin
                assert($past(PC) == $past(PC, 3) + 16'd2);
            end
      end

    logic [15:0] f_abs_address;

initial f_abs_address = 0;
always_comb
  begin
      f_abs_address = 0;
      if (f_past_valid)
        begin
            f_abs_address[15:8] = mem_data;
            f_abs_address[7:0] = mem_aux_addr;
        end
  end

always @(posedge clk)
  if (f2_past_valid && state == STATE_EXECUTE_DATA_2)
    if ($past(decoded_instr) == I_STA && $past(address_code) == ADDR_MODE_ABSOLUTE)
      begin
          assert(mem_wr == 1'b1);
          assert(mem_data_wr == A);
          assert(f_abs_address == mem_addr_eff);
          if (f3_past_valid)
            begin
                assert(PC == $past(PC, 3) + 16'd3);
            end
      end

always @(posedge clk)
  if (f4_past_valid &&
      state == STATE_EXECUTE &&
      $past(state) == STATE_FETCH &&
      ($past(state, 2) == STATE_EXECUTE_DATA_2 ||
       $past(state, 2) == STATE_EXECUTE_ZP ||
       $past(state, 2) == STATE_EXECUTE))
    begin
        if ($past(decoded_instr, 2) == I_EOR)
          assert(A == ($past(A) ^ $past(mem_data)));
        else if ($past(decoded_instr, 2) == I_AND)
          assert(A == ($past(A) & $past(mem_data)));
        else if ($past(decoded_instr, 2) == I_ORA)
          assert(A == ($past(A) | $past(mem_data)));
        else if ($past(decoded_instr, 2) == I_ADC)
          assert(A == ($past(A) + $past(mem_data) + $past(P[P_C])));
        else
          assume(0);

        assert($past(mem_wr, 2) == 1'b0);

        if ($past(address_code, 2) == ADDR_MODE_ABSOLUTE)
          assert($past(f_abs_address, 2) == $past(mem_addr_eff, 2));
        else if ($past(address_code, 2) == ADDR_MODE_ZP)
          assert($past(mem_data, 2) == $past(mem_addr_eff, 2));
        else if ($past(address_code, 2) == ADDR_MODE_INDEXED_ZP)
          assert((($past(mem_data, 3) + $past(X, 3)) & 16'hff) == $past(mem_addr_eff, 2));

        assert(P[P_Z] == (A == 0));
        assert(P[P_N] == (A[7] == 1));
        if ($past(decoded_instr) == I_ADC)
          begin
              assert(P[P_C] == ({1'b0, $past(A)} +
                                {1'b0, $past(mem_data)} +
                                {8'b0, $past(P[P_C])} >= 9'h100));
              assert(P[P_V] == (($past(A[7]) ^ A[7]) & ($past(mem_data[7]) ^ A[7])));
          end
        else
          begin
              assert(P[P_C] == $past(P[P_C], 2));
              assert(P[P_V] == $past(P[P_V], 2));
          end
        assert(P[P_B] == $past(P[P_B], 2));
        assert(P[P_D] == $past(P[P_D], 2));
        assert(P[P_I] == $past(P[P_I], 2));
        assert(S == $past(S, 2));
        assert(X == $past(X, 2));
        assert(Y == $past(Y, 2));

        if (f3_past_valid)
          begin
              if ($past(address_code, 2) == ADDR_MODE_ABSOLUTE)
                assert($past(PC, 2) == $past(PC, 5) + 16'd3);
              else if ($past(address_code, 2) == ADDR_MODE_ZP)
                assert($past(PC, 2) == $past(PC, 4) + 16'd2);
              else if ($past(address_code, 2) == ADDR_MODE_INDEXED_ZP)
                assert($past(PC, 2) == $past(PC, 5) + 16'd2);
              else if ($past(address_code, 2) == ADDR_MODE_IMMEDIATE)
                assert($past(PC, 1) == $past(PC, 3) + 16'd2);
          end
    end

always @(posedge clk)
  if (f2_past_valid && state == STATE_FETCH)
    if ($past(decoded_instr) == I_BNE && $past(address_code) == ADDR_MODE_RELATIVE)
      begin
          if ($past(state) == STATE_BRANCH)
            begin
                assert(PC == $past(PC) + {{8{$past(mem_data[7])}}, mem_data[7:0]} + 1'b1);
                assert(!$past(P[P_Z]));
            end
          else
            begin
                assert(PC == $past(PC) + 1'b1);
                assert($past(P[P_Z]));
            end
      end

always @(posedge clk)
  if (f3_past_valid && state == STATE_FETCH)
    if ($past(decoded_instr) == I_JMP && $past(address_code) == ADDR_MODE_ABSOLUTE)
      begin
          assert(PC == $past(f_abs_address));
          assert(P == $past(P, 3));
          assert(S == $past(S, 3));
          assert(A == $past(A, 3));
          assert(X == $past(X, 3));
          assert(Y == $past(Y, 3));
      end

always @(posedge clk)
  if (f_past_valid)
    assume(state != $past(state));

always @(posedge clk)
  cover(state == STATE_EXECUTE);



`endif

endmodule