Fix timings for STA

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;
@@ -27,6 +26,7 @@ module cpu
     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,
@@ -87,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;
@@ -102,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),
@@ -236,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
@@ -292,6 +310,7 @@ always @(posedge clk)
               PC <= PC + 1;
               state <= STATE_EXECUTE;
           end
+    end
   else if (state == STATE_EXECUTE)
     begin
         instr <= mem_data;
@@ -319,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
@@ -347,6 +367,10 @@ always @(posedge clk)
           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
@@ -376,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)
@@ -399,7 +430,11 @@ always @(posedge clk)
           begin
               pending_y_read <= READ_SOURCE_MEM;
           end
-        else
+        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
@@ -446,6 +481,7 @@ always @(posedge clk)
     begin
         mem_aux_addr <= mem_data;
         state <= STATE_EXECUTE_DATA_2;
+        PC <= PC + 1'b1;
     end
   else if (state == STATE_FETCH_DATA_2)
     begin
@@ -463,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
@@ -490,8 +527,6 @@ always_comb
       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
@@ -499,7 +534,6 @@ always_comb
                   mem_wr = 1'b1;
               end
         end
-        end
       else if (state == STATE_EXECUTE_ZP)
         begin
             if(decoded_instr == I_STA)
@@ -554,12 +588,13 @@ always @(posedge clk)
       f6_past_valid <= 1;
 
     logic [7:0] f_instr_count;
+initial f_instr_count = 0;
 always @(posedge clk)
-    if (state == STATE_FETCH)
+    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)
+  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);
@@ -635,25 +670,29 @@ always_comb
   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)
+    if (f_past_valid)
 begin
-                assert(PC == $past(PC, 3) + 16'd3);
-            end
+      assume(decoded_instr == I_LDA ||
+             decoded_instr == I_LDX ||
+             decoded_instr == I_LDY ||
+             decoded_instr == I_STA ||
+             decoded_instr == I_STX ||
+             decoded_instr == I_STY ||
+             decoded_instr == I_AND ||
+             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 &&
-      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))
+  if (f6_past_valid && state == STATE_EXECUTE && $past(state) == STATE_FETCH)
     begin
         if (f_prev_instruction == I_EOR)
           assert(A == ($past(A) ^ $past(mem_data)));
@@ -663,19 +702,23 @@ always @(posedge clk)
           assert(A == ($past(A) | $past(mem_data)));
         else if (f_prev_instruction == I_ADC)
           assert(A == ($past(A) + $past(mem_data) + $past(P[P_C])));
+        else if (f_prev_instruction == I_SBC)
+          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
           assume(0);
 
         if (f_prev_instruction == I_STA)
           begin
               assert($past(mem_wr, 2) == 1'b1);
-              assert($past(mem_data_wr) == A);
+              assert($past(mem_data_wr, 2) == $past(A, 2));
           end
         else
           begin
@@ -687,7 +730,12 @@ always @(posedge clk)
         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)
@@ -702,21 +750,33 @@ always @(posedge clk)
               assert(($past(f_abs_address, 2) + $past(Y, 2)) == $past(mem_addr_eff, 2));
           end
 
-        if (f_prev_instruction == I_LDX)
+        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)
+        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
+        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));
           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)} +
@@ -724,6 +784,13 @@ always @(posedge clk)
                                 {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));
@@ -742,16 +809,37 @@ always @(posedge clk)
               assert(Y == $past(Y, 2));
           end
 
-        if (f3_past_valid)
+        if (f6_past_valid)
           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
 
@@ -784,11 +872,10 @@ always @(posedge clk)
       end
 
 always @(posedge clk)
-  if (f_past_valid)
-    assume(state != $past(state));
+  cover(state == STATE_EXECUTE);
 
 always @(posedge clk)
-  cover(state == STATE_EXECUTE);
+  cover(f6_past_valid);
 
 always @(posedge clk)
   cover(f_instr_count > 16);
@@ -804,6 +891,22 @@ always @(posedge clk)
             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_SBC)
+        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
 
@@ -818,6 +921,21 @@ always @(posedge clk)
             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
 
@@ -844,6 +962,7 @@ always @(posedge clk)
             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
 

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