Add preindexed indirect mode

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,9 +384,22 @@ always @(posedge clk)
         pending_rel_branch <= 0;
         state <= STATE_FETCH;
     end
-  else if (state == STATE_FETCH_DATA_2)
+  else if (state == STATE_EXECUTE_PRE_IDX_1)
     begin
-        if (address_code == ADDR_MODE_ABSOLUTE)
+        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
         mem_aux_addr[7:0] <= mem_data;
         mem_sel <= DMUX_AUX;
@@ -366,13 +407,11 @@ always @(posedge clk)
         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 ||
@@ -380,12 +419,15 @@ always @(posedge clk)
               begin
                   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
-        end
 
 always_comb
   begin
@@ -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
 

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

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

src/mio.verilog

@@ -8,16 +8,6 @@ module mio(clk, i_data, i_addr, i_wr, o_data, o_led);
 
     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

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;

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