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
Split View
Diff Options
Show Stats
  1. 636
      src/cpu.verilog
  2. 6
      src/slon.sby

636
src/cpu.verilog
Unescape View File

@ -11,6 +11,7 @@ module cpu @@ -11,6 +11,7 @@ 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;
@ -22,11 +23,8 @@ module cpu @@ -22,11 +23,8 @@ module cpu
localparam STATE_FETCH_DATA_2 = 4;
localparam STATE_EXECUTE_DATA_2 = 5;
localparam STATE_BRANCH = 7;
localparam STATE_EXECUTE_IDX_1 = 8;
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 STATE_EXECUTE_PRE_IDX_1 = 8;
localparam STATE_EXECUTE_PRE_IDX_2 = 9;
localparam
READ_SOURCE_NONE = 2'h0,
@ -87,8 +85,6 @@ localparam @@ -87,8 +85,6 @@ 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;
@ -104,13 +100,12 @@ initial pending_y_read = 0; @@ -104,13 +100,12 @@ 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 || decoded_instr == I_SBC);
assign is_arith = (decoded_instr == I_ADC);
alu alui(
.A(alu_op_1),
@ -178,21 +173,6 @@ always_comb @@ -178,21 +173,6 @@ 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
@ -215,7 +195,13 @@ always_comb @@ -215,7 +195,13 @@ always_comb
alu_op_c = 1'b1;
alu_op_sel = OP_SUB;
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
alu_op_1 = A;
alu_op_2 = mem_data;
@ -239,77 +225,61 @@ always_comb @@ -239,77 +225,61 @@ 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 (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)
if (pending_a_read == READ_SOURCE_MEM)
begin
extra_timing <= extra_timing - 1'b1;
A <= mem_data;
P[P_Z] <= (mem_data == 0);
P[P_N] <= mem_data[7];
end
else
else if (pending_a_read == READ_SOURCE_ALU)
begin
if (pending_a_read == READ_SOURCE_MEM)
A <= alu_op_result;
P[P_Z] <= alu_z;
P[P_N] <= alu_n;
if (is_arith)
begin
A <= mem_data;
P[P_Z] <= (mem_data == 0);
P[P_N] <= mem_data[7];
P[P_C] <= alu_c;
P[P_V] <= alu_v;
end
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;
end
pending_a_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_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;
PC <= PC + 1;
state <= STATE_EXECUTE;
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;
end
else if (state == STATE_EXECUTE)
begin
@ -338,8 +308,7 @@ always @(posedge clk) @@ -338,8 +308,7 @@ always @(posedge clk)
else if (decoded_instr == I_EOR ||
decoded_instr == I_AND ||
decoded_instr == I_ORA ||
decoded_instr == I_ADC ||
decoded_instr == I_SBC)
decoded_instr == I_ADC)
begin
pending_a_read <= READ_SOURCE_ALU;
end
@ -361,16 +330,7 @@ always @(posedge clk) @@ -361,16 +330,7 @@ always @(posedge clk)
end
else if (address_code == ADDR_MODE_PREINDEXED_INDIRECT)
begin
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
state <= STATE_EXECUTE_PRE_IDX_1;
end
else if (address_code == ADDR_MODE_IMPLIED)
begin
@ -401,14 +361,7 @@ always @(posedge clk) @@ -401,14 +361,7 @@ always @(posedge clk)
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
mem_aux_addr <= mem_data + X;
state <= STATE_EXECUTE_ZP;
end
else if (state == STATE_EXECUTE_ZP)
@ -418,26 +371,7 @@ always @(posedge clk) @@ -418,26 +371,7 @@ 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
pending_a_read <= READ_SOURCE_ALU;
state <= STATE_FETCH;
end
@ -450,39 +384,21 @@ always @(posedge clk) @@ -450,39 +384,21 @@ always @(posedge clk)
pending_rel_branch <= 0;
state <= STATE_FETCH;
end
else if (state == STATE_EXECUTE_IDX_1)
else if (state == STATE_EXECUTE_PRE_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[7:0] <= mem_data + X;
mem_aux2_addr[15:8] <= 0;
state <= STATE_EXECUTE_IDX_2;
state <= STATE_EXECUTE_PRE_IDX_2;
end
else if (state == STATE_EXECUTE_IDX_2)
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_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;
@ -491,36 +407,27 @@ always @(posedge clk) @@ -491,36 +407,27 @@ 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 ||
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
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)
begin
PC <= mem_addr;
end
end
always_comb
begin
@ -528,38 +435,21 @@ always_comb @@ -528,38 +435,21 @@ always_comb
mem_wr = 0;
if (state == STATE_EXECUTE_DATA_2)
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)
if (address_code == ADDR_MODE_ABSOLUTE)
begin
mem_wr = 1'b1;
mem_data_wr = Y;
if(decoded_instr == I_STA)
begin
mem_data_wr = A;
mem_wr = 1'b1;
end
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
@ -573,13 +463,6 @@ always_comb @@ -573,13 +463,6 @@ 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;
@ -609,34 +492,6 @@ always @(posedge clk) @@ -609,34 +492,6 @@ 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)
@ -707,84 +562,45 @@ always_comb @@ -707,84 +562,45 @@ always_comb
end
always @(posedge clk)
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
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
always @(posedge clk)
if (f6_past_valid && state == STATE_EXECUTE && $past(state) == STATE_FETCH)
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))
begin
if (f_prev_instruction == I_EOR)
if ($past(decoded_instr, 2) == I_EOR)
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)));
else if (f_prev_instruction == I_ORA)
else if ($past(decoded_instr, 2) == I_ORA)
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])));
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
begin
assert($past(mem_wr, 2) == 1'b0);
end
assume(0);
assert($past(mem_wr, 2) == 1'b0);
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
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)
@ -794,52 +610,16 @@ always @(posedge clk) @@ -794,52 +610,16 @@ 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));
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)
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 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));
@ -849,50 +629,19 @@ always @(posedge clk) @@ -849,50 +629,19 @@ 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
assert(X == $past(X, 2));
assert(Y == $past(Y, 2));
if (f6_past_valid && !f_prev_instruction_is_branch)
if (f3_past_valid)
begin
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)
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)
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)
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
@ -925,143 +674,34 @@ always @(posedge clk) @@ -925,143 +674,34 @@ always @(posedge clk)
end
always @(posedge clk)
cover(state == STATE_EXECUTE);
always @(posedge clk)
cover(f6_past_valid);
if (f_past_valid)
assume(state != $past(state));
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)
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
cover(state == STATE_EXECUTE);
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
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
if (decoded_instr == I_DEX)
begin
cover(address_code == ADDR_MODE_IMPLIED);
end
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
always @(posedge clk)
begin
if (decoded_instr == I_DEY)
begin
cover(address_code == ADDR_MODE_IMPLIED);
end
end
`endif
endmodule

6
src/slon.sby
Unescape View File

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

Write Preview
Loading…
Cancel
Save