From e66e89bbd9a5b6f2901b2113f5bee0954aad2a5d Mon Sep 17 00:00:00 2001 From: Denis Tereshkin Date: Sat, 8 Nov 2025 19:04:11 +0700 Subject: [PATCH] Fix timings for STA --- src/cpu.verilog | 343 ++++++++++++++++++++++++++++++++---------------- src/slon.sby | 6 +- 2 files changed, 234 insertions(+), 115 deletions(-) diff --git a/src/cpu.verilog b/src/cpu.verilog index 3e46f1d..f948a5f 100644 --- a/src/cpu.verilog +++ b/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,61 +239,77 @@ 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 (pending_a_read == READ_SOURCE_MEM) + if (extra_timing > 0) begin - A <= mem_data; - P[P_Z] <= (mem_data == 0); - P[P_N] <= mem_data[7]; + extra_timing <= extra_timing - 1'b1; end - else if (pending_a_read == READ_SOURCE_ALU) + else begin - A <= alu_op_result; - P[P_Z] <= alu_z; - P[P_N] <= alu_n; - if (is_arith) + if (pending_a_read == READ_SOURCE_MEM) begin - P[P_C] <= alu_c; - P[P_V] <= alu_v; + A <= mem_data; + P[P_Z] <= (mem_data == 0); + P[P_N] <= mem_data[7]; end - end - pending_a_read <= READ_SOURCE_NONE; + else if (pending_a_read == READ_SOURCE_ALU) + begin + 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; - if (pending_x_read == READ_SOURCE_MEM) - begin - X <= mem_data; - P[P_Z] <= (mem_data == 0); - P[P_N] <= mem_data[7]; - end - else if (pending_x_read == READ_SOURCE_ALU) - begin - X <= alu_op_result; - P[P_Z] <= alu_z; - P[P_N] <= alu_n; - end - pending_x_read <= READ_SOURCE_NONE; + if (pending_x_read == READ_SOURCE_MEM) + begin + X <= mem_data; + P[P_Z] <= (mem_data == 0); + P[P_N] <= mem_data[7]; + end + else if (pending_x_read == READ_SOURCE_ALU) + begin + X <= alu_op_result; + P[P_Z] <= alu_z; + P[P_N] <= alu_n; + end + pending_x_read <= READ_SOURCE_NONE; - if (pending_y_read == READ_SOURCE_MEM) - begin - Y <= mem_data; - P[P_Z] <= (mem_data == 0); - P[P_N] <= mem_data[7]; - end - else if (pending_y_read == READ_SOURCE_ALU) - begin - Y <= alu_op_result; - P[P_Z] <= alu_z; - P[P_N] <= alu_n; - end - pending_y_read <= READ_SOURCE_NONE; + if (pending_y_read == READ_SOURCE_MEM) + begin + Y <= mem_data; + P[P_Z] <= (mem_data == 0); + P[P_N] <= mem_data[7]; + end + else if (pending_y_read == READ_SOURCE_ALU) + begin + Y <= alu_op_result; + P[P_Z] <= alu_z; + P[P_N] <= alu_n; + end + pending_y_read <= READ_SOURCE_NONE; - PC <= PC + 1; - state <= STATE_EXECUTE; + PC <= PC + 1; + state <= STATE_EXECUTE; + end end else if (state == STATE_EXECUTE) begin @@ -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 @@ -377,7 +401,14 @@ always @(posedge clk) end else if (state == STATE_EXECUTE_ZPX) begin - mem_aux_addr <= mem_data + X; + 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 @@ -455,35 +491,36 @@ always @(posedge clk) state <= STATE_EXECUTE_DATA_2; PC <= PC + 1'b1; end - else if (state == STATE_EXECUTE_DATA_2) - begin - mem_sel <= DMUX_PC; - state <= STATE_FETCH; + 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_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; - end - end + if (decoded_instr == I_EOR || + decoded_instr == I_AND || + decoded_instr == I_ORA || + decoded_instr == I_ADC || + decoded_instr == I_SBC) + 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_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; + end + end always_comb begin @@ -491,13 +528,10 @@ 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_data_wr = A; - mem_wr = 1'b1; - end + mem_data_wr = A; + mem_wr = 1'b1; end end else if (state == STATE_EXECUTE_ZP) @@ -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) - begin - assert(PC == $past(PC, 3) + 16'd3); - end - end + if (f_past_valid) +begin + 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) - assert((($past(mem_data, 3) + $past(X, 3)) & 16'hff) == $past(mem_addr_eff, 2)); + 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 diff --git a/src/slon.sby b/src/slon.sby index 88eba2e..2d05d38 100644 --- a/src/slon.sby +++ b/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