Add STX, STY instructions

src/cpu.verilog

@@ -11,7 +11,6 @@ module cpu
 
 `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;
@@ -23,8 +22,11 @@ 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_IDX_1 = 8;
-    localparam STATE_EXECUTE_PRE_IDX_2 = 9;
+    localparam STATE_EXECUTE_IDX_2 = 9;
+    localparam STATE_EXECUTE_POST_IDX_1 = 10;
+    localparam STATE_EXECUTE_POST_IDX_2 = 11;
+    localparam STATE_DELAY = 12;
 
 localparam
           READ_SOURCE_NONE = 2'h0,
@@ -85,6 +87,8 @@ localparam
     logic [1:0]  pending_y_read;
     logic        pending_rel_branch;
     wire         is_arith;
+    logic [2:0]  extra_timing;
+    reg [3:0]  state_after_delay;
 
 initial A = 0;
 initial X = 0;
@@ -100,12 +104,13 @@ initial pending_y_read = 0;
 initial pending_rel_branch = 0;
 initial mem_aux_addr = 0;
 initial instr = 0;
+initial extra_timing = 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);
+assign is_arith = (decoded_instr == I_ADC || decoded_instr == I_SBC);
 
 alu alui(
          .A(alu_op_1),
@@ -173,6 +178,21 @@ always_comb
         begin
             {mem_aux_addr_hi, mem_aux_addr_lo} = {mem_data, mem_aux_addr} + Y;
         end
+      else if (address_code == ADDR_MODE_POSTINDEXED_INDIRECT)
+        begin
+            if (state == STATE_EXECUTE_POST_IDX_1)
+              begin
+                  {mem_aux_addr_hi, mem_aux_addr_lo} = {8'h0, mem_data};
+              end
+            else if (state == STATE_EXECUTE_POST_IDX_2)
+              begin
+                  {mem_aux_addr_hi, mem_aux_addr_lo} = {8'h0, mem_aux2_addr};
+              end
+            else
+              begin
+                  {mem_aux_addr_hi, mem_aux_addr_lo} = {mem_data, mem_aux_addr} + Y;
+              end
+        end
   end
 
 always_comb
@@ -195,13 +215,7 @@ always_comb
             alu_op_c = 1'b1;
             alu_op_sel = OP_SUB;
         end
-      else if (address_code == ADDR_MODE_IMMEDIATE ||
+      else
-               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)
         begin
             alu_op_1 = A;
             alu_op_2 = mem_data;
@@ -225,11 +239,26 @@ always_comb
                   alu_op_c = P[P_C];
                   alu_op_sel = OP_ADC;
               end
+            else if (decoded_instr == I_SBC)
+              begin
+                  alu_op_c = P[P_C];
+                  alu_op_sel = OP_SUB;
+              end
         end
   end
 
 always @(posedge clk)
-  if (state == STATE_FETCH)
+  if (extra_timing > 0)
+    begin
+        extra_timing <= extra_timing - 1'b1;
+    end
+  else if (state == STATE_FETCH)
+    begin
+        if (extra_timing > 0)
+          begin
+              extra_timing <= extra_timing - 1'b1;
+          end
+        else
           begin
               if (pending_a_read == READ_SOURCE_MEM)
                 begin
@@ -281,6 +310,7 @@ always @(posedge clk)
               PC <= PC + 1;
               state <= STATE_EXECUTE;
           end
+    end
   else if (state == STATE_EXECUTE)
     begin
         instr <= mem_data;
@@ -308,7 +338,8 @@ always @(posedge clk)
               else if (decoded_instr == I_EOR ||
                        decoded_instr == I_AND ||
                        decoded_instr == I_ORA ||
-                       decoded_instr == I_ADC)
+                       decoded_instr == I_ADC ||
+                       decoded_instr == I_SBC)
                 begin
                     pending_a_read <= READ_SOURCE_ALU;
                 end
@@ -330,7 +361,16 @@ always @(posedge clk)
           end
         else if (address_code == ADDR_MODE_PREINDEXED_INDIRECT)
           begin
-              state <= STATE_EXECUTE_PRE_IDX_1;
+              state <= STATE_EXECUTE_IDX_1;
+          end
+        else if(address_code == ADDR_MODE_POSTINDEXED_INDIRECT)
+          begin
+              mem_sel <= DMUX_AUX;
+              state <= STATE_EXECUTE_POST_IDX_1;
+              if (decoded_instr == I_STA)
+                begin
+                    extra_timing <= 1;
+                end
           end
         else if (address_code == ADDR_MODE_IMPLIED)
           begin
@@ -360,8 +400,15 @@ always @(posedge clk)
           end
     end
   else if (state == STATE_EXECUTE_ZPX)
+    begin
+        if (decoded_instr != I_LDX)
           begin
               mem_aux_addr <= mem_data + X;
+          end
+        else
+          begin
+              mem_aux_addr <= mem_data + Y;
+          end
         state <= STATE_EXECUTE_ZP;
     end
   else if (state == STATE_EXECUTE_ZP)
@@ -371,7 +418,26 @@ always @(posedge clk)
               mem_aux_addr <= mem_data;
           end
         mem_sel <= DMUX_PC;
+        if (decoded_instr == I_LDA)
+          begin
+              pending_a_read <= READ_SOURCE_MEM;
+          end
+        else if (decoded_instr == I_LDX)
+          begin
+              pending_x_read <= READ_SOURCE_MEM;
+          end
+        else if (decoded_instr == I_LDY)
+          begin
+              pending_y_read <= READ_SOURCE_MEM;
+          end
+        else if (decoded_instr == I_ORA ||
+                 decoded_instr == I_AND ||
+                 decoded_instr == I_EOR ||
+                 decoded_instr == I_ADC ||
+                 decoded_instr == I_SBC)
+          begin
               pending_a_read <= READ_SOURCE_ALU;
+          end
 
         state <= STATE_FETCH;
     end
@@ -384,21 +450,39 @@ always @(posedge clk)
         pending_rel_branch <= 0;
         state <= STATE_FETCH;
     end
-  else if (state == STATE_EXECUTE_PRE_IDX_1)
+  else if (state == STATE_EXECUTE_IDX_1)
     begin
         mem_sel <= DMUX_AUX2;
+        if (address_code == ADDR_MODE_PREINDEXED_INDIRECT)
+          begin
               mem_aux2_addr[7:0] <= mem_data + X;
+          end
+        else
+          begin
+              mem_aux2_addr[7:0] <= mem_data;
+          end
         mem_aux2_addr[15:8] <= 0;
 
-        state <= STATE_EXECUTE_PRE_IDX_2;
+        state <= STATE_EXECUTE_IDX_2;
     end
-  else if (state == STATE_EXECUTE_PRE_IDX_2)
+  else if (state == STATE_EXECUTE_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_EXECUTE_POST_IDX_1)
+    begin
+        mem_aux2_addr <= mem_data + 1'b1;
+        state <= STATE_EXECUTE_POST_IDX_2;
+    end
+  else if (state == STATE_EXECUTE_POST_IDX_2)
+    begin
+        mem_aux_addr <= mem_data;
+        state <= STATE_EXECUTE_DATA_2;
+        PC <= PC + 1'b1;
+    end
   else if (state == STATE_FETCH_DATA_2)
     begin
         mem_aux_addr[7:0] <= mem_data;
@@ -415,7 +499,8 @@ always @(posedge clk)
         if (decoded_instr == I_EOR ||
             decoded_instr == I_AND ||
             decoded_instr == I_ORA ||
-                decoded_instr == I_ADC)
+            decoded_instr == I_ADC ||
+            decoded_instr == I_SBC)
           begin
               pending_a_read <= READ_SOURCE_ALU;
           end
@@ -423,6 +508,14 @@ always @(posedge clk)
           begin
               pending_a_read <= READ_SOURCE_MEM;
           end
+        else if(decoded_instr == I_LDX)
+          begin
+              pending_x_read <= READ_SOURCE_MEM;
+          end
+        else if(decoded_instr == I_LDY)
+          begin
+              pending_y_read <= READ_SOURCE_MEM;
+          end
         else if(decoded_instr == I_JMP)
           begin
               PC <= mem_addr;
@@ -435,21 +528,38 @@ always_comb
       mem_wr = 0;
       if (state == STATE_EXECUTE_DATA_2)
         begin
-            if (address_code == ADDR_MODE_ABSOLUTE)
+            if (decoded_instr == I_STA)
-              begin
-                  if(decoded_instr == I_STA)
               begin
+                  mem_wr = 1'b1;
                   mem_data_wr = A;
+              end
+            else if (decoded_instr == I_STX)
+              begin
                   mem_wr = 1'b1;
+                  mem_data_wr = X;
               end
+            else if (decoded_instr == I_STY)
+              begin
+                  mem_wr = 1'b1;
+                  mem_data_wr = Y;
               end
         end
       else if (state == STATE_EXECUTE_ZP)
         begin
             if(decoded_instr == I_STA)
               begin
+                  mem_wr = 1'b1;
                   mem_data_wr = A;
+              end
+            else if(decoded_instr == I_STX)
+              begin
                   mem_wr = 1'b1;
+                  mem_data_wr = X;
+              end
+            else if(decoded_instr == I_STY)
+              begin
+                  mem_wr = 1'b1;
+                  mem_data_wr = Y;
               end
         end
   end
@@ -463,6 +573,13 @@ always_comb
     logic f5_past_valid;
     logic f6_past_valid;
 
+    logic [7:0] f_prev_instruction;
+    logic [4:0] f_prev_addr_code;
+    logic f_prev_instruction_is_branch;
+
+
+initial f_prev_instruction = 0;
+initial f_prev_addr_code = 0;
 initial f_past_valid = 0;
 initial f2_past_valid = 0;
 initial f3_past_valid = 0;
@@ -492,6 +609,34 @@ always @(posedge clk)
     if (f5_past_valid)
       f6_past_valid <= 1;
 
+    logic [7:0] f_instr_count;
+initial f_instr_count = 0;
+always @(posedge clk)
+    if (state == STATE_FETCH && $past(state) != STATE_FETCH)
+      f_instr_count <= f_instr_count + 1'b1;
+
+always @(posedge clk)
+  if (f2_past_valid && state == STATE_FETCH && $past(state) != STATE_FETCH)
+    begin
+        f_prev_instruction <= $past(decoded_instr);
+        f_prev_addr_code <= $past(address_code);
+    end
+
+always @(*)
+    f_prev_instruction_is_branch <=
+                                   (f_prev_instruction == I_JMP ||
+                                    f_prev_instruction == I_BCC ||
+                                    f_prev_instruction == I_BCS ||
+                                    f_prev_instruction == I_BEQ ||
+                                    f_prev_instruction == I_BMI ||
+                                    f_prev_instruction == I_BNE ||
+                                    f_prev_instruction == I_BPL ||
+                                    f_prev_instruction == I_BVC ||
+                                    f_prev_instruction == I_BVS ||
+                                    f_prev_instruction == I_JSR ||
+                                    f_prev_instruction == I_RTS ||
+                                    f_prev_instruction == I_RTI);
+
 always @(posedge clk)
   if (f2_past_valid && state == STATE_EXECUTE)
     if ($past(decoded_instr) == I_DEX)
@@ -562,45 +707,84 @@ always_comb
   end
 
 always @(posedge clk)
-  if (f2_past_valid && state == STATE_EXECUTE_DATA_2)
+    if (f_past_valid)
-    if ($past(decoded_instr) == I_STA && $past(address_code) == ADDR_MODE_ABSOLUTE)
+begin
-      begin
+      assume(decoded_instr == I_LDA ||
-          assert(mem_wr == 1'b1);
+             decoded_instr == I_LDX ||
-          assert(mem_data_wr == A);
+             decoded_instr == I_LDY ||
-          assert(f_abs_address == mem_addr_eff);
+             decoded_instr == I_STA ||
-          if (f3_past_valid)
+             decoded_instr == I_STX ||
-            begin
+             decoded_instr == I_STY ||
-                assert(PC == $past(PC, 3) + 16'd3);
+             decoded_instr == I_AND ||
-            end
+             decoded_instr == I_EOR ||
+             decoded_instr == I_ORA ||
+             decoded_instr == I_ADC ||
+             decoded_instr == I_SBC ||
+             decoded_instr == I_DEX ||
+             decoded_instr == I_DEY ||
+             decoded_instr == I_BNE ||
+             decoded_instr == I_JMP
+);
+    assume(address_code != ADDR_MODE_INDIRECT);
     end
 
 always @(posedge clk)
-  if (f6_past_valid &&
+  if (f6_past_valid && state == STATE_EXECUTE && $past(state) == STATE_FETCH)
-      state == STATE_EXECUTE &&
+    begin
-      $past(state) == STATE_FETCH &&
+        if (f_prev_instruction == I_EOR)
-      ($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)
+        else if (f_prev_instruction == I_AND)
           assert(A == ($past(A) & $past(mem_data)));
-        else if ($past(decoded_instr, 2) == I_ORA)
+        else if (f_prev_instruction == I_ORA)
           assert(A == ($past(A) | $past(mem_data)));
-        else if ($past(decoded_instr, 2) == I_ADC)
+        else if (f_prev_instruction == I_ADC)
           assert(A == ($past(A) + $past(mem_data) + $past(P[P_C])));
-        else
+        else if (f_prev_instruction == I_SBC)
-          assume(0);
+          assert(A == ($past(A) - $past(mem_data) - (1'b1 - $past(P[P_C]))));
+        else if (f_prev_instruction == I_LDA)
+          assert(A == $past(mem_data));
+        else if (f_prev_instruction == I_LDX)
+          assert(X == $past(mem_data));
+        else if (f_prev_instruction == I_LDY)
+          assert(Y == $past(mem_data));
+        else if (f_prev_instruction == I_STA)
+          assert(A == $past(A));
+        else if (f_prev_instruction == I_STX)
+          assert(X == $past(X));
+        else if (f_prev_instruction == I_STY)
+          assert(Y == $past(Y));
 
+        if (f_prev_instruction == I_STA)
+          begin
+              assert($past(mem_wr, 2) == 1'b1);
+              assert($past(mem_data_wr, 2) == $past(A, 2));
+          end
+        else if (f_prev_instruction == I_STX)
+          begin
+              assert($past(mem_wr, 2) == 1'b1);
+              assert($past(mem_data_wr, 2) == $past(X, 2));
+          end
+        else if (f_prev_instruction == I_STY)
+          begin
+              assert($past(mem_wr, 2) == 1'b1);
+              assert($past(mem_data_wr, 2) == $past(Y, 2));
+          end
+        else
+          begin
               assert($past(mem_wr, 2) == 1'b0);
+          end
 
         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)
+          begin
+              if (f_prev_instruction != I_LDX)
                 assert((($past(mem_data, 3) + $past(X, 3)) & 16'hff) == $past(mem_addr_eff, 2));
+              else
+                assert((($past(mem_data, 3) + $past(Y, 3)) & 16'hff) == $past(mem_addr_eff, 2));
+          end
         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)
@@ -610,16 +794,52 @@ always @(posedge clk)
               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
+        else if ($past(address_code, 2) == ADDR_MODE_POSTINDEXED_INDIRECT)
+          begin
+              assert(($past(f_abs_address, 2) + $past(Y, 2)) == $past(mem_addr_eff, 2));
+          end
 
+        if (f_prev_instruction == I_LDX ||
+            f_prev_instruction == I_DEX)
+            begin
+                assert(P[P_Z] == (X == 0));
+                assert(P[P_N] == (X[7] == 1));
+            end
+        else if (f_prev_instruction == I_LDY ||
+            f_prev_instruction == I_DEY)
+            begin
+                assert(P[P_Z] == (Y == 0));
+                assert(P[P_N] == (Y[7] == 1));
+            end
+        else if (f_prev_instruction == I_LDA ||
+                 f_prev_instruction == I_ORA ||
+                 f_prev_instruction == I_AND ||
+                 f_prev_instruction == I_EOR ||
+                 f_prev_instruction == I_ADC ||
+                 f_prev_instruction == I_SBC)
+          begin
               assert(P[P_Z] == (A == 0));
               assert(P[P_N] == (A[7] == 1));
-        if ($past(decoded_instr) == I_ADC)
+          end
+        else
+          begin
+              assert(P[P_Z] == $past(P[P_Z], 2));
+              assert(P[P_N] == $past(P[P_N], 2));
+          end
+        if (f_prev_instruction == 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 if (f_prev_instruction == I_SBC)
+          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));
@@ -629,19 +849,50 @@ always @(posedge clk)
         assert(P[P_D] == $past(P[P_D], 2));
         assert(P[P_I] == $past(P[P_I], 2));
         assert(S == $past(S, 2));
+        if (f_prev_instruction != I_LDX &&
+            f_prev_instruction != I_DEX &&
+            f_prev_instruction != I_INX)
+          begin
               assert(X == $past(X, 2));
+          end
+        if (f_prev_instruction != I_LDY &&
+            f_prev_instruction != I_DEY &&
+            f_prev_instruction != I_INY)
+          begin
               assert(Y == $past(Y, 2));
+          end
 
-        if (f3_past_valid)
+        if (f6_past_valid && !f_prev_instruction_is_branch)
           begin
               if ($past(address_code, 2) == ADDR_MODE_ABSOLUTE)
-                assert($past(PC, 2) == $past(PC, 5) + 16'd3);
+                assert($past(PC, 1) == $past(PC, 5) + 16'd3);
               else if ($past(address_code, 2) == ADDR_MODE_ZP)
-                assert($past(PC, 2) == $past(PC, 4) + 16'd2);
+                assert($past(PC, 1) == $past(PC, 4) + 16'd2);
               else if ($past(address_code, 2) == ADDR_MODE_INDEXED_ZP)
-                assert($past(PC, 2) == $past(PC, 5) + 16'd2);
+                assert($past(PC, 1) == $past(PC, 5) + 16'd2);
               else if ($past(address_code, 2) == ADDR_MODE_IMMEDIATE)
                 assert($past(PC, 1) == $past(PC, 3) + 16'd2);
+              else if ($past(address_code, 2) == ADDR_MODE_PREINDEXED_INDIRECT)
+                assert($past(PC, 1) == $past(PC, 7) + 16'd2);
+
+              if (f_prev_instruction != I_STA)
+                begin
+                    if ($past(address_code, 2) == ADDR_MODE_INDEXED_ABSOLUTE_X)
+                      assert($past(PC, 1) == $past(PC, 5) + 16'd3);
+                    else if ($past(address_code, 2) == ADDR_MODE_INDEXED_ABSOLUTE_Y)
+                      assert($past(PC, 1) == $past(PC, 5) + 16'd3);
+                    else if ($past(address_code, 2) == ADDR_MODE_POSTINDEXED_INDIRECT)
+                      assert($past(PC, 1) == $past(PC, 6) + 16'd2);
+                end
+              else
+                begin
+                    if ($past(address_code, 2) == ADDR_MODE_INDEXED_ABSOLUTE_X)
+                      assert($past(PC, 1) == $past(PC, 5) + 16'd3);
+                    else if ($past(address_code, 2) == ADDR_MODE_INDEXED_ABSOLUTE_Y)
+                      assert($past(PC, 1) == $past(PC, 5) + 16'd3);
+                    else if ($past(address_code, 2) == ADDR_MODE_POSTINDEXED_INDIRECT)
+                      assert($past(PC, 1) == $past(PC, 7) + 16'd2);
+                end
           end
     end
 
@@ -674,34 +925,143 @@ always @(posedge clk)
       end
 
 always @(posedge clk)
-  if (f_past_valid)
+  cover(state == STATE_EXECUTE);
-    assume(state != $past(state));
 
 always @(posedge clk)
-  cover(state == STATE_EXECUTE);
+  cover(f6_past_valid);
+
+always @(posedge clk)
+  cover(f_instr_count > 16);
+
+always @(posedge clk)
+  begin
+      if (decoded_instr == I_ADC)
+        begin
+            cover(address_code == ADDR_MODE_IMMEDIATE);
+            cover(address_code == ADDR_MODE_ABSOLUTE);
+            cover(address_code == ADDR_MODE_ZP);
+            cover(address_code == ADDR_MODE_INDEXED_ABSOLUTE_X);
+            cover(address_code == ADDR_MODE_INDEXED_ABSOLUTE_Y);
+            cover(address_code == ADDR_MODE_INDEXED_ZP);
+            cover(address_code == ADDR_MODE_PREINDEXED_INDIRECT);
+            cover(address_code == ADDR_MODE_POSTINDEXED_INDIRECT);
+        end
+  end
 
 always @(posedge clk)
   begin
-      cover(decoded_instr == I_ADC && address_code == ADDR_MODE_IMMEDIATE);
+      if (decoded_instr == I_SBC)
-      cover(decoded_instr == I_ADC && address_code == ADDR_MODE_ABSOLUTE);
+        begin
-      cover(decoded_instr == I_ADC && address_code == ADDR_MODE_ZP);
+            cover(address_code == ADDR_MODE_IMMEDIATE);
-      cover(decoded_instr == I_ADC && address_code == ADDR_MODE_INDEXED_ABSOLUTE_X);
+            cover(address_code == ADDR_MODE_ABSOLUTE);
-      cover(decoded_instr == I_ADC && address_code == ADDR_MODE_INDEXED_ABSOLUTE_Y);
+            cover(address_code == ADDR_MODE_ZP);
-      cover(decoded_instr == I_ADC && address_code == ADDR_MODE_INDEXED_ZP);
+            cover(address_code == ADDR_MODE_INDEXED_ABSOLUTE_X);
-      cover(decoded_instr == I_ADC && address_code == ADDR_MODE_PREINDEXED_INDIRECT);
+            cover(address_code == ADDR_MODE_INDEXED_ABSOLUTE_Y);
+            cover(address_code == ADDR_MODE_INDEXED_ZP);
+            cover(address_code == ADDR_MODE_PREINDEXED_INDIRECT);
+            cover(address_code == ADDR_MODE_POSTINDEXED_INDIRECT);
+        end
   end
 
 always @(posedge clk)
   begin
-      cover(decoded_instr == I_LDA && address_code == ADDR_MODE_IMMEDIATE);
+      if (decoded_instr == I_LDA)
-      cover(decoded_instr == I_LDA && address_code == ADDR_MODE_ABSOLUTE);
+        begin
-      cover(decoded_instr == I_LDA && address_code == ADDR_MODE_ZP);
+            cover(address_code == ADDR_MODE_IMMEDIATE);
-      cover(decoded_instr == I_LDA && address_code == ADDR_MODE_INDEXED_ABSOLUTE_X);
+            cover(address_code == ADDR_MODE_ABSOLUTE);
-      cover(decoded_instr == I_LDA && address_code == ADDR_MODE_INDEXED_ABSOLUTE_Y);
+            cover(address_code == ADDR_MODE_ZP);
-      cover(decoded_instr == I_LDA && address_code == ADDR_MODE_INDEXED_ZP);
+            cover(address_code == ADDR_MODE_INDEXED_ABSOLUTE_X);
-      cover(decoded_instr == I_LDA && address_code == ADDR_MODE_PREINDEXED_INDIRECT);
+            cover(address_code == ADDR_MODE_INDEXED_ABSOLUTE_Y);
+            cover(address_code == ADDR_MODE_INDEXED_ZP);
+            cover(address_code == ADDR_MODE_PREINDEXED_INDIRECT);
+            cover(address_code == ADDR_MODE_POSTINDEXED_INDIRECT);
+        end
+  end
+
+always @(posedge clk)
+  begin
+      if (decoded_instr == I_STA)
+        begin
+            cover(address_code == ADDR_MODE_ZP);
+            cover(address_code == ADDR_MODE_INDEXED_ZP);
+            cover(address_code == ADDR_MODE_ABSOLUTE);
+            cover(address_code == ADDR_MODE_INDEXED_ABSOLUTE_X);
+            cover(address_code == ADDR_MODE_INDEXED_ABSOLUTE_Y);
+            cover(address_code == ADDR_MODE_PREINDEXED_INDIRECT);
+            cover(address_code == ADDR_MODE_POSTINDEXED_INDIRECT);
+        end
+  end
+
+always @(posedge clk)
+  begin
+      if (decoded_instr == I_LDX)
+        begin
+            cover(address_code == ADDR_MODE_IMMEDIATE);
+            cover(address_code == ADDR_MODE_ABSOLUTE);
+            cover(address_code == ADDR_MODE_ZP);
+            cover(address_code == ADDR_MODE_INDEXED_ABSOLUTE_Y);
+            cover(address_code == ADDR_MODE_INDEXED_ZP);
+        end
+  end
+
+always @(posedge clk)
+  begin
+      if (decoded_instr == I_EOR)
+        begin
+            cover(address_code == ADDR_MODE_IMMEDIATE);
+            cover(address_code == ADDR_MODE_ABSOLUTE);
+            cover(address_code == ADDR_MODE_ZP);
+            cover(address_code == ADDR_MODE_INDEXED_ABSOLUTE_X);
+            cover(address_code == ADDR_MODE_INDEXED_ABSOLUTE_Y);
+            cover(address_code == ADDR_MODE_INDEXED_ZP);
+            cover(address_code == ADDR_MODE_PREINDEXED_INDIRECT);
+            cover(address_code == ADDR_MODE_POSTINDEXED_INDIRECT);
+        end
   end
 
+always @(posedge clk)
+  begin
+      if (decoded_instr == I_AND)
+        begin
+            cover(address_code == ADDR_MODE_IMMEDIATE);
+            cover(address_code == ADDR_MODE_ABSOLUTE);
+            cover(address_code == ADDR_MODE_ZP);
+            cover(address_code == ADDR_MODE_INDEXED_ABSOLUTE_X);
+            cover(address_code == ADDR_MODE_INDEXED_ABSOLUTE_Y);
+            cover(address_code == ADDR_MODE_INDEXED_ZP);
+            cover(address_code == ADDR_MODE_PREINDEXED_INDIRECT);
+        end
+  end
+
+always @(posedge clk)
+  begin
+      if (decoded_instr == I_ORA)
+        begin
+            cover(address_code == ADDR_MODE_IMMEDIATE);
+            cover(address_code == ADDR_MODE_ABSOLUTE);
+            cover(address_code == ADDR_MODE_ZP);
+            cover(address_code == ADDR_MODE_INDEXED_ABSOLUTE_X);
+            cover(address_code == ADDR_MODE_INDEXED_ABSOLUTE_Y);
+            cover(address_code == ADDR_MODE_INDEXED_ZP);
+            cover(address_code == ADDR_MODE_PREINDEXED_INDIRECT);
+        end
+  end
+
+always @(posedge clk)
+  begin
+      if (decoded_instr == I_DEX)
+        begin
+            cover(address_code == ADDR_MODE_IMPLIED);
+        end
+  end
+
+always @(posedge clk)
+  begin
+      if (decoded_instr == I_DEY)
+        begin
+            cover(address_code == ADDR_MODE_IMPLIED);
+        end
+  end
 `endif
 
 endmodule

src/slon.sby

@@ -4,12 +4,12 @@ cvr
 
 [options]
 prf: mode prove
-prf: depth 30
+prf: depth 20
 cvr: mode cover
-cvr: depth 60
+cvr: depth 100
 
 [engines]
-smtbmc yices
+smtbmc --unroll yices
 
 [script]
 read  -formal decoder.verilog