diff --git a/src/cpu.verilog b/src/cpu.verilog index 5429a43..e38b16f 100644 --- a/src/cpu.verilog +++ b/src/cpu.verilog @@ -23,6 +23,8 @@ module cpu localparam STATE_FETCH_DATA_2 = 4; localparam STATE_EXECUTE_DATA_2 = 5; localparam STATE_BRANCH = 7; + localparam STATE_EXECUTE_PRE_IDX_1 = 8; + localparam STATE_EXECUTE_PRE_IDX_2 = 9; localparam READ_SOURCE_NONE = 2'h0, @@ -64,6 +66,8 @@ localparam logic [7:0] mem_aux_addr_lo; logic [7:0] mem_aux_addr_hi; + logic [15:0] mem_aux2_addr; + logic [7:0] alu_op_1; logic [7:0] alu_op_2; logic alu_op_c; @@ -95,6 +99,7 @@ initial pending_x_read = 0; initial pending_y_read = 0; initial pending_rel_branch = 0; initial mem_aux_addr = 0; +initial instr = 0; assign o_state[3:0] = state; assign o_state[31:24] = A; @@ -136,6 +141,7 @@ dmux dmuxi( .i_y(Y), .i_sp(S), .i_aux({mem_aux_addr_hi, mem_aux_addr_lo}), + .i_aux2(mem_aux2_addr), .o_mux(mem_addr)); initial state = STATE_FETCH; @@ -146,7 +152,8 @@ always_comb begin mem_aux_addr_lo = mem_aux_addr; mem_aux_addr_hi = 0; - if (address_code == ADDR_MODE_ABSOLUTE) + if (address_code == ADDR_MODE_ABSOLUTE || + address_code == ADDR_MODE_PREINDEXED_INDIRECT) begin mem_aux_addr_hi = mem_data; end @@ -158,6 +165,14 @@ always_comb begin mem_aux_addr_lo = mem_aux_addr; end + else if (address_code == ADDR_MODE_INDEXED_ABSOLUTE_X) + begin + {mem_aux_addr_hi, mem_aux_addr_lo} = {mem_data, mem_aux_addr} + X; + end + else if (address_code == ADDR_MODE_INDEXED_ABSOLUTE_Y) + begin + {mem_aux_addr_hi, mem_aux_addr_lo} = {mem_data, mem_aux_addr} + Y; + end end always_comb @@ -182,8 +197,11 @@ always_comb end else if (address_code == ADDR_MODE_IMMEDIATE || address_code == ADDR_MODE_ABSOLUTE || + address_code == ADDR_MODE_INDEXED_ABSOLUTE_X || + address_code == ADDR_MODE_INDEXED_ABSOLUTE_Y || address_code == ADDR_MODE_ZP || - address_code == ADDR_MODE_INDEXED_ZP) + address_code == ADDR_MODE_INDEXED_ZP || + address_code == ADDR_MODE_PREINDEXED_INDIRECT) begin alu_op_1 = A; alu_op_2 = mem_data; @@ -266,7 +284,9 @@ always @(posedge clk) else if (state == STATE_EXECUTE) begin instr <= mem_data; - if (address_code == ADDR_MODE_ABSOLUTE) + if (address_code == ADDR_MODE_ABSOLUTE || + address_code == ADDR_MODE_INDEXED_ABSOLUTE_X || + address_code == ADDR_MODE_INDEXED_ABSOLUTE_Y) begin PC <= PC + 1; state <= STATE_FETCH_DATA_2; @@ -277,6 +297,10 @@ always @(posedge clk) begin pending_x_read <= READ_SOURCE_MEM; end + if (decoded_instr == I_LDY) + begin + pending_y_read <= READ_SOURCE_MEM; + end else if (decoded_instr == I_LDA) begin pending_a_read <= READ_SOURCE_MEM; @@ -304,6 +328,10 @@ always @(posedge clk) state <= STATE_EXECUTE_ZPX; PC <= PC + 1; end + else if (address_code == ADDR_MODE_PREINDEXED_INDIRECT) + begin + state <= STATE_EXECUTE_PRE_IDX_1; + end else if (address_code == ADDR_MODE_IMPLIED) begin if (decoded_instr == I_DEX) @@ -356,34 +384,48 @@ always @(posedge clk) pending_rel_branch <= 0; state <= STATE_FETCH; end + else if (state == STATE_EXECUTE_PRE_IDX_1) + begin + mem_sel <= DMUX_AUX2; + mem_aux2_addr[7:0] <= mem_data + X; + mem_aux2_addr[15:8] <= 0; + + state <= STATE_EXECUTE_PRE_IDX_2; + end + else if (state == STATE_EXECUTE_PRE_IDX_2) + begin + mem_aux_addr <= mem_data; + mem_aux2_addr[7:0] <= mem_aux2_addr[7:0] + 1'b1; + + state <= STATE_FETCH_DATA_2; + 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; + mem_aux_addr[7:0] <= mem_data; + mem_sel <= DMUX_AUX; - state <= STATE_EXECUTE_DATA_2; - PC <= PC + 1'b1; - end + state <= STATE_EXECUTE_DATA_2; + PC <= PC + 1'b1; end else if (state == STATE_EXECUTE_DATA_2) begin - if (address_code == ADDR_MODE_ABSOLUTE) + 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 - 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 + pending_a_read <= READ_SOURCE_ALU; + end + else if(decoded_instr == I_LDA) + begin + pending_a_read <= READ_SOURCE_MEM; + end + else if(decoded_instr == I_JMP) + begin + PC <= mem_addr; end end @@ -419,12 +461,14 @@ always_comb logic f3_past_valid; logic f4_past_valid; logic f5_past_valid; + logic f6_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; +initial f6_past_valid = 0; always @(posedge clk) f_past_valid <= 1; @@ -444,11 +488,15 @@ always @(posedge clk) if (f4_past_valid) f5_past_valid <= 1; +always @(posedge clk) + if (f5_past_valid) + f6_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(X == $past(X, 2) - 8'd1); assert($past(PC) == $past(PC, 3) + 16'd1); assert(P[P_Z] == (X == 0)); assert(P[P_N] == (X[7] == 1)); @@ -463,7 +511,7 @@ 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(Y == $past(Y, 2) - 8'd1); assert($past(PC) == $past(PC, 3) + 16'd1); assert(P[P_Z] == (Y == 0)); assert(P[P_N] == (Y[7] == 1)); @@ -476,11 +524,11 @@ always @(posedge clk) always @(posedge clk) if (f2_past_valid && state == STATE_EXECUTE) - if ($past(decoded_instr) == I_LDX && $past(address_code) == ADDR_MODE_IMMEDIATE) + if ($past(decoded_instr) == I_LDY && $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)); + assert(Y == $past(mem_data)); + assert(P[P_Z] == (Y == 0)); + assert(P[P_N] == (Y[7] == 1)); if (f3_past_valid) begin assert($past(PC) == $past(PC, 3) + 16'd2); @@ -527,7 +575,7 @@ always @(posedge clk) end always @(posedge clk) - if (f4_past_valid && + if (f6_past_valid && state == STATE_EXECUTE && $past(state) == STATE_FETCH && ($past(state, 2) == STATE_EXECUTE_DATA_2 || @@ -553,6 +601,15 @@ always @(posedge clk) 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)); + else if ($past(address_code, 2) == ADDR_MODE_INDEXED_ABSOLUTE_X) + assert((($past(f_abs_address, 2) + $past(X, 2)) & 16'hffff) == $past(mem_addr_eff, 2)); + else if ($past(address_code, 2) == ADDR_MODE_INDEXED_ABSOLUTE_Y) + assert((($past(f_abs_address, 2) + $past(Y, 2)) & 16'hffff) == $past(mem_addr_eff, 2)); + else if ($past(address_code, 2) == ADDR_MODE_PREINDEXED_INDIRECT) + begin + assert($past(f_abs_address, 2) == $past(mem_addr_eff, 2)); + assert($past(mem_addr_eff, 4) == (($past(mem_data, 5) + $past(X, 5)) & 8'hff)); + end assert(P[P_Z] == (A == 0)); assert(P[P_N] == (A[7] == 1)); @@ -623,7 +680,27 @@ always @(posedge clk) always @(posedge clk) cover(state == STATE_EXECUTE); +always @(posedge clk) + begin + cover(decoded_instr == I_ADC && address_code == ADDR_MODE_IMMEDIATE); + cover(decoded_instr == I_ADC && address_code == ADDR_MODE_ABSOLUTE); + cover(decoded_instr == I_ADC && address_code == ADDR_MODE_ZP); + cover(decoded_instr == I_ADC && address_code == ADDR_MODE_INDEXED_ABSOLUTE_X); + cover(decoded_instr == I_ADC && address_code == ADDR_MODE_INDEXED_ABSOLUTE_Y); + cover(decoded_instr == I_ADC && address_code == ADDR_MODE_INDEXED_ZP); + cover(decoded_instr == I_ADC && address_code == ADDR_MODE_PREINDEXED_INDIRECT); + end +always @(posedge clk) + begin + cover(decoded_instr == I_LDA && address_code == ADDR_MODE_IMMEDIATE); + cover(decoded_instr == I_LDA && address_code == ADDR_MODE_ABSOLUTE); + cover(decoded_instr == I_LDA && address_code == ADDR_MODE_ZP); + cover(decoded_instr == I_LDA && address_code == ADDR_MODE_INDEXED_ABSOLUTE_X); + cover(decoded_instr == I_LDA && address_code == ADDR_MODE_INDEXED_ABSOLUTE_Y); + cover(decoded_instr == I_LDA && address_code == ADDR_MODE_INDEXED_ZP); + cover(decoded_instr == I_LDA && address_code == ADDR_MODE_PREINDEXED_INDIRECT); + end `endif diff --git a/src/decoder.verilog b/src/decoder.verilog index 1c680ea..9b5d1aa 100644 --- a/src/decoder.verilog +++ b/src/decoder.verilog @@ -179,7 +179,7 @@ always_comb begin address_code = ADDR_MODE_ABSOLUTE; end else begin - address_code = ADDR_MODE_INDEXED_ABSOLUTE; + address_code = ADDR_MODE_INDIRECT; end end else if (column == 4) begin @@ -192,7 +192,7 @@ always_comb begin address_code = ADDR_MODE_IMPLIED; end else if (column == 7) begin - address_code = ADDR_MODE_INDEXED_ABSOLUTE; + address_code = ADDR_MODE_INDEXED_ABSOLUTE_X; end end else if(sector == 1) begin @@ -214,8 +214,11 @@ always_comb begin else if (column == 5) begin address_code = ADDR_MODE_INDEXED_ZP; end - else if (column == 6 || column == 7) begin - address_code = ADDR_MODE_INDEXED_ABSOLUTE; + else if (column == 6) begin + address_code = ADDR_MODE_INDEXED_ABSOLUTE_Y; + end + else if (column == 7) begin + address_code = ADDR_MODE_INDEXED_ABSOLUTE_X; end end else if(sector == 2) begin @@ -236,7 +239,10 @@ always_comb begin address_code = ADDR_MODE_INDEXED_ZP; end else if (column == 7) begin - address_code = ADDR_MODE_INDEXED_ABSOLUTE; + if (row == 5) + address_code = ADDR_MODE_INDEXED_ABSOLUTE_Y; + else + address_code = ADDR_MODE_INDEXED_ABSOLUTE_X; end end end diff --git a/src/dmux.verilog b/src/dmux.verilog index b10e6cf..604860f 100644 --- a/src/dmux.verilog +++ b/src/dmux.verilog @@ -1,5 +1,5 @@ `default_nettype none -module dmux(sel, i_pc, i_a, i_x, i_y, i_sp, i_aux, o_mux); +module dmux(sel, i_pc, i_a, i_x, i_y, i_sp, i_aux, i_aux2, o_mux); input wire [2:0] sel; input wire [15:0] i_pc; input wire [7:0] i_a; @@ -7,6 +7,7 @@ module dmux(sel, i_pc, i_a, i_x, i_y, i_sp, i_aux, o_mux); input wire [7:0] i_y; input wire [7:0] i_sp; input wire [15:0] i_aux; + input wire [15:0] i_aux2; output logic [15:0] o_mux; `include "parameters.vh" @@ -26,6 +27,8 @@ always_comb o_mux[15:0] = { 8'h1, i_sp }; else if (sel == DMUX_AUX) o_mux = i_aux; + else if (sel == DMUX_AUX2) + o_mux = i_aux2; end endmodule diff --git a/src/mio.verilog b/src/mio.verilog index 621cd0c..6f50864 100644 --- a/src/mio.verilog +++ b/src/mio.verilog @@ -7,17 +7,7 @@ module mio(clk, i_data, i_addr, i_wr, o_data, o_led); input wire i_wr; reg [14:0] mem_addr; - -`ifndef VERILOG -//output wire [7:0] o_data; -//wire rst; -//wire ce; -//assign rst = 0; -//assign ce = 1; - -`endif - output logic [7:0] o_data; output logic [5:0] o_led; reg [7:0] memory [0:32768]; @@ -27,7 +17,7 @@ initial o_led = 6'h3f; `ifndef FORMAL initial $readmemh("foo.hex", memory, 0, 32); initial begin - for (integer i = 32; i < 256; i++) + for (integer i = 32; i < 8192; i++) begin memory[i] = 0; end diff --git a/src/parameters.vh b/src/parameters.vh index 2568536..114854d 100644 --- a/src/parameters.vh +++ b/src/parameters.vh @@ -3,12 +3,13 @@ localparam ADDR_MODE_IMPLIED = 0; localparam ADDR_MODE_IMMEDIATE = 1; localparam ADDR_MODE_ABSOLUTE = 2; localparam ADDR_MODE_ZP = 3; -localparam ADDR_MODE_INDEXED_ABSOLUTE = 4; +localparam ADDR_MODE_INDEXED_ABSOLUTE_X = 4; localparam ADDR_MODE_INDEXED_ZP = 5; localparam ADDR_MODE_INDIRECT = 6; localparam ADDR_MODE_PREINDEXED_INDIRECT = 7; localparam ADDR_MODE_POSTINDEXED_INDIRECT = 8; localparam ADDR_MODE_RELATIVE = 9; +localparam ADDR_MODE_INDEXED_ABSOLUTE_Y = 10; localparam OP_OR = 0; localparam OP_AND = 1; @@ -98,3 +99,4 @@ localparam DMUX_X = 3'h2; localparam DMUX_Y = 3'h3; localparam DMUX_SP = 3'h4; localparam DMUX_AUX = 3'h5; +localparam DMUX_AUX2 = 3'h6; diff --git a/src/slon.sby b/src/slon.sby index 4ae2451..88eba2e 100644 --- a/src/slon.sby +++ b/src/slon.sby @@ -4,9 +4,9 @@ cvr [options] prf: mode prove -prf: depth 20 +prf: depth 30 cvr: mode cover -cvr: depth 40 +cvr: depth 60 [engines] smtbmc yices