asakul
/
slon
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

Compare commits

base: asakul:0f1ab8fd19d266189563960e7e78fa2f82f3c7bb
Branches Tags
asakul:master
..
compare: asakul:bed4bc7316d182cfa0b1a8a974d8b81e919971a6
Branches Tags
asakul:master

No commits in common. '0f1ab8fd19d266189563960e7e78fa2f82f3c7bb' and 'bed4bc7316d182cfa0b1a8a974d8b81e919971a6' have entirely different histories.
0f1ab8fd19 ... bed4bc7316

2 changed files with 141 additions and 501 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats
  1. 488
      src/cpu.verilog
  2. 6
      src/slon.sby

488
src/cpu.verilog
Unescape View File

@ -11,6 +11,7 @@ module cpu
`include "parameters.vh" `include "parameters.vh"
localparam STATE_START_1 = 4'hc;
localparam STATE_START_2 = 4'hd; localparam STATE_START_2 = 4'hd;
localparam STATE_START_3 = 4'he; localparam STATE_START_3 = 4'he;
localparam STATE_START_4 = 4'hf; localparam STATE_START_4 = 4'hf;
@ -22,11 +23,8 @@ module cpu
localparam STATE_FETCH_DATA_2 = 4; localparam STATE_FETCH_DATA_2 = 4;
localparam STATE_EXECUTE_DATA_2 = 5; localparam STATE_EXECUTE_DATA_2 = 5;
localparam STATE_BRANCH = 7; localparam STATE_BRANCH = 7;
localparam STATE_EXECUTE_IDX_1 = 8; localparam STATE_EXECUTE_PRE_IDX_1 = 8;
localparam STATE_EXECUTE_IDX_2 = 9; localparam STATE_EXECUTE_PRE_IDX_2 = 9;
localparam STATE_EXECUTE_POST_IDX_1 = 10;
localparam STATE_EXECUTE_POST_IDX_2 = 11;
localparam STATE_DELAY = 12;
localparam localparam
READ_SOURCE_NONE = 2'h0, READ_SOURCE_NONE = 2'h0,
@ -87,8 +85,6 @@ localparam
logic [1:0] pending_y_read; logic [1:0] pending_y_read;
logic pending_rel_branch; logic pending_rel_branch;
wire is_arith; wire is_arith;
logic [2:0] extra_timing;
reg [3:0] state_after_delay;
initial A = 0; initial A = 0;
initial X = 0; initial X = 0;
@ -104,13 +100,12 @@ initial pending_y_read = 0;
initial pending_rel_branch = 0; initial pending_rel_branch = 0;
initial mem_aux_addr = 0; initial mem_aux_addr = 0;
initial instr = 0; initial instr = 0;
initial extra_timing = 0;
assign o_state[3:0] = state; assign o_state[3:0] = state;
assign o_state[31:24] = A; assign o_state[31:24] = A;
assign o_state[23:16] = X; assign o_state[23:16] = X;
assign is_arith = (decoded_instr == I_ADC || decoded_instr == I_SBC); assign is_arith = (decoded_instr == I_ADC);
alu alui( alu alui(
.A(alu_op_1), .A(alu_op_1),
@ -178,21 +173,6 @@ always_comb
begin begin
{mem_aux_addr_hi, mem_aux_addr_lo} = {mem_data, mem_aux_addr} + Y; {mem_aux_addr_hi, mem_aux_addr_lo} = {mem_data, mem_aux_addr} + Y;
end 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 end
always_comb always_comb
@ -215,7 +195,13 @@ always_comb
alu_op_c = 1'b1; alu_op_c = 1'b1;
alu_op_sel = OP_SUB; alu_op_sel = OP_SUB;
end end
else 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)
begin begin
alu_op_1 = A; alu_op_1 = A;
alu_op_2 = mem_data; alu_op_2 = mem_data;
@ -239,26 +225,11 @@ always_comb
alu_op_c = P[P_C]; alu_op_c = P[P_C];
alu_op_sel = OP_ADC; alu_op_sel = OP_ADC;
end end
else if (decoded_instr == I_SBC)
begin
alu_op_c = P[P_C];
alu_op_sel = OP_SUB;
end
end end
end end
always @(posedge clk) always @(posedge clk)
if (extra_timing > 0) if (state == STATE_FETCH)
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 begin
if (pending_a_read == READ_SOURCE_MEM) if (pending_a_read == READ_SOURCE_MEM)
begin begin
@ -310,7 +281,6 @@ always @(posedge clk)
PC <= PC + 1; PC <= PC + 1;
state <= STATE_EXECUTE; state <= STATE_EXECUTE;
end end
end
else if (state == STATE_EXECUTE) else if (state == STATE_EXECUTE)
begin begin
instr <= mem_data; instr <= mem_data;
@ -338,8 +308,7 @@ always @(posedge clk)
else if (decoded_instr == I_EOR || else if (decoded_instr == I_EOR ||
decoded_instr == I_AND || decoded_instr == I_AND ||
decoded_instr == I_ORA || decoded_instr == I_ORA ||
decoded_instr == I_ADC || decoded_instr == I_ADC)
decoded_instr == I_SBC)
begin begin
pending_a_read <= READ_SOURCE_ALU; pending_a_read <= READ_SOURCE_ALU;
end end
@ -361,16 +330,7 @@ always @(posedge clk)
end end
else if (address_code == ADDR_MODE_PREINDEXED_INDIRECT) else if (address_code == ADDR_MODE_PREINDEXED_INDIRECT)
begin begin
state <= STATE_EXECUTE_IDX_1; state <= STATE_EXECUTE_PRE_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 end
else if (address_code == ADDR_MODE_IMPLIED) else if (address_code == ADDR_MODE_IMPLIED)
begin begin
@ -400,15 +360,8 @@ always @(posedge clk)
end end
end end
else if (state == STATE_EXECUTE_ZPX) else if (state == STATE_EXECUTE_ZPX)
begin
if (decoded_instr != I_LDX)
begin begin
mem_aux_addr <= mem_data + X; mem_aux_addr <= mem_data + X;
end
else
begin
mem_aux_addr <= mem_data + Y;
end
state <= STATE_EXECUTE_ZP; state <= STATE_EXECUTE_ZP;
end end
else if (state == STATE_EXECUTE_ZP) else if (state == STATE_EXECUTE_ZP)
@ -418,26 +371,7 @@ always @(posedge clk)
mem_aux_addr <= mem_data; mem_aux_addr <= mem_data;
end end
mem_sel <= DMUX_PC; 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; pending_a_read <= READ_SOURCE_ALU;
end
state <= STATE_FETCH; state <= STATE_FETCH;
end end
@ -450,39 +384,21 @@ always @(posedge clk)
pending_rel_branch <= 0; pending_rel_branch <= 0;
state <= STATE_FETCH; state <= STATE_FETCH;
end end
else if (state == STATE_EXECUTE_IDX_1) else if (state == STATE_EXECUTE_PRE_IDX_1)
begin begin
mem_sel <= DMUX_AUX2; mem_sel <= DMUX_AUX2;
if (address_code == ADDR_MODE_PREINDEXED_INDIRECT)
begin
mem_aux2_addr[7:0] <= mem_data + X; 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; mem_aux2_addr[15:8] <= 0;
state <= STATE_EXECUTE_IDX_2; state <= STATE_EXECUTE_PRE_IDX_2;
end end
else if (state == STATE_EXECUTE_IDX_2) else if (state == STATE_EXECUTE_PRE_IDX_2)
begin begin
mem_aux_addr <= mem_data; mem_aux_addr <= mem_data;
mem_aux2_addr[7:0] <= mem_aux2_addr[7:0] + 1'b1; mem_aux2_addr[7:0] <= mem_aux2_addr[7:0] + 1'b1;
state <= STATE_FETCH_DATA_2; state <= STATE_FETCH_DATA_2;
end 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) else if (state == STATE_FETCH_DATA_2)
begin begin
mem_aux_addr[7:0] <= mem_data; mem_aux_addr[7:0] <= mem_data;
@ -499,8 +415,7 @@ always @(posedge clk)
if (decoded_instr == I_EOR || if (decoded_instr == I_EOR ||
decoded_instr == I_AND || decoded_instr == I_AND ||
decoded_instr == I_ORA || decoded_instr == I_ORA ||
decoded_instr == I_ADC || decoded_instr == I_ADC)
decoded_instr == I_SBC)
begin begin
pending_a_read <= READ_SOURCE_ALU; pending_a_read <= READ_SOURCE_ALU;
end end
@ -508,14 +423,6 @@ always @(posedge clk)
begin begin
pending_a_read <= READ_SOURCE_MEM; pending_a_read <= READ_SOURCE_MEM;
end 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) else if(decoded_instr == I_JMP)
begin begin
PC <= mem_addr; PC <= mem_addr;
@ -527,39 +434,22 @@ always_comb
mem_data_wr = 0; mem_data_wr = 0;
mem_wr = 0; mem_wr = 0;
if (state == STATE_EXECUTE_DATA_2) if (state == STATE_EXECUTE_DATA_2)
begin
if (address_code == ADDR_MODE_ABSOLUTE)
begin begin
if(decoded_instr == I_STA) if(decoded_instr == I_STA)
begin begin
mem_wr = 1'b1;
mem_data_wr = A; mem_data_wr = A;
end
else if (decoded_instr == I_STX)
begin
mem_wr = 1'b1; mem_wr = 1'b1;
mem_data_wr = X;
end end
else if (decoded_instr == I_STY)
begin
mem_wr = 1'b1;
mem_data_wr = Y;
end end
end end
else if (state == STATE_EXECUTE_ZP) else if (state == STATE_EXECUTE_ZP)
begin begin
if(decoded_instr == I_STA) if(decoded_instr == I_STA)
begin begin
mem_wr = 1'b1;
mem_data_wr = A; mem_data_wr = A;
end
else if(decoded_instr == I_STX)
begin
mem_wr = 1'b1; 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 end
end end
@ -573,13 +463,6 @@ always_comb
logic f5_past_valid; logic f5_past_valid;
logic f6_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 f_past_valid = 0;
initial f2_past_valid = 0; initial f2_past_valid = 0;
initial f3_past_valid = 0; initial f3_past_valid = 0;
@ -609,34 +492,6 @@ always @(posedge clk)
if (f5_past_valid) if (f5_past_valid)
f6_past_valid <= 1; 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) always @(posedge clk)
if (f2_past_valid && state == STATE_EXECUTE) if (f2_past_valid && state == STATE_EXECUTE)
if ($past(decoded_instr) == I_DEX) if ($past(decoded_instr) == I_DEX)
@ -707,84 +562,45 @@ always_comb
end end
always @(posedge clk) always @(posedge clk)
if (f_past_valid) if (f2_past_valid && state == STATE_EXECUTE_DATA_2)
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 end
always @(posedge clk) always @(posedge clk)
if (f6_past_valid && state == STATE_EXECUTE && $past(state) == STATE_FETCH) if (f6_past_valid &&
begin state == STATE_EXECUTE &&
if (f_prev_instruction == I_EOR) $past(state) == STATE_FETCH &&
($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))); assert(A == ($past(A) ^ $past(mem_data)));
else if (f_prev_instruction == I_AND) else if ($past(decoded_instr, 2) == I_AND)
assert(A == ($past(A) & $past(mem_data))); assert(A == ($past(A) & $past(mem_data)));
else if (f_prev_instruction == I_ORA) else if ($past(decoded_instr, 2) == I_ORA)
assert(A == ($past(A) | $past(mem_data))); assert(A == ($past(A) | $past(mem_data)));
else if (f_prev_instruction == I_ADC) else if ($past(decoded_instr, 2) == I_ADC)
assert(A == ($past(A) + $past(mem_data) + $past(P[P_C]))); 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 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 else
begin assume(0);
assert($past(mem_wr, 2) == 1'b0); assert($past(mem_wr, 2) == 1'b0);
end
if ($past(address_code, 2) == ADDR_MODE_ABSOLUTE) if ($past(address_code, 2) == ADDR_MODE_ABSOLUTE)
assert($past(f_abs_address, 2) == $past(mem_addr_eff, 2)); assert($past(f_abs_address, 2) == $past(mem_addr_eff, 2));
else if ($past(address_code, 2) == ADDR_MODE_ZP) else if ($past(address_code, 2) == ADDR_MODE_ZP)
assert($past(mem_data, 2) == $past(mem_addr_eff, 2)); assert($past(mem_data, 2) == $past(mem_addr_eff, 2));
else if ($past(address_code, 2) == ADDR_MODE_INDEXED_ZP) 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)); 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) 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)); 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) else if ($past(address_code, 2) == ADDR_MODE_INDEXED_ABSOLUTE_Y)
@ -794,52 +610,16 @@ always @(posedge clk)
assert($past(f_abs_address, 2) == $past(mem_addr_eff, 2)); 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)); assert($past(mem_addr_eff, 4) == (($past(mem_data, 5) + $past(X, 5)) & 8'hff));
end 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_Z] == (A == 0));
assert(P[P_N] == (A[7] == 1)); assert(P[P_N] == (A[7] == 1));
end if ($past(decoded_instr) == I_ADC)
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 begin
assert(P[P_C] == ({1'b0, $past(A)} + assert(P[P_C] == ({1'b0, $past(A)} +
{1'b0, $past(mem_data)} + {1'b0, $past(mem_data)} +
{8'b0, $past(P[P_C])} >= 9'h100)); {8'b0, $past(P[P_C])} >= 9'h100));
assert(P[P_V] == (($past(A[7]) ^ A[7]) & ($past(mem_data[7]) ^ A[7]))); assert(P[P_V] == (($past(A[7]) ^ A[7]) & ($past(mem_data[7]) ^ A[7])));
end 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 else
begin begin
assert(P[P_C] == $past(P[P_C], 2)); assert(P[P_C] == $past(P[P_C], 2));
@ -849,50 +629,19 @@ always @(posedge clk)
assert(P[P_D] == $past(P[P_D], 2)); assert(P[P_D] == $past(P[P_D], 2));
assert(P[P_I] == $past(P[P_I], 2)); assert(P[P_I] == $past(P[P_I], 2));
assert(S == $past(S, 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)); 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)); assert(Y == $past(Y, 2));
end
if (f6_past_valid && !f_prev_instruction_is_branch) if (f3_past_valid)
begin begin
if ($past(address_code, 2) == ADDR_MODE_ABSOLUTE) if ($past(address_code, 2) == ADDR_MODE_ABSOLUTE)
assert($past(PC, 1) == $past(PC, 5) + 16'd3); assert($past(PC, 2) == $past(PC, 5) + 16'd3);
else if ($past(address_code, 2) == ADDR_MODE_ZP) else if ($past(address_code, 2) == ADDR_MODE_ZP)
assert($past(PC, 1) == $past(PC, 4) + 16'd2); assert($past(PC, 2) == $past(PC, 4) + 16'd2);
else if ($past(address_code, 2) == ADDR_MODE_INDEXED_ZP) else if ($past(address_code, 2) == ADDR_MODE_INDEXED_ZP)
assert($past(PC, 1) == $past(PC, 5) + 16'd2); assert($past(PC, 2) == $past(PC, 5) + 16'd2);
else if ($past(address_code, 2) == ADDR_MODE_IMMEDIATE) else if ($past(address_code, 2) == ADDR_MODE_IMMEDIATE)
assert($past(PC, 1) == $past(PC, 3) + 16'd2); 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
end end
@ -925,143 +674,34 @@ always @(posedge clk)
end end
always @(posedge clk) always @(posedge clk)
cover(state == STATE_EXECUTE); if (f_past_valid)
assume(state != $past(state));
always @(posedge clk)
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
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
always @(posedge clk)
begin
if (decoded_instr == I_LDA)
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_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) always @(posedge clk)
begin cover(state == STATE_EXECUTE);
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) always @(posedge clk)
begin begin
if (decoded_instr == I_ORA) cover(decoded_instr == I_ADC && address_code == ADDR_MODE_IMMEDIATE);
begin cover(decoded_instr == I_ADC && address_code == ADDR_MODE_ABSOLUTE);
cover(address_code == ADDR_MODE_IMMEDIATE); cover(decoded_instr == I_ADC && address_code == ADDR_MODE_ZP);
cover(address_code == ADDR_MODE_ABSOLUTE); cover(decoded_instr == I_ADC && address_code == ADDR_MODE_INDEXED_ABSOLUTE_X);
cover(address_code == ADDR_MODE_ZP); cover(decoded_instr == I_ADC && address_code == ADDR_MODE_INDEXED_ABSOLUTE_Y);
cover(address_code == ADDR_MODE_INDEXED_ABSOLUTE_X); cover(decoded_instr == I_ADC && address_code == ADDR_MODE_INDEXED_ZP);
cover(address_code == ADDR_MODE_INDEXED_ABSOLUTE_Y); cover(decoded_instr == I_ADC && address_code == ADDR_MODE_PREINDEXED_INDIRECT);
cover(address_code == ADDR_MODE_INDEXED_ZP);
cover(address_code == ADDR_MODE_PREINDEXED_INDIRECT);
end
end end
always @(posedge clk) always @(posedge clk)
begin begin
if (decoded_instr == I_DEX) cover(decoded_instr == I_LDA && address_code == ADDR_MODE_IMMEDIATE);
begin cover(decoded_instr == I_LDA && address_code == ADDR_MODE_ABSOLUTE);
cover(address_code == ADDR_MODE_IMPLIED); cover(decoded_instr == I_LDA && address_code == ADDR_MODE_ZP);
end 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 end
always @(posedge clk)
begin
if (decoded_instr == I_DEY)
begin
cover(address_code == ADDR_MODE_IMPLIED);
end
end
`endif `endif
endmodule endmodule

6
src/slon.sby
Unescape View File

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

Write Preview
Loading…
Cancel
Save