src/cpu.verilog

@@ -18,13 +18,11 @@ module cpu
     localparam STATE_START_0 = 4'hb;
     localparam STATE_FETCH = 0;
     localparam STATE_EXECUTE = 1;
-    localparam STATE_EXECUTE_ZPX = 2;
+    localparam STATE_WRITE = 2;
     localparam STATE_EXECUTE_ZP = 3;
     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,
@@ -66,8 +64,6 @@ 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;
@@ -84,7 +80,6 @@ localparam
     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;
@@ -98,15 +93,11 @@ 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;
-initial instr = 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),
@@ -141,7 +132,6 @@ 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;
@@ -152,8 +142,7 @@ always_comb
   begin
       mem_aux_addr_lo = mem_aux_addr;
       mem_aux_addr_hi = 0;
-      if (address_code == ADDR_MODE_ABSOLUTE ||
-          address_code == ADDR_MODE_PREINDEXED_INDIRECT)
+      if (address_code == ADDR_MODE_ABSOLUTE)
         begin
             mem_aux_addr_hi = mem_data;
         end
@@ -161,18 +150,6 @@ always_comb
         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
-      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
@@ -197,34 +174,29 @@ 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_PREINDEXED_INDIRECT)
+               address_code == ADDR_MODE_ZP)
         begin
-            alu_op_1 = A;
-            alu_op_2 = mem_data;
             if (decoded_instr == I_EOR)
               begin
+                  alu_op_1 = A;
+                  alu_op_2 = mem_data;
                   alu_op_c = 0;
                   alu_op_sel = OP_EOR;
               end
             else if (decoded_instr == I_AND)
               begin
+                  alu_op_1 = A;
+                  alu_op_2 = mem_data;
                   alu_op_c = 0;
                   alu_op_sel = OP_AND;
               end
             else if (decoded_instr == I_ORA)
               begin
+                  alu_op_1 = A;
+                  alu_op_2 = mem_data;
                   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
 
@@ -242,11 +214,6 @@ always @(posedge clk)
               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;
 
@@ -284,9 +251,7 @@ always @(posedge clk)
   else if (state == STATE_EXECUTE)
     begin
         instr <= mem_data;
-        if (address_code == ADDR_MODE_ABSOLUTE ||
-            address_code == ADDR_MODE_INDEXED_ABSOLUTE_X ||
-            address_code == ADDR_MODE_INDEXED_ABSOLUTE_Y)
+        if (address_code == ADDR_MODE_ABSOLUTE)
           begin
               PC <= PC + 1;
               state <= STATE_FETCH_DATA_2;
@@ -297,18 +262,13 @@ 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;
                 end
               else if (decoded_instr == I_EOR ||
                        decoded_instr == I_AND ||
-                       decoded_instr == I_ORA ||
-                       decoded_instr == I_ADC)
+                       decoded_instr == I_ORA)
                 begin
                     pending_a_read <= READ_SOURCE_ALU;
                 end
@@ -322,16 +282,6 @@ always @(posedge clk)
               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_PREINDEXED_INDIRECT)
-          begin
-              state <= STATE_EXECUTE_PRE_IDX_1;
-          end
         else if (address_code == ADDR_MODE_IMPLIED)
           begin
               if (decoded_instr == I_DEX)
@@ -359,17 +309,9 @@ always @(posedge clk)
                 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_aux_addr <= mem_data;
         mem_sel <= DMUX_PC;
         pending_a_read <= READ_SOURCE_ALU;
 
@@ -384,48 +326,34 @@ 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
-        mem_aux_addr[7:0] <= mem_data;
-        mem_sel <= DMUX_AUX;
+        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;
+              state <= STATE_EXECUTE_DATA_2;
+              PC <= PC + 1'b1;
+          end
     end
     else if (state == STATE_EXECUTE_DATA_2)
         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_LDA)
-              begin
-                  pending_a_read <= READ_SOURCE_MEM;
-              end
-            else if(decoded_instr == I_JMP)
+            if (address_code == ADDR_MODE_ABSOLUTE)
               begin
-                  PC <= mem_addr;
+                  mem_sel <= DMUX_PC;
+                  state <= STATE_FETCH;
+                  if (decoded_instr == I_EOR ||
+                      decoded_instr == I_AND ||
+                      decoded_instr == I_ORA)
+                    begin
+                        tmp <= mem_data;
+                        pending_a_read <= READ_SOURCE_ALU;
+                    end
+                  else if(decoded_instr == I_JMP)
+                    begin
+                        PC <= mem_addr;
+                    end
               end
         end
 
@@ -461,14 +389,12 @@ 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;
 
@@ -488,15 +414,11 @@ 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, 2) - 8'd1);
+          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));
@@ -511,7 +433,7 @@ always @(posedge clk)
   if (f2_past_valid && state == STATE_EXECUTE)
     if ($past(decoded_instr) == I_DEY)
       begin
-          assert(Y == $past(Y, 2) - 8'd1);
+          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));
@@ -524,11 +446,11 @@ always @(posedge clk)
 
 always @(posedge clk)
   if (f2_past_valid && state == STATE_EXECUTE)
-    if ($past(decoded_instr) == I_LDY && $past(address_code) == ADDR_MODE_IMMEDIATE)
+    if ($past(decoded_instr) == I_LDX && $past(address_code) == ADDR_MODE_IMMEDIATE)
       begin
-          assert(Y == $past(mem_data));
-          assert(P[P_Z] == (Y == 0));
-          assert(P[P_N] == (Y[7] == 1));
+          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);
@@ -575,7 +497,7 @@ always @(posedge clk)
       end
 
 always @(posedge clk)
-  if (f6_past_valid &&
+  if (f4_past_valid &&
       state == STATE_EXECUTE &&
       $past(state) == STATE_FETCH &&
       ($past(state, 2) == STATE_EXECUTE_DATA_2 ||
@@ -588,8 +510,6 @@ always @(posedge clk)
           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);
 
@@ -599,32 +519,11 @@ always @(posedge clk)
           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));
-        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));
-        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_C] == $past(P[P_C], 2));
+        assert(P[P_V] == $past(P[P_V], 2));
         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));
@@ -638,8 +537,6 @@ always @(posedge clk)
                 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
@@ -680,27 +577,7 @@ 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_INDIRECT;
+                    address_code = ADDR_MODE_INDEXED_ABSOLUTE;
                 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_X;
+                address_code = ADDR_MODE_INDEXED_ABSOLUTE;
             end
         end
         else if(sector == 1) begin
@@ -214,11 +214,8 @@ always_comb begin
             else if (column == 5) begin
                 address_code = ADDR_MODE_INDEXED_ZP;
             end
-            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;
+            else if (column == 6 || column == 7) begin
+                address_code = ADDR_MODE_INDEXED_ABSOLUTE;
             end
         end
         else if(sector == 2) begin
@@ -239,10 +236,7 @@ always_comb begin
                 address_code = ADDR_MODE_INDEXED_ZP;
             end
             else if (column == 7) begin
-                if (row == 5)
-                  address_code = ADDR_MODE_INDEXED_ABSOLUTE_Y;
-                else
-                  address_code = ADDR_MODE_INDEXED_ABSOLUTE_X;
+                address_code = ADDR_MODE_INDEXED_ABSOLUTE;
             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, i_aux2, o_mux);
+module dmux(sel, i_pc, i_a, i_x, i_y, i_sp, i_aux, o_mux);
     input wire [2:0] sel;
     input wire [15:0] i_pc;
     input wire [7:0] i_a;
@@ -7,7 +7,6 @@ module dmux(sel, i_pc, i_a, i_x, i_y, i_sp, i_aux, i_aux2, 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"
@@ -27,8 +26,6 @@ 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,6 +8,16 @@ 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];
@@ -17,7 +27,7 @@ initial o_led = 6'h3f;
 `ifndef FORMAL
 initial $readmemh("foo.hex", memory, 0, 32);
 initial begin
-    for (integer i = 32; i < 8192; i++)
+    for (integer i = 32; i < 256; i++)
       begin
           memory[i] = 0;
       end

src/parameters.vh

@@ -3,13 +3,12 @@ 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_X = 4;
+localparam ADDR_MODE_INDEXED_ABSOLUTE = 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;
@@ -99,4 +98,3 @@ 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 30
+prf: depth 20
 cvr: mode cover
-cvr: depth 60
+cvr: depth 40
 
 [engines]
 smtbmc yices